reconsider u0 = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;

defpred S_{1}[ object ] means ex B being MSSubset of U0 st

( B in SubSort A & S = B . s );

set C = bool (Union the Sorts of U0);

consider X being set such that

A1: for x being object holds

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

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

A3: for x being object holds

( x in X iff ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) )

u0 is opers_closed by Th3;

then u0 in SubSort A by A7, Th13;

then the Sorts of U0 . s in X by A3;

then reconsider X = X as non empty set ;

X = SubSort (A,s) by A3, Def13;

hence not SubSort (A,s) is empty ; :: thesis: verum

defpred S

( B in SubSort A & S = B . s );

set C = bool (Union the Sorts of U0);

consider X being set such that

A1: for x being object holds

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

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

A3: for x being object holds

( x in X iff ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) )

proof

A7:
( A c= u0 & Constants U0 c= u0 )
by PBOOLE:def 18;
dom the Sorts of U0 = the carrier of S
by PARTFUN1:def 2;

then the Sorts of U0 . s in rng the Sorts of U0 by FUNCT_1:def 3;

then A4: the Sorts of U0 . s c= union (rng the Sorts of U0) by ZFMISC_1:74;

let x be object ; :: thesis: ( x in X iff ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) )

thus ( x in X implies ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) ) by A1; :: thesis: ( ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) implies x in X )

given B being MSSubset of U0 such that A5: B in SubSort A and

A6: x = B . s ; :: thesis: x in X

reconsider x = x as set by TARSKI:1;

B c= the Sorts of U0 by PBOOLE:def 18;

then B . s c= the Sorts of U0 . s ;

then x c= union (rng the Sorts of U0) by A6, A4;

hence x in X by A1, A2, A5, A6; :: thesis: verum

end;then the Sorts of U0 . s in rng the Sorts of U0 by FUNCT_1:def 3;

then A4: the Sorts of U0 . s c= union (rng the Sorts of U0) by ZFMISC_1:74;

let x be object ; :: thesis: ( x in X iff ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) )

thus ( x in X implies ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) ) by A1; :: thesis: ( ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) implies x in X )

given B being MSSubset of U0 such that A5: B in SubSort A and

A6: x = B . s ; :: thesis: x in X

reconsider x = x as set by TARSKI:1;

B c= the Sorts of U0 by PBOOLE:def 18;

then B . s c= the Sorts of U0 . s ;

then x c= union (rng the Sorts of U0) by A6, A4;

hence x in X by A1, A2, A5, A6; :: thesis: verum

u0 is opers_closed by Th3;

then u0 in SubSort A by A7, Th13;

then the Sorts of U0 . s in X by A3;

then reconsider X = X as non empty set ;

X = SubSort (A,s) by A3, Def13;

hence not SubSort (A,s) is empty ; :: thesis: verum