a,b:
, P:({a..b
}
Prop).
Thm* a<b
((
i:{a..b}. P(i)) 
(i:{a..(b-1)}. P(i)) 
P(b-1))a,b:, P:({a..b}Prop).
Thm* a<b
Thm*
Thm* (
c:. b = c+1 ((i:{a..b}. P(i)) (i:{a..c}. P(i)) P(c)))| Theorem | Name |
| a,b:, P:({a..b}Prop).
Thm* a<b ((i:{a..b}. P(i)) (i:{a..(b-1)}. P(i)) P(b-1)) | [or_via_exist_intseg_split_last] |
| cites the following: | |
| a,b:, P:({a..b}Prop).
Thm* a<b Thm*
Thm* ( c:. b = c+1 ((i:{a..b}. P(i)) (i:{a..c}. P(i)) P(c))) | [or_via_exist_intseg_notnull] |