i:
, j:{i+1...}, E:({i..j
}
Prop).
Thm* 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 |
| 5 | i:, j:{i+1...}, E:({i..j}Prop).
Thm* E(i) (k:{(i+1)..j}. E(k-1) E(k)) (k:{i..j}. E(k)) | [int_seg_ind] |
| cites the following: | ||
| 4 | i:, j:{i...}. WellFnd{u}({i..j};x,y.x<y) | [int_seg_well_founded_up] |