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

proof

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

end;

assume for i being Nat holds S . i c= S . (i + 1) ; :: thesis: S is non-descending
then A4: for i, j being Nat st i <= j holds
S . i c= S . j by MEASURE2:18;
for i, j being Nat st i <= j holds
S . i c= S . j by A4;
hence S is non-descending by PROB_1:def 5; :: thesis: verum