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 )