theorem Th56: :: BKMODEL4:66

for P, Q, P1, P2 being non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)) st P <> Q & P in BK_model & Q in BK_model & P1 in absolute & P2 in absolute & P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & not between RP3_to_T2 Q, RP3_to_T2 P, RP3_to_T2 P1 holds
between RP3_to_T2 Q, RP3_to_T2 P, RP3_to_T2 P2