for P1, P2 being Element of absolute
for Q being Element of BK_model
for u, v, w being non zero Element of (TOP-REAL 3) st Dir u = P1 & Dir v = P2 & Dir w = Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 1 & v . 1 = - (u . 1) & v . 2 = - (u . 2) & P1,Q,P2 are_collinear holds
ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) )