let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for v, u, w being Element of V holds v - (u - w) = (v - u) + w
let v, u, w be Element of V; :: thesis: v - (u - w) = (v - u) + w
thus v - (u - w) = v - (u + (- w))
.= (v - u) - (- w) by Th41
.= (v - u) + w by Th30 ; :: thesis: verum