let n be Element of NAT ; :: thesis: for x, y, z being Point of (TOP-REAL n) holds (x - y) - z = (x - z) - y
let x, y, z be Point of (TOP-REAL n); :: thesis: (x - y) - z = (x - z) - y
thus (x - y) - z = (x - z) + (- y) by JORDAN2C:9
.= (x - z) - y ; :: thesis: verum