let n be Nat; 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; |(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)|
; verum