let n be Nat; :: thesis: for p, q being Element of n -tuples_on REAL holds |(p,q)| <= |(p,p)| + |(q,q)|
let p, q be Element of n -tuples_on REAL; :: thesis: |(p,q)| <= |(p,p)| + |(q,q)|
( 0 <= |(p,p)| & 0 <= |(q,q)| ) by Th119;
then A1: 0 / 2 <= (|(p,p)| + |(q,q)|) / 2 ;
|((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| by Th139
.= (|(p,p)| + |(q,q)|) - (2 * |(p,q)|) ;
then 2 * |(p,q)| <= (|(p,p)| + |(q,q)|) - 0 by Th119, 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