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