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