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