theorem :: BKMODEL1:77

for R being POINT of (IncProjSp_of real_projective_plane)
for L being LINE of (IncProjSp_of real_projective_plane)
for p, q being Point of real_projective_plane
for u, v, w being non zero Element of (TOP-REAL 3) st p = Dir u & q = Dir v & R = Dir w & L = Line (p,q) holds
( R on L iff |{u,v,w}| = 0 )