let P, Q, P1, P2 be non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)); ( 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 implies between RP3_to_T2 Q, RP3_to_T2 P, RP3_to_T2 P2 )
assume that
A1:
P <> Q
and
A2:
P in BK_model
and
A3:
Q in BK_model
and
A4:
P1 in absolute
and
A5:
P2 in absolute
and
A6:
P1 <> P2
and
A7:
P,Q,P1 are_collinear
and
A8:
P,Q,P2 are_collinear
; ( between RP3_to_T2 Q, RP3_to_T2 P, RP3_to_T2 P1 or between RP3_to_T2 Q, RP3_to_T2 P, RP3_to_T2 P2 )
set P9 = RP3_to_T2 P;
set Q9 = RP3_to_T2 Q;
set P19 = RP3_to_T2 P1;
set P29 = RP3_to_T2 P2;
( Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 P1 & Collinear RP3_to_T2 P, RP3_to_T2 Q, RP3_to_T2 P2 & not between RP3_to_T2 Q, RP3_to_T2 P1, RP3_to_T2 P & not between RP3_to_T2 Q, RP3_to_T2 P2, RP3_to_T2 P )
by A2, A3, A4, A5, A7, A8, Th47, Th46;
hence
( between RP3_to_T2 Q, RP3_to_T2 P, RP3_to_T2 P1 or between RP3_to_T2 Q, RP3_to_T2 P, RP3_to_T2 P2 )
by A1, A2, A4, A5, A6, Th55, GTARSKI1:16; verum