theorem ThConv7ter: :: GTARSKI2:23

for a, b being Point of TarskiEuclid2Space st between a,b,a holds
a = b