let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for u, w being Element of V holds - (u + w) = (- w) + (- u)
let u, w be Element of V; :: thesis: - (u + w) = (- w) + (- u)
(u + w) + ((- w) + (- u)) = u + (w + ((- w) + (- u))) by Def6
.= u + ((w + (- w)) + (- u)) by Def6
.= u + ((0. V) + (- u)) by Def13
.= u + (- u) by Th10
.= 0. V by Def13 ;
hence - (u + w) = (- w) + (- u) by Def13; :: thesis: verum