theorem Th70: :: BKMODEL1:88

for u being Element of (TOP-REAL 3) st qfconic (1,1,(- 1),0,0,0,u) = 0 & u . 3 = 1 holds
|[(u . 1),(u . 2)]| in Sphere ((0. (TOP-REAL 2)),1)