let a, b, c, d be POINT of TarskiEuclid2Space; :: thesis: ( (dist (a,b)) + (dist (c,d)) = 0 implies ( a = b & c = d ) )
assume A1: (dist (a,b)) + (dist (c,d)) = 0 ; :: thesis: ( a = b & c = d )
( 0 <= dist (a,b) & 0 <= dist (c,d) ) by METRIC_1:5;
then ( dist (a,b) = 0 & dist (c,d) = 0 ) by A1;
hence ( a = b & c = d ) by ThEgal; :: thesis: verum