let n be Element of NAT ; :: thesis: for p1, p2, p3 being Point of (TOP-REAL n) holds (p1 + p2) - p3 = (p1 - p3) + p2
let p1, p2, p3 be Point of (TOP-REAL n); :: thesis: (p1 + p2) - p3 = (p1 - p3) + p2
thus (p1 + p2) - p3 = (p1 + (- p3)) + p2 by EUCLID:30
.= (p1 - p3) + p2 ; :: thesis: verum