let n be Nat; for p1, p2 being Point of (TOP-REAL n) holds |((- p1),(- p2))| = |(p1,p2)|
let p1, p2 be Point of (TOP-REAL n); |((- p1),(- p2))| = |(p1,p2)|
|((- p1),(- p2))| =
- |(p1,(- p2))|
by Th19
.=
- (- |(p1,p2)|)
by Th19
;
hence
|((- p1),(- p2))| = |(p1,p2)|
; verum