set f = Funcs ( the carrier of S,(bool (Union the Sorts of U0)));

defpred S_{1}[ object ] means ( S is MSSubset of U0 & ( for B being MSSubset of U0 st B = S holds

B is opers_closed ) );

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();

Union the Sorts of U0 = union (rng the Sorts of U0) by CARD_3:def 4;

then ( dom the Sorts of U0 = the carrier of S & rng the Sorts of U0 c= bool (Union the Sorts of U0) ) by PARTFUN1:def 2, ZFMISC_1:82;

then A2: the Sorts of U0 in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by FUNCT_2:def 2;

( the Sorts of U0 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of U0 holds

B is opers_closed ) ) by Th3, PBOOLE:def 18;

then reconsider X = X as non empty set by A1, A2;

SubSort U0 = X by A1, Def11;

hence not SubSort U0 is empty ; :: thesis: verum

defpred S

B is opers_closed ) );

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

Union the Sorts of U0 = union (rng the Sorts of U0) by CARD_3:def 4;

then ( dom the Sorts of U0 = the carrier of S & rng the Sorts of U0 c= bool (Union the Sorts of U0) ) by PARTFUN1:def 2, ZFMISC_1:82;

then A2: the Sorts of U0 in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) by FUNCT_2:def 2;

( the Sorts of U0 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of U0 holds

B is opers_closed ) ) by Th3, PBOOLE:def 18;

then reconsider X = X as non empty set by A1, A2;

SubSort U0 = X by A1, Def11;

hence not SubSort U0 is empty ; :: thesis: verum