defpred S_{1}[ object , object ] means ex s being 1-sorted st

( s = $1 & $2 = the carrier of s );

A1: for x, y, z being object st S_{1}[x,y] & S_{1}[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 & S_{1}[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 ) )

( s in X & x = the carrier of s ) ) ; :: thesis: verum

( s = $1 & $2 = the carrier of s );

A1: for x, y, z being object st S

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 & S

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

hence
( x in CX iff ex s being 1-sorted st
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 )

thus x in CX by A2, A6; :: thesis: verum

end;( 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

given s being 1-sorted such that A6:
( s in X & x = the carrier of s )
; :: thesis: x in CX
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;( 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

thus x in CX by A2, A6; :: thesis: verum

( s in X & x = the carrier of s ) ) ; :: thesis: verum