theorem Th17: :: BKMODEL4:27

for R being Element of (ProjectiveSpace (TOP-REAL 3))
for P, Q being Element of BK_model
for u, v, w being non zero Element of (TOP-REAL 3)
for r being Real st 0 <= r & r <= 1 & P = Dir u & Q = Dir v & R = Dir w & u . 3 = 1 & v . 3 = 1 & w = (r * u) + ((1 - r) * v) holds
R is Element of BK_model