defpred S_{1}[ 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 ) );

for X1, X2 being set st ( for x being object holds

( x in X1 iff S_{1}[x] ) ) & ( for x being object holds

( x in X2 iff S_{1}[x] ) ) holds

X1 = X2 from XBOOLE_0:sch 3();

hence for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} 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 ) ) ) ) & ( for x being object holds

( x in b_{2} 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 ) ) ) ) holds

b_{1} = b_{2}
; :: thesis: verum

B is opers_closed ) );

for X1, X2 being set st ( for x being object holds

( x in X1 iff S

( x in X2 iff S

X1 = X2 from XBOOLE_0:sch 3();

hence for b

( x in b

B is opers_closed ) ) ) ) & ( for x being object holds

( x in b

B is opers_closed ) ) ) ) holds

b