theorem Th24: :: BKMODEL3:29

for u, v, w being non zero Element of (TOP-REAL 3) st u `2 <> 0 & u `3 = 1 & v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) holds
((w `1) ^2) + ((w `2) ^2) <> 1