let a, b be non zero Real; :: thesis: |.((a |^ 2) - (b |^ 2)).| < |.((a |^ 2) + (b |^ 2)).|
reconsider c = a |^ (2 * 1) as positive Real ;
reconsider d = b |^ (2 * 1) as positive Real ;
c * d > 0 ;
hence |.((a |^ 2) - (b |^ 2)).| < |.((a |^ 2) + (b |^ 2)).| by MP; :: thesis: verum