let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, Y being Subset of T
for p being Point of T holds (X + p) (O) Y = (X (O) Y) + p
let X, Y be Subset of T; :: thesis: for p being Point of T holds (X + p) (O) Y = (X (O) Y) + p
let p be Point of T; :: thesis: (X + p) (O) Y = (X (O) Y) + p
thus (X + p) (O) Y = ((X (-) Y) + p) (+) Y by Th14
.= (X (O) Y) + p by Th15 ; :: thesis: verum