theorem Th17: :: BKMODEL2:25

for P being Element of BK_model
for u being non zero Element of (TOP-REAL 3) st P = Dir u & u . 3 = 1 holds
((u . 1) ^2) + ((u . 2) ^2) < 1