let L be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for b, c being Element of L holds c = b - (b - c)
let b, c be Element of L; :: thesis: c = b - (b - c)
set a = b - c;
((b - c) + c) - (b - c) = (c - (b - c)) + (b - c) by RLVECT_1:28
.= c by Th1 ;
hence c = b - (b - c) by Th1; :: thesis: verum