let F be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for a, b being Element of F holds a + b = - ((- b) + (- a))
let a, b be Element of F; :: thesis: a + b = - ((- b) + (- a))
thus a + b = - (- (a + b)) by RLVECT_1:17
.= - ((- b) + (- a)) by RLVECT_1:31 ; :: thesis: verum