theorem Th1: :: GTARSKI5:1

for S being satisfying_CongruenceIdentity satisfying_BetweennessIdentity TarskiGeometryStruct
for a, b, c being POINT of S st a,b <= c,c holds
a = b