let X be set ; :: thesis: ( bool X is non-decreasing-closed & bool X is non-increasing-closed )
for A1 being SetSequence of X st A1 is V71() & rng A1 c= bool X holds
Union A1 in bool X ;
hence bool X is non-decreasing-closed by Def9; :: thesis: bool X is non-increasing-closed
for A1 being SetSequence of X st A1 is V70() & rng A1 c= bool X holds
Intersection A1 in bool X ;
hence bool X is non-increasing-closed by Def10; :: thesis: verum