let A be complex-membered set ; :: thesis: -- (A "" ) = (-- A) ""
let a be complex number ; :: according to MEMBERED:def 13 :: thesis: ( ( not a in -- (A "" ) or a in (-- A) "" ) & ( not a in (-- A) "" or a in -- (A "" ) ) )
A1: (- a) " = - (a " ) by XCMPLX_1:224;

hereby :: thesis: ( not a in (-- A) "" or a in -- (A "" ) )

assume a in -- (A "" ) ; :: thesis: a in (-- A) ""
then - a in A "" by Th18;
then (- a) " in A by Th35;
then a " in -- A by A1, Th18;
hence a in (-- A) "" by Th35; :: thesis: verum

end;

assume a in (-- A) "" ; :: thesis: a in -- (A "" )
then a " in -- A by Th35;
then - (a " ) in A by Th18;
then - a in A "" by A1, Th35;
hence a in -- (A "" ) by Th18; :: thesis: verum