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: S is non-descending

( 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: S is non-descending

now :: thesis: for n, m being Nat st n <= m holds

S . n c= S . m

hence
S is non-descending
; :: thesis: verumS . 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

A7: m = n + k by A2, NAT_1:10;

thus S . n c= S . m by A3, A7; :: thesis: verum

end;assume A2: n <= m ; :: thesis: S . n c= S . m

A3: now :: thesis: for k being Nat holds S_{1}[k]

consider k being Nat such that defpred S_{1}[ Nat] means S . n c= S . (n + $1);

A4: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

thus for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A6, A4); :: thesis: verum

end;A4: for k being Nat st S

S

proof

A6:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: S . n c= S . (n + k) ; :: thesis: S_{1}[k + 1]

S . (n + k) c= S . ((n + k) + 1) by A1;

hence S_{1}[k + 1]
by A5, XBOOLE_1:1; :: thesis: verum

end;assume A5: S . n c= S . (n + k) ; :: thesis: S

S . (n + k) c= S . ((n + k) + 1) by A1;

hence S

thus for k being Nat holds S

A7: m = n + k by A2, NAT_1:10;

thus S . n c= S . m by A3, A7; :: thesis: verum