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