let A be complex-membered set ; :: thesis: for a being complex number holds
( a in A iff a " in A "" )
let a be complex number ; :: thesis: ( a in A iff a " in A "" )
a in COMPLEX by XCMPLX_0:def 2;
hence ( a in A implies a " in A "" ) ; :: thesis: ( a " in A "" implies a in A )
assume a " in A "" ; :: thesis: a in A
then ex c being Element of COMPLEX st
( c " = a " & c in A ) ;
hence a in A by XCMPLX_1:202; :: thesis: verum