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

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

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

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

end;

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

A2: |.q2.| - |.q1.| <= |.(q2 - q1).| by TOPRNS_1:33;
|.q2.| - |.q1.| > 0 by A1, XREAL_1:52;
then abs (|.q2.| - |.q1.|) <= |.(q2 - q1).| by A2, ABSVALUE:def 1;
then abs (|.q2.| - |.q1.|) <= |.(q1 - q2).| by TOPRNS_1:28;
hence abs (|.q1.| - |.q2.|) <= |.(q1 - q2).| by UNIFORM1:13; :: thesis: verum

end;

end;