theorem :: ANPROJ11:53

for P, Q being Point of real_projective_plane
for P9, Q9 being Element of (ProjectiveSpace (TOP-REAL 3)) st P = P9 & Q = Q9 holds
Line (P,Q) = Line (P9,Q9) ;