theorem Th24: :: SETLIM_1:24

for X being set
for B being SetSequence of X holds superior_setsequence B is non-ascending