i:
, E:({i...}
Prop).
E(i) 
(k:{i+1...}. E(k-1) E(k)) (k:{i...}. E(k))n:. WellFnd{i}({n...};x,y.x < y)| Rank | Theorem | Name |
| 5 |
Thm* i:, E:({i...}Prop).
E(i) (k:{i+1...}. E(k-1) E(k)) (k:{i...}. E(k)) | [int_upper_ind] |
| cites | ||
| 4 |
Thm* n:. WellFnd{i}({n...};x,y.x < y) | [int_upper_well_founded] |