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

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