theorem :: MATHMORP:25

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, Z being Subset of T holds X (+) (Y (-) Z) c= (X (+) Y) (-) Z