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 & b,x equiv b,y holds

x = y

let a, b, x, y be POINT of S; :: thesis: ( a <> b & between a,b,x & between a,b,y & b,x equiv b,y implies x = y )

assume that

H1: a <> b and

H2: ( between a,b,x & between a,b,y ) and

H3: b,x equiv b,y ; :: thesis: x = y

a,b,y cong a,b,y by EquivReflexive;

hence y = x by A3, H1, H2, H3, A5; :: thesis: verum

x = y

let a, b, x, y be POINT of S; :: thesis: ( a <> b & between a,b,x & between a,b,y & b,x equiv b,y implies x = y )

assume that

H1: a <> b and

H2: ( between a,b,x & between a,b,y ) and

H3: b,x equiv b,y ; :: thesis: x = y

a,b,y cong a,b,y by EquivReflexive;

hence y = x by A3, H1, H2, H3, A5; :: thesis: verum