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:64
.= (- a) - (- b) by RLVECT_1:30 ; :: thesis: (a - b) + c = (a + c) - b
thus (a - b) + c = (a + c) - b by RLVECT_1:def 6; :: thesis: verum