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