i:
, j:{i+1...}, E:({i..j
}
Prop).
E(i) 
(k:{(i+1)..j}. E(k-1) E(k)) (k:{i..j}. E(k))i:, j:{i...}. WellFnd{u}({i..j};x,y.x < y)| Rank | Theorem | Name |
| 6 |
Thm* i:, j:{i+1...}, E:({i..j}Prop).
E(i) (k:{(i+1)..j}. E(k-1) E(k)) (k:{i..j}. E(k)) | [int_seg_ind] |
| cites | ||
| 5 |
Thm* i:, j:{i...}. WellFnd{u}({i..j};x,y.x < y) | [int_seg_well_founded_up] |