let n be Nat; for p, q being Point of (TOP-REAL n) holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
let p, q be Point of (TOP-REAL n); |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
|((p - q),(p - q))| =
((|(p,p)| - |(p,q)|) - |(p,q)|) + |(q,q)|
by Th27
.=
(|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
;
hence
|((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
; verum