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 ") " = a ;
hence ( a " in A iff a in A "" ) by Th28; :: thesis: verum