let a, b be Real; :: thesis: ( (a ^2) + (b ^2) is negative implies ( a = 0 & b = 0 ) )
assume A1: (a ^2) + (b ^2) is negative ; :: thesis: ( a = 0 & b = 0 )
( 0 <= a * a & 0 <= b * b ) by XREAL_1:63;
hence ( a = 0 & b = 0 ) by A1; :: thesis: verum