let E be RealNormSpace; :: thesis: for a, b being Point of E holds (a + b) - b = a
let a, b be Point of E; :: thesis: (a + b) - b = a
thus (a + b) - b = a + (b - b) by RLVECT_1:28
.= a + (0. E) by RLVECT_1:15
.= a by RLVECT_1:4 ; :: thesis: verum