theorem :: PROB_2:7

for X being set
for S being SetSequence of X holds
( S is non-descending iff for n being Nat holds S . n c= S . (n + 1) )