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

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