let S be satisfying_CongruenceIdentity satisfying_BetweennessIdentity TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st a,b <= c,c holds
a = b
let a, b, c be POINT of S; :: thesis: ( a,b <= c,c implies a = b )
assume a,b <= c,c ; :: thesis: a = b
then consider y being POINT of S such that
A1: between c,y,c and
A2: a,b equiv c,y ;
c = y by A1, GTARSKI1:def 10;
hence a = b by A2, GTARSKI1:def 7; :: thesis: verum