theorem Th8: :: PROB_2:8

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