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 object holds

( a in C1 iff a in C2 )

( 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 object holds

( a in C1 iff a in C2 )

proof

hence
C1 = C2
by TARSKI:2; :: thesis: verum
let a be object ; :: thesis: ( a in C1 iff a in C2 )

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

end;thus ( a in C1 implies a in C2 ) :: thesis: ( a in C2 implies a in C1 )

proof

thus
( a in C2 implies a in C1 )
:: thesis: verum
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;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

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