defpred S_{1}[ object ] 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 object holds

( x in X iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & S_{1}[x] ) )
from XBOOLE_0:sch 1();

take X ; :: thesis: for x being object 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 object 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

( B is opers_closed & Constants U0 c= B & A c= B ) ) );

consider X being set such that

A1: for x being object holds

( x in X iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & S

take X ; :: thesis: for x being object 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 object 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