theorem :: REALALG1:16

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for S1, S2 being Subset of L holds - (S1 \/ S2) = (- S1) \/ (- S2)