let a, b, c, p, q be Point of TarskiEuclid2Space; ( p <> q & a,p equiv a,q & b,p equiv b,q & c,p equiv c,q & not between a,b,c & not between b,c,a implies between c,a,b )
assume that
A1:
p <> q
and
A2:
a,p equiv a,q
and
A3:
b,p equiv b,q
and
A4:
c,p equiv c,q
; ( between a,b,c or between b,c,a or between c,a,b )
|.((Tn2TR a) - (Tn2TR p)).| = |.((Tn2TR a) - (Tn2TR q)).|
by A2, ThConv4;
then A5:
Tn2TR a in the_perpendicular_bisector ((Tn2TR p),(Tn2TR q))
by A1, EUCLID12:60;
|.((Tn2TR b) - (Tn2TR p)).| = |.((Tn2TR b) - (Tn2TR q)).|
by A3, ThConv4;
then A6:
Tn2TR b in the_perpendicular_bisector ((Tn2TR p),(Tn2TR q))
by A1, EUCLID12:60;
|.((Tn2TR c) - (Tn2TR p)).| = |.((Tn2TR c) - (Tn2TR q)).|
by A4, ThConv4;
then
Tn2TR c in the_perpendicular_bisector ((Tn2TR p),(Tn2TR q))
by A1, EUCLID12:60;
then
( Tn2TR a in LSeg ((Tn2TR b),(Tn2TR c)) or Tn2TR b in LSeg ((Tn2TR c),(Tn2TR a)) or Tn2TR c in LSeg ((Tn2TR a),(Tn2TR b)) )
by A5, A6, ThAZ9;
hence
( between a,b,c or between b,c,a or between c,a,b )
by ThConv6; verum