let a, b be complex number ; :: thesis: ( a " = b " implies a = b )
assume a " = b " ; :: thesis: a = b
then a = (b " ) " ;
hence a = b ; :: thesis: verum