thus ( S is non-ascending implies for i being Nat holds S . (i + 1) c= S . i ) :: thesis: ( ( for i being Nat holds S . (i + 1) c= S . i ) implies S is non-ascending )

proof

assume A1: S is non-ascending ; :: thesis: for i being Nat holds S . (i + 1) c= S . i
let i be Nat; :: thesis: S . (i + 1) c= S . i
i <= i + 1 by NAT_1:13;
hence S . (i + 1) c= S . i by A1, PROB_1:def 4; :: thesis: verum

end;

assume for i being Nat holds S . (i + 1) c= S . i ; :: thesis: S is non-ascending
then A2: for i, j being Nat st i <= j holds
S . j c= S . i by Th18;
for i, j being Nat st i <= j holds
S . j c= S . i by A2;
hence S is non-ascending by PROB_1:def 4; :: thesis: verum