let X be set ; :: thesis: for S being SetSequence of X holds
( S is non-descending iff for n being Nat holds S . n c= S . (n + 1) )

let S be SetSequence of X; :: thesis: ( S is non-descending iff for n being Nat holds S . n c= S . (n + 1) )
thus ( S is non-descending implies for n being Nat holds S . n c= S . (n + 1) ) by NAT_1:11; :: thesis: ( ( for n being Nat holds S . n c= S . (n + 1) ) implies S is non-descending )
assume A1: for n being Nat holds S . n c= S . (n + 1) ; :: thesis:
now :: thesis: for n, m being Nat st n <= m holds
S . n c= S . m
let n, m be Nat; :: thesis: ( n <= m implies S . n c= S . m )
assume A2: n <= m ; :: thesis: S . n c= S . m
A3: now :: thesis: for k being Nat holds S1[k]
defpred S1[ Nat] means S . n c= S . (n + \$1);
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S . n c= S . (n + k) ; :: thesis: S1[k + 1]
S . (n + k) c= S . ((n + k) + 1) by A1;
hence S1[k + 1] by ; :: thesis: verum
end;
A6: S1[ 0 ] ;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A6, A4); :: thesis: verum
end;
consider k being Nat such that
A7: m = n + k by ;
thus S . n c= S . m by A3, A7; :: thesis: verum
end;
hence S is non-descending ; :: thesis: verum