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

proof

assume A1: S is non-descending ; :: thesis: for n being Element of NAT holds S . n c= S . (n + 1)

now

let n be Element of NAT ; :: thesis: S . n c= S . (n + 1)
n <= n + 1 by NAT_1:11;
hence S . n c= S . (n + 1) by A1, PROB_1:def 7; :: thesis: verum

end;

hence for n being Element of NAT holds S . n c= S . (n + 1) ; :: thesis: verum

end;

assume A2: for n being Element of NAT holds S . n c= S . (n + 1) ; :: thesis: S is non-descending

now

let n, m be Element of NAT ; :: thesis: ( n <= m implies S . n c= S . m )
assume A3: n <= m ; :: thesis: S . n c= S . m

A4: now

defpred S₁[ Element of NAT ] means S . n c= S . (n + $1);
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S . n c= S . (n + k) ; :: thesis: S₁[k + 1]
S . (n + k) c= S . ((n + k) + 1) by A2;
hence S₁[k + 1] by A6, XBOOLE_1:1; :: thesis: verum

end;

A7: S₁[ 0 ] ;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A7, A5); :: thesis: verum

end;

consider k being Nat such that
A8: m = n + k by A3, NAT_1:10;
k in NAT by ORDINAL1:def 13;
hence S . n c= S . m by A4, A8; :: thesis: verum

end;

hence S is non-descending by PROB_1:def 7; :: thesis: verum