let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, x, y being POINT of S st a <> b & between a,b,x & between a,b,y & a,x equiv a,y holds
x = y
let a, b, x, y be POINT of S; :: thesis: ( a <> b & between a,b,x & between a,b,y & a,x equiv a,y implies x = y )
assume that
H1: a <> b and
H2: between a,b,x and
H3: between a,b,y and
H4: a,x equiv a,y ; :: thesis: x = y
consider m being POINT of S such that
X1: ( between b,a,m & a,m equiv a,b ) by A4;
X3: m <> a by X1, EquivSymmetric, A3, H1;
X2: between m,a,b by X1, Bsymmetry;
then x4: m,a,b,x are_ordered by H1, H2, BTransitivityOrdered;
m,a,b,y are_ordered by H1, X2, H3, BTransitivityOrdered;
hence x = y by X3, x4, H4, C1; :: thesis: verum