theorem Th46: :: BKMODEL4:53

for P, Q, R being non point_at_infty Point of (ProjectiveSpace (TOP-REAL 3)) holds
( P,Q,R are_collinear iff Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 R )