theorem :: PROB_2:6

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