i:
, j:{i...}. WellFnd{u}({i..j
};x,y.x > y)i:, j:{i...}. WellFnd{u}({i..j};x,y.x < y)n:. WellFnd{i}({...n};x,y.x > y)n:. WellFnd{i}({n...};x,y.x < y);x,y.|x| < |y|)P:(A
Prop). (j:A. (k:A. R(k;j) 
P(k)) P(j)) {n:A. P(n)}
is mentioned by
|
Thm* i:, j:{i...}. WellFnd{u}({i..j};x,y.x > y) | [int_seg_well_founded_down] |
|
Thm* i:, j:{i...}. WellFnd{u}({i..j};x,y.x < y) | [int_seg_well_founded_up] |
|
Thm* n:. WellFnd{i}({...n};x,y.x > y) | [int_lower_well_founded] |
|
Thm* n:. WellFnd{i}({n...};x,y.x < y) | [int_upper_well_founded] |
|
Thm* WellFnd{i}(;x,y.|x| < |y|) | [int_mag_well_founded] |
In prior sections: well fnd int 1
Try larger context: StandardLIB