theorem min1: :: REALALG1:15

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