reconsider b = a * (a *') as Real ;
not b |^ (2 * 1) is negative ;
hence not (a * (a *')) |^ 2 is negative ; :: thesis: verum