theorem Th61: :: BKMODEL1:74

for R being POINT of (IncProjSp_of real_projective_plane)
for L being LINE of (IncProjSp_of real_projective_plane)
for p, q, r being Point of real_projective_plane st R = r & L = Line (p,q) holds
( R on L iff p,q,r are_collinear )