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))| = - |(p1,(- p2))| by Th19
.= - (- |(p1,p2)|) by Th19 ;
hence |((- p1),(- p2))| = |(p1,p2)| ; :: thesis: verum