n:
. WellFnd{i}({...n};x,y.x>y)n:. WellFnd{i}({n...};x,y.x<y)r:(T
TProp), S:Type, f:(ST).
Thm* WellFnd{i}(T;x,y.r(x,y))
WellFnd{i}(S;x,y.r(f(x),f(y)))| Rank | Theorem | Name |
| 4 | n:. WellFnd{i}({...n};x,y.x>y) | [int_lower_well_founded] |
| cites the following: | ||
| 3 | n:. WellFnd{i}({n...};x,y.x<y) | [int_upper_well_founded] |
| 0 | r:(TTProp), S:Type, f:(ST).
Thm* WellFnd{i}(T;x,y.r(x,y)) WellFnd{i}(S;x,y.r(f(x),f(y))) | [inv_image_ind_a] |