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