let F be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for a, b being Element of F holds - (a - b) = b - a
let a, b be Element of F; :: thesis: - (a - b) = b - a
thus - (a - b) = b + (- a) by RLVECT_1:33
.= b - a by RLVECT_1:def 11 ; :: thesis: verum