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 z = - w; :: thesis: v - z = u
thus v - z = u by A1, Th30; :: thesis: verum