i:
, j:{i...}. WellFnd{u}({i..j
};x,y.x > y)n:. WellFnd{i}({n...};x,y.x < y)r:(A
AProp), B:Type, f:(BA).
WellFnd{i}(A;x,y.r(x,y)) 
WellFnd{i}(B;x,y.r(f(x),f(y)))i,j:. i > j 
-i < -ja,b,n:. a < b a+n < b+n| Rank | Theorem | Name |
| 5 |
Thm* i:, j:{i...}. WellFnd{u}({i..j};x,y.x > y) | [int_seg_well_founded_down] |
| cites | ||
| 4 |
Thm* n:. WellFnd{i}({n...};x,y.x < y) | [int_upper_well_founded] |
| 1 |
Thm* r:(AAProp), B:Type, f:(BA).
WellFnd{i}(A;x,y.r(x,y)) WellFnd{i}(B;x,y.r(f(x),f(y))) | [inv_image_ind] |
| 0 |
Thm* i,j:. i > j -i < -j | [minus_mono_wrt_lt] |
| 3 |
Thm* a,b,n:. a < b a+n < b+n | [add_mono_wrt_lt] |