theorem :: GTARSKI2:29

for a being Point of TarskiEuclid2Space holds between a,a,a by ThConv7;