defpred S1[ object , object ] means ex s being 1-sorted st
( s = \$1 & \$2 = the carrier of s );
A1: for x, y, z being object st S1[x,y] & S1[x,z] holds
y = z ;
consider CX being set such that
A2: for x being object holds
( x in CX iff ex y being object st
( y in X & S1[y,x] ) ) from 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 object 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