let P, Q, R be Point of BK-model-Plane; :: thesis: for P2, Q2, R2 being POINT of TarskiEuclid2Space st P2 = BK_to_T2 P & Q2 = BK_to_T2 Q & R2 = BK_to_T2 R holds
( between P,Q,R iff between P2,Q2,R2 )
let P2, Q2, R2 be POINT of TarskiEuclid2Space; :: thesis: ( P2 = BK_to_T2 P & Q2 = BK_to_T2 Q & R2 = BK_to_T2 R implies ( between P,Q,R iff between P2,Q2,R2 ) )
assume that
A1: P2 = BK_to_T2 P and
A2: Q2 = BK_to_T2 Q and
A3: R2 = BK_to_T2 R ; :: thesis: ( between P,Q,R iff between P2,Q2,R2 )
reconsider p = P, q = Q, r = R as Element of BK_model ;
A4: ( Tn2TR (BK_to_T2 P) = BK_to_REAL2 p & Tn2TR (BK_to_T2 Q) = BK_to_REAL2 q & Tn2TR (BK_to_T2 R) = BK_to_REAL2 r ) by Th04;
hereby :: thesis: ( between P2,Q2,R2 implies between P,Q,R )
assume between P,Q,R ; :: thesis: between P2,Q2,R2
then BK_to_REAL2 q in LSeg ((BK_to_REAL2 p),(BK_to_REAL2 r)) by BKMODEL3:def 7;
hence between P2,Q2,R2 by A4, A1, A2, A3, GTARSKI2:20; :: thesis: verum
end;
assume between P2,Q2,R2 ; :: thesis: between P,Q,R
then Tn2TR (BK_to_T2 Q) in LSeg ((Tn2TR (BK_to_T2 P)),(Tn2TR (BK_to_T2 R))) by A1, A2, A3, GTARSKI2:20;
hence between P,Q,R by A4, BKMODEL3:def 7; :: thesis: verum