theorem Th13: :: BKMODEL2:21

for P, Q, R being Element of real_projective_plane
for u, v, w being non zero Element of (TOP-REAL 3)
for a, b, c, d being Real st P in BK_model & Q in absolute & P = Dir u & Q = Dir v & R = Dir w & u = |[a,b,1]| & v = |[c,d,1]| & w = |[((a + c) / 2),((b + d) / 2),1]| holds
( R in BK_model & R <> P & P,R,Q are_collinear )