theorem :: BKMODEL1:8

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