theorem :: SETLIM_1:25

for X being set
for B being SetSequence of X holds
( inferior_setsequence B is monotone & superior_setsequence B is monotone ) by Th23, Th24;