let a, b, c, d be POINT of TarskiEuclid2Space; :: thesis: ( (dist (a,b)) ^2 = (dist (c,d)) ^2 iff a,b equiv c,d )

hereby :: thesis: ( a,b equiv c,d implies (dist (a,b)) ^2 = (dist (c,d)) ^2 )

assume A1: (dist (a,b)) ^2 = (dist (c,d)) ^2 ; :: thesis: a,b equiv c,d
( sqrt ((dist (a,b)) ^2) = dist (a,b) & sqrt ((dist (c,d)) ^2) = dist (c,d) ) by METRIC_1:5, SQUARE_1:22;
hence a,b equiv c,d by A1, GTARSKI1:def 15; :: thesis: verum

end;

assume a,b equiv c,d ; :: thesis: (dist (a,b)) ^2 = (dist (c,d)) ^2
hence (dist (a,b)) ^2 = (dist (c,d)) ^2 by GTARSKI1:def 15; :: thesis: verum