let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n) holds |(p,q)| <= |(p,p)| + |(q,q)|
let p, q be Point of (TOP-REAL n); :: thesis: |(p,q)| <= |(p,p)| + |(q,q)|
( 0 <= |(p,p)| & 0 <= |(q,q)| ) by Th33;
then 0 + 0 <= |(p,p)| + |(q,q)| by XREAL_1:7;
then A1: 0 / 2 <= (|(p,p)| + |(q,q)|) / 2 by XREAL_1:72;
|((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| by Th29
.= (|(p,p)| + |(q,q)|) - (2 * |(p,q)|) ;
then 2 * |(p,q)| <= (|(p,p)| + |(q,q)|) - 0 by Th33, XREAL_1:11;
then (2 * |(p,q)|) / 2 <= (|(p,p)| + |(q,q)|) / 2 by XREAL_1:72;
then 0 + |(p,q)| <= ((|(p,p)| + |(q,q)|) / 2) + ((|(p,p)| + |(q,q)|) / 2) by A1, XREAL_1:7;
hence |(p,q)| <= |(p,p)| + |(q,q)| ; :: thesis: verum