theorem Th23: :: SETLIM_1:23

for X being set
for B being SetSequence of X holds inferior_setsequence B is non-descending