let a, b, c be Element of (OASpace (TOP-REAL 2)); for ap, bp, cp being POINT of TarskiEuclid2Space st a = ap & b = bp & c = cp holds
( Mid a,b,c iff between ap,bp,cp )
let ap, bp, cp be POINT of TarskiEuclid2Space; ( a = ap & b = bp & c = cp implies ( Mid a,b,c iff between ap,bp,cp ) )
assume that
A1:
a = ap
and
A2:
b = bp
and
A3:
c = cp
; ( Mid a,b,c iff between ap,bp,cp )
hereby ( between ap,bp,cp implies Mid a,b,c )
assume
Mid a,
b,
c
;
between ap,bp,cpthen
ex
u,
v being
Point of
(TOP-REAL 2) st
(
u = a &
v = c &
b in LSeg (
u,
v) )
by THSS2;
then
Tn2TR bp in LSeg (
(Tn2TR ap),
(Tn2TR cp))
by A1, A2, A3;
hence
between ap,
bp,
cp
by ThConv6;
verum
end;
assume
between ap,bp,cp
; Mid a,b,c
then
Tn2TR bp in LSeg ((Tn2TR ap),(Tn2TR cp))
by ThConv6;
hence
Mid a,b,c
by A1, A2, A3, THSS2; verum