let P, Q be POINT of BK-model-Plane; :: according to GTARSKI1:def 10 :: thesis: ( not between P,Q,P or P = Q )
assume A1: between P,Q,P ; :: thesis: P = Q
reconsider P2 = BK_to_T2 P, Q2 = BK_to_T2 Q as POINT of TarskiEuclid2Space ;
between P2,Q2,P2 by A1, Th05;
hence P = Q by GTARSKI1:def 10, Th65; :: thesis: verum