for Omega being set
for ASeq being SetSequence of Omega holds
( ASeq is non-ascending iff Complement ASeq is non-descending )