theorem :: MATHMORP:5

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T holds X (-) {(0. T)} = X