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)|
A1: |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| by Th53
.= (|(p,p)| + |(q,q)|) - (2 * |(p,q)|) ;
( 0 <= |(p,p)| & 0 <= |(q,q)| ) by Th57;
then 0 + 0 <= |(p,p)| + |(q,q)| by XREAL_1:9;
then A2: 0 / 2 <= (|(p,p)| + |(q,q)|) / 2 by XREAL_1:74;
0 <= |((p - q),(p - q))| by Th57;
then 2 * |(p,q)| <= (|(p,p)| + |(q,q)|) - 0 by A1, XREAL_1:13;
then (2 * |(p,q)|) / 2 <= (|(p,p)| + |(q,q)|) / 2 by XREAL_1:74;
then 0 + |(p,q)| <= ((|(p,p)| + |(q,q)|) / 2) + ((|(p,p)| + |(q,q)|) / 2) by A2, XREAL_1:9;
hence |(p,q)| <= |(p,p)| + |(q,q)| ; :: thesis: verum