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

proof

let z be Complex; :: according to MEMBERED:def 7 :: thesis: ( not z in B or z in { (- c) where c is Complex : c in A } )
A2: ( - z in COMPLEX & z = - (- z) ) by XCMPLX_0:def 2;
assume z in B ; :: thesis: z in { (- c) where c is Complex : c in A }
then - z in A by A1;
hence z in { (- c) where c is Complex : c in A } by A2; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (- c) where c is Complex : c in A } or e in B )
assume e in { (- c) where c is Complex : c in A } ; :: thesis: e in B
then consider r0 being Complex such that
A3: - r0 = e and
A4: r0 in A ;
ex c being Complex st
( - c = r0 & c in B ) by A1, A4;
hence e in B by A3; :: thesis: verum