:: deftheorem defines non-ascending KURATO_0:def 3 :
for T being set
for S being SetSequence of T holds
( S is non-ascending iff for i being Nat holds S . (i + 1) c= S . i );