let X be set ; :: thesis: for B being SetSequence of X holds
( inferior_setsequence B is monotone & superior_setsequence B is monotone )
let B be SetSequence of X; :: thesis: ( inferior_setsequence B is monotone & superior_setsequence B is monotone )
inferior_setsequence B is non-descending by Th23;
hence inferior_setsequence B is monotone by Def1; :: thesis: superior_setsequence B is monotone
superior_setsequence B is non-ascending by Th24;
hence superior_setsequence B is monotone by Def1; :: thesis: verum