let a, b, c, p, q be Point of TarskiEuclid2Space; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum