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