let F be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for a, b being Element of F st a - b = 0. F holds

b - a = 0. F

let a, b be Element of F; :: thesis: ( a - b = 0. F implies b - a = 0. F )

a - b = - (b - a) by RLVECT_1:33;

hence ( a - b = 0. F implies b - a = 0. F ) by Th24; :: thesis: verum

b - a = 0. F

let a, b be Element of F; :: thesis: ( a - b = 0. F implies b - a = 0. F )

a - b = - (b - a) by RLVECT_1:33;

hence ( a - b = 0. F implies b - a = 0. F ) by Th24; :: thesis: verum