let C1, C2 be set ; :: thesis: ( ( for a being set holds
( a in C1 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) ) & ( for a being set holds
( a in C2 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) ) implies C1 = C2 )
assume that
A7: for a being set holds
( a in C1 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) and
A8: for a being set holds
( a in C2 iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) ; :: thesis: C1 = C2
for a being set holds
( a in C1 iff a in C2 )

proof

let a be set ; :: thesis: ( a in C1 iff a in C2 )
thus ( a in C1 implies a in C2 ) :: thesis: ( a in C2 implies a in C1 )

proof

assume a in C1 ; :: thesis: a in C2
then ex s being 1-sorted st
( s in X & a = the carrier of s ) by A7;
hence a in C2 by A8; :: thesis: verum

end;

thus ( a in C2 implies a in C1 ) :: thesis: verum

proof

assume a in C2 ; :: thesis: a in C1
then ex s being 1-sorted st
( s in X & a = the carrier of s ) by A8;
hence a in C1 by A7; :: thesis: verum

end;

end;

hence C1 = C2 by TARSKI:2; :: thesis: verum