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)) | [and_via_all_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))) | [and_via_all_intseg_notnull] |