let A, B, P, Q, Z be POINT of BK-model-Plane; :: according to GTARSKI1:def 11 :: thesis: ( not between A,P,Z or not between B,Q,Z or ex b₁ being Element of the carrier of BK-model-Plane st
( between P,b₁,B & between Q,b₁,A ) )
assume that
A1: between A,P,Z and
A2: between B,Q,Z ; :: thesis: ex b₁ being Element of the carrier of BK-model-Plane st
( between P,b₁,B & between Q,b₁,A )
reconsider a = A, b = B, p = P, q = Q, z = Z as Element of BK_model ;
reconsider A2 = BK_to_T2 A, B2 = BK_to_T2 B, P2 = BK_to_T2 P, Q2 = BK_to_T2 Q, Z2 = BK_to_T2 Z as POINT of TarskiEuclid2Space ;
( between A2,P2,Z2 & between B2,Q2,Z2 ) by A1, A2, Th05;
then consider X2 being POINT of TarskiEuclid2Space such that
A3: between P2,X2,B2 and
A4: between Q2,X2,A2 by GTARSKI1:def 11;
reconsider X = T2_to_BK X2 as POINT of BK-model-Plane ;
A5: Tn2TR X2 in LSeg ((Tn2TR P2),(Tn2TR B2)) by A3, GTARSKI2:20;
set P9 = Tn2TR P2;
set B9 = Tn2TR B2;
( Tn2TR P2 in inside_of_circle (0,0,1) & Tn2TR B2 in inside_of_circle (0,0,1) ) by Th02;
then Tn2TR X2 is Element of inside_of_circle (0,0,1) by A5, Th15;
then X2 = BK_to_T2 X by Th03;
then ( between P,X,B & between Q,X,A ) by A3, A4, Th05;
hence ex b₁ being Element of the carrier of BK-model-Plane st
( between P,b₁,B & between Q,b₁,A ) ; :: thesis: verum