let A be complex-membered set ; :: thesis: for a being Complex holds
( a in A iff a " in A "" )
let a be Complex; :: thesis: ( a in A iff a " in A "" )
thus ( 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 Complex st
( c " = a " & c in A ) ;
hence a in A by XCMPLX_1:201; :: thesis: verum