let X be non empty set ; :: thesis: for C being ascending Chain of X
for x being object
for i, j being Nat st i <= j & x in C . i holds
x in C . j
let C be ascending Chain of X; :: thesis: for x being object
for i, j being Nat st i <= j & x in C . i holds
x in C . j
let x be object ; :: thesis: for i, j being Nat st i <= j & x in C . i holds
x in C . j
let i, j be Nat; :: thesis: ( i <= j & x in C . i implies x in C . j )
assume AS: ( i <= j & x in C . i ) ; :: thesis: x in C . j
defpred S₁[ Nat] means for j being Nat st j = i + $1 holds
x in C . j;
A: S₁[ 0 ] by AS;

B: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for j being Nat st j = i + (k + 1) holds
x in C . j

let j be Nat; :: thesis: ( j = i + (k + 1) implies x in C . j )
assume C: j = i + (k + 1) ; :: thesis: x in C . j
C . (i + k) c= C . ((i + k) + 1) by asc;
hence x in C . j by C, IV; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(A, B);
ex k being Nat st j = i + k by AS, NAT_1:10;
hence x in C . j by I; :: thesis: verum