let n be Nat; :: thesis: for q1, q2 being Point of (TOP-REAL n) holds |.(|.q1.| - |.q2.|).| <= |.(q1 - q2).|
let q1, q2 be Point of (TOP-REAL n); :: thesis: |.(|.q1.| - |.q2.|).| <= |.(q1 - q2).|

per cases ( |.q1.| >= |.q2.| or |.q1.| < |.q2.| ) ;

suppose |.q1.| >= |.q2.| ; :: thesis: |.(|.q1.| - |.q2.|).| <= |.(q1 - q2).|

then |.q1.| - |.q2.| >= 0 by XREAL_1:48;
then |.q1.| - |.q2.| = |.(|.q1.| - |.q2.|).| by ABSVALUE:def 1;
hence |.(|.q1.| - |.q2.|).| <= |.(q1 - q2).| by TOPRNS_1:32; :: thesis: verum

end;

suppose A1: |.q1.| < |.q2.| ; :: thesis: |.(|.q1.| - |.q2.|).| <= |.(q1 - q2).|

A2: |.q2.| - |.q1.| <= |.(q2 - q1).| by TOPRNS_1:32;
|.q2.| - |.q1.| > 0 by A1, XREAL_1:50;
then |.(|.q2.| - |.q1.|).| <= |.(q2 - q1).| by A2, ABSVALUE:def 1;
then |.(|.q2.| - |.q1.|).| <= |.(q1 - q2).| by TOPRNS_1:27;
hence |.(|.q1.| - |.q2.|).| <= |.(q1 - q2).| by UNIFORM1:11; :: thesis: verum

end;

end;