let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( |.(p1 - p2).| = 0 iff p1 = p2 )

hereby :: thesis: ( p1 = p2 implies |.(p1 - p2).| = 0 )

assume |.(p1 - p2).| = 0 ; :: thesis: p1 = p2
then p1 - p2 = 0. (TOP-REAL 2) by EUCLID_2:42;
hence p1 = p2 by RLVECT_1:21; :: thesis: verum

end;

assume p1 = p2 ; :: thesis: |.(p1 - p2).| = 0
then p1 - p2 = 0. (TOP-REAL 2) by RLVECT_1:5;
hence |.(p1 - p2).| = 0 by EUCLID_2:39; :: thesis: verum