theorem :: MATHMORP:29

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B, C being Subset of T holds X (-) (B \/ C) = (X (-) B) /\ (X (-) C)