assume A1: A = F ; :: thesis: A "" = F ""
let a be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not a in A "" or a in F "" ) & ( not a in F "" or a in A "" ) )
hereby :: thesis: ( not a in F "" or a in A "" )
assume a in A "" ; :: thesis: a in F ""
then consider c being Complex such that
A2: a = c " and
A3: c in A ;
reconsider w = c as Element of ExtREAL by A3, XXREAL_0:def 1;
ex m being Complex st
( w = m & w " = m " ) by A3, XXREAL_3:def 6;
hence a in F "" by A1, A2, A3; :: thesis: verum
end;
assume a in F "" ; :: thesis: a in A ""
then consider w being Element of ExtREAL such that
A4: a = w " and
A5: w in F ;
reconsider c = w as Element of COMPLEX by A1, A5, XCMPLX_0:def 2;
w " = c " by A1, A5, XXREAL_3:def 6;
hence a in A "" by A1, A4, A5; :: thesis: verum