let P, Q be Point of BK-model-Plane; :: thesis: ( between P,P,Q & between P,Q,Q )
reconsider P2 = BK_to_T2 P, Q2 = BK_to_T2 Q as Point of TarskiEuclid2Space ;
between P2,P2,Q2 by GTARSKI1:17;
hence between P,P,Q by Th05; :: thesis: between P,Q,Q
between P2,Q2,Q2 by GTARSKI1:14;
hence between P,Q,Q by Th05; :: thesis: verum