let a, b, c, d be POINT of TarskiEuclid2Space; :: thesis: ( |.((Tn2TR a) - (Tn2TR b)).| = |.((Tn2TR c) - (Tn2TR d)).| iff a,b equiv c,d )
A1: ( dist (a,b) = |.((Tn2TR a) - (Tn2TR b)).| & dist (c,d) = |.((Tn2TR c) - (Tn2TR d)).| ) by ThConv3;
thus ( |.((Tn2TR a) - (Tn2TR b)).| = |.((Tn2TR c) - (Tn2TR d)).| implies a,b equiv c,d ) by A1, GTARSKI1:def 15; :: thesis: ( a,b equiv c,d implies |.((Tn2TR a) - (Tn2TR b)).| = |.((Tn2TR c) - (Tn2TR d)).| )
assume a,b equiv c,d ; :: thesis: |.((Tn2TR a) - (Tn2TR b)).| = |.((Tn2TR c) - (Tn2TR d)).|
hence |.((Tn2TR a) - (Tn2TR b)).| = |.((Tn2TR c) - (Tn2TR d)).| by A1, GTARSKI1:def 15; :: thesis: verum