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