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

proof

assume A1: S is non-ascending ; :: thesis: for i being Element of NAT holds S . (i + 1) c= S . i
let i be Element of 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 6; :: thesis: verum

end;

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