theorem :: BKMODEL1:3

for a, b, c being Real st (a ^2) + (b ^2) = 1 & ((c * a) ^2) + ((c * b) ^2) = 1 & not c = 1 holds
c = - 1