defpred S₁[ object ] means ex B being OSSubset of OU0 st
( B in OSSubSort A & $1 = B . s );
set C = bool (Union the Sorts of OU0);
consider X being set such that
A1: for x being object holds
( x in X iff ( x in bool (Union the Sorts of OU0) & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being object holds
( x in X iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) )
A2: bool (Union the Sorts of OU0) = bool (union (rng the Sorts of OU0)) by CARD_3:def 4;
for x being set holds
( x in X iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) )

proof

dom the Sorts of OU0 = the carrier of S1 by PARTFUN1:def 2;
then the Sorts of OU0 . s in rng the Sorts of OU0 by FUNCT_1:def 3;
then A3: the Sorts of OU0 . s c= union (rng the Sorts of OU0) by ZFMISC_1:74;
let x be set ; :: thesis: ( x in X iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) )
thus ( x in X implies ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) ) by A1; :: thesis: ( ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) implies x in X )
given B being OSSubset of OU0 such that A4: B in OSSubSort A and
A5: x = B . s ; :: thesis: x in X
B c= the Sorts of OU0 by PBOOLE:def 18;
then B . s c= the Sorts of OU0 . s ;
then x c= union (rng the Sorts of OU0) by A5, A3;
hence x in X by A2, A1, A4, A5; :: thesis: verum

end;

hence for x being object holds
( x in X iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) ) ; :: thesis: verum