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_lower_ind] |
| cites | ||
| 4 |
Thm* n:. WellFnd{i}({...n};x,y.x > y) | [int_lower_well_founded] |