let A, B be complex-membered set ; :: thesis: ( A = { (c " ) where c is Element of COMPLEX : c in B } implies B = { (c " ) where c is Element of COMPLEX : c in A } )
assume A1: A = { (c " ) where c is Element of COMPLEX : c in B } ; :: thesis: B = { (c " ) where c is Element of COMPLEX : c in A }
thus B c= { (c " ) where c is Element of COMPLEX : c in A } :: according to XBOOLE_0:def 10 :: thesis: { (c " ) where c is Element of COMPLEX : c in A } c= B

proof

let z be complex number ; :: according to MEMBERED:def 7 :: thesis: ( not z in B or z in { (c " ) where c is Element of COMPLEX : c in A } )
assume A2: z in B ; :: thesis: z in { (c " ) where c is Element of COMPLEX : c in A }
A3: z in COMPLEX by XCMPLX_0:def 2;
A4: z " in COMPLEX by XCMPLX_0:def 2;
A5: z = (z " ) " ;
z " in A by A1, A2, A3;
hence z in { (c " ) where c is Element of COMPLEX : c in A } by A5, A4; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (c " ) where c is Element of COMPLEX : c in A } or e in B )
assume e in { (c " ) where c is Element of COMPLEX : c in A } ; :: thesis: e in B
then consider r0 being Element of COMPLEX such that
A6: r0 " = e and
A7: r0 in A ;
ex c being Element of COMPLEX st
( c " = r0 & c in B ) by A1, A7;
hence e in B by A6; :: thesis: verum