let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for p, x being Point of T holds
( (p - x) + x = p & (p + x) - x = p )
let p, x be Point of T; :: thesis: ( (p - x) + x = p & (p + x) - x = p )
(p + x) - x = p + (x - x) by RLVECT_1:def 6
.= p + (0. T) by RLVECT_1:28
.= p by RLVECT_1:10 ;
hence ( (p - x) + x = p & (p + x) - x = p ) by RLVECT_1:42; :: thesis: verum