let A be complex-membered set ; :: thesis: -- (A "") = (-- A) ""
let a be Complex; :: 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:222;
hereby :: thesis: ( not a in (-- A) "" or a in -- (A "") )
assume a in -- (A "") ; :: thesis: a in (-- A) ""
then - a in A "" by Th12;
then (- a) " in A by Th29;
then a " in -- A by A1, Th12;
hence a in (-- A) "" by Th29; :: thesis: verum
end;
assume a in (-- A) "" ; :: thesis: a in -- (A "")
then a " in -- A by Th29;
then - (a ") in A by Th12;
then - a in A "" by A1, Th29;
hence a in -- (A "") by Th12; :: thesis: verum