set f = Funcs the carrier of S,(bool (Union the Sorts of U0));
defpred S₁[ set ] 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 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();
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 4, ZFMISC_1:100;
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 Th4, PBOOLE:def 23;
then reconsider X = X as non empty set by A1, A2;
SubSort U0 = X by A1, Def12;
hence not SubSort U0 is empty ; :: thesis: verum