theorem ThEgal: :: GTARSKI2:24

for a, b being POINT of TarskiEuclid2Space holds
( a = b iff dist (a,b) = 0 )