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

proof

assume A2: S is non-descending ; :: thesis: for i being Element of NAT holds S . i c= S . (i + 1)
let i be Element of NAT ; :: thesis: S . i c= S . (i + 1)
i <= i + 1 by NAT_1:13;
hence S . i c= S . (i + 1) by A2, PROB_1:def 7; :: thesis: verum

end;

assume for i being Element of NAT holds S . i c= S . (i + 1) ; :: thesis: S is non-descending
then for i, j being Element of NAT st i <= j holds
S . i c= S . j by MEASURE2:22;
hence S is non-descending by PROB_1:def 7; :: thesis: verum