set C = bool (Union the Sorts of U0);
defpred S₁[ set ] means ex B being MSSubset of U0 st
( B in SubSort A & $1 = B . s );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool (Union the Sorts of U0) & S₁[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 set holds
( x in X iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) )

proof

let x be set ; :: 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 A4: ( B in SubSort A & x = B . s ) ; :: thesis: x in X
( dom the Sorts of U0 = the carrier of S & dom B = the carrier of S ) by PARTFUN1:def 4;
then the Sorts of U0 . s in rng the Sorts of U0 by FUNCT_1:def 5;
then A5: the Sorts of U0 . s c= union (rng the Sorts of U0) by ZFMISC_1:92;
B c= the Sorts of U0 by PBOOLE:def 23;
then B . s c= the Sorts of U0 . s by PBOOLE:def 5;
then x c= union (rng the Sorts of U0) by A4, A5, XBOOLE_1:1;
hence x in X by A1, A2, A4; :: thesis: verum

end;

take X ; :: thesis: for x being set holds
( x in X iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) )
thus for x being set holds
( x in X iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) by A3; :: thesis: verum