let a, b, c be Element of (OASpace (TOP-REAL 2)); :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( Mid a,b,c iff between ap,bp,cp )
hereby :: thesis: ( between ap,bp,cp implies Mid a,b,c )
assume Mid a,b,c ; :: thesis: between ap,bp,cp
then 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; :: thesis: verum
end;
assume between ap,bp,cp ; :: thesis: 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; :: thesis: verum