theorem ThConv7: :: GTARSKI2:21

for a, b being Point of TarskiEuclid2Space holds
( between a,a,b & between a,b,b )