theorem :: BKMODEL1:19

for a, b being Real st (a ^2) + (b ^2) is negative holds
( a = 0 & b = 0 )