defpred S₁[ set , set ] means ex s being 1-sorted st
( s = $1 & $2 = the carrier of s );
A1: for x, y, z being set st S₁[x,y] & S₁[x,z] holds
y = z ;
consider CX being set such that
A2: for x being set holds
( x in CX iff ex y being set st
( y in X & S₁[y,x] ) ) from TARSKI:sch 1(A1);
take CX ; :: thesis: for a being set holds
( a in CX iff ex s being 1-sorted st
( s in X & a = the carrier of s ) )
let x be set ; :: thesis: ( x in CX iff ex s being 1-sorted st
( s in X & x = the carrier of s ) )
( x in CX iff ex s being 1-sorted st
( s in X & x = the carrier of s ) )

proof

thus ( x in CX implies ex s being 1-sorted st
( s in X & x = the carrier of s ) ) :: thesis: ( ex s being 1-sorted st
( s in X & x = the carrier of s ) implies x in CX )

proof

assume x in CX ; :: thesis: ex s being 1-sorted st
( s in X & x = the carrier of s )
then consider y being set such that
A3: y in X and
A4: ex s being 1-sorted st
( s = y & x = the carrier of s ) by A2;
consider s being 1-sorted such that
A5: s = y and
x = the carrier of s by A4;
take s ; :: thesis: ( s in X & x = the carrier of s )
thus ( s in X & x = the carrier of s ) by A3, A4, A5; :: thesis: verum

end;

given s being 1-sorted such that A6: ( s in X & x = the carrier of s ) ; :: thesis: x in CX
thus x in CX by A2, A6; :: thesis: verum

end;

hence ( x in CX iff ex s being 1-sorted st
( s in X & x = the carrier of s ) ) ; :: thesis: verum