i:
, E:({i...}
Prop).
Thm* 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 |
| 4 | i:, E:({i...}Prop).
Thm* E(i) (k:{i+1...}. E(k-1) E(k)) (k:{i...}. E(k)) | [int_upper_ind] |
| cites the following: | ||
| 3 | n:. WellFnd{i}({n...};x,y.x<y) | [int_upper_well_founded] |