let G be AbGroup; :: thesis: for a, b, c being Element of G holds
( - (a - b) = (- a) - (- b) & (a - b) + c = (a + c) - b )
let a, b, c be Element of G; :: thesis: ( - (a - b) = (- a) - (- b) & (a - b) + c = (a + c) - b )
thus - (a - b) = (- a) + b by VECTSP_1:17
.= (- a) - (- b) by RLVECT_1:17 ; :: thesis: (a - b) + c = (a + c) - b
thus (a - b) + c = (a + c) - b by RLVECT_1:def 3; :: thesis: verum