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 S1[ Nat] means for j being Nat st j = i + $1 holds
x in C . j;
A: S1[ 0 ] by AS;
B: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume IV: S1[k] ; :: thesis: S1[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 S1[k + 1] ; :: thesis: verum
end;
I: for k being Nat holds S1[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