defpred S₁[ object ] means ( $1 in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & $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 ) ) );
for X1, X2 being set st ( for x being object holds
( x in X1 iff S₁[x] ) ) & ( for x being object holds
( x in X2 iff S₁[x] ) ) holds
X1 = X2 from XBOOLE_0:sch 3();
hence for b₁, b₂ being set st ( for x being object holds
( x in b₁ 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 ) ) ) ) ) & ( for x being object holds
( x in b₂ 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 ) ) ) ) ) holds
b₁ = b₂ ; :: thesis: verum