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)| =
|(((- 1) * p1),p2)|
.=
(- 1) * |(p1,p2)|
by Th17
;
hence
|((- p1),p2)| = - |(p1,p2)|
; verum