let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for u, v being Element of V ex w being Element of V st v - w = u
let u, v be Element of V; :: thesis: ex w being Element of V st v - w = u
consider w being Element of V such that
A1: v + w = u by Lm2;
take - w ; :: thesis: v - (- w) = u
thus v - (- w) = u by A1; :: thesis: verum