for P, Q, R being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3))
for u, v, w being non zero Element of (TOP-REAL 3) st P in absolute & Q in absolute & P <> Q & P = Dir u & Q = Dir v & R = Dir w & u `3 = 1 & v `3 = 1 & w = |[(((u `1) + (v `1)) / 2),(((u `2) + (v `2)) / 2),1]| holds
R in BK_model