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