let n be Nat; :: thesis: for p1, p2, p3 being Point of (TOP-REAL n) holds p1 + (p2 - p3) = (p1 + p2) - p3
let p1, p2, p3 be Point of (TOP-REAL n); :: thesis: p1 + (p2 - p3) = (p1 + p2) - p3
thus p1 + (p2 - p3) = (p1 + p2) + (- p3) by FINSEQOP:29
.= (p1 + p2) - p3 ; :: thesis: verum