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