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 non-descending & rng A1 c= bool X holds
Union A1 in bool X ;
hence bool X is non-decreasing-closed by Def12; :: thesis: bool X is non-increasing-closed
for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= bool X holds
Intersection A1 in bool X ;
hence bool X is non-increasing-closed by Def13; :: thesis: verum