theorem ThNull: :: GTARSKI2:25

for a, b, c, d being POINT of TarskiEuclid2Space st (dist (a,b)) + (dist (c,d)) = 0 holds
( a = b & c = d )