let P, Q, R be Point of BK-model-Plane; 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; ( 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
; ( 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 ( between P2,Q2,R2 implies between P,Q,R )
assume
between P,
Q,
R
;
between P2,Q2,R2then
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;
verum
end;
assume
between P2,Q2,R2
; 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; verum