let X be set ; :: thesis: for S being SetSequence of X holds
( S is non-ascending iff for n being Nat holds S . (n + 1) c= S . n )
let S be SetSequence of X; :: thesis: ( S is non-ascending iff for n being Nat holds S . (n + 1) c= S . n )
thus ( S is non-ascending implies for n being Nat holds S . (n + 1) c= S . n ) by NAT_1:11; :: thesis: ( ( for n being Nat holds S . (n + 1) c= S . n ) implies S is non-ascending )
assume A1: for n being Nat holds S . (n + 1) c= S . n ; :: thesis: S is non-ascending

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

let n, m be Nat; :: thesis: ( n <= m implies S . m c= S . n )
assume A2: n <= m ; :: thesis: S . m c= S . n

A3: now :: thesis: for k being Nat holds S₁[k]

defpred S₁[ Nat] means S . (n + $1) c= S . n;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S . (n + k) c= S . n ; :: thesis: S₁[k + 1]
S . ((n + k) + 1) c= S . (n + k) by A1;
hence S₁[k + 1] by A5, XBOOLE_1:1; :: thesis: verum

end;

A6: S₁[ 0 ] ;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A6, A4); :: thesis: verum

end;

consider k being Nat such that
A7: m = n + k by A2, NAT_1:10;
thus S . m c= S . n by A3, A7; :: thesis: verum

end;

hence S is non-ascending ; :: thesis: verum