defpred S₁[ set ] means ( $1 is MSSubset of U0 & ( for B being MSSubset of U0 st B = $1 holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in Funcs the carrier of S,(bool (Union the Sorts of U0)) & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being set holds
( x in X iff ( x in Funcs the carrier of S,(bool (Union the Sorts of U0)) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) )
thus for x being set holds
( x in X iff ( x in Funcs the carrier of S,(bool (Union the Sorts of U0)) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) by A1; :: thesis: verum