theorem :: ROUGHS_2:21

for X being set
for f being Function of (bool X),(bool X) st ( for A, B being Subset of X holds f . (A \/ B) = (f . A) \/ (f . B) ) holds
for A, B being Subset of X holds (Flip f) . (A /\ B) = ((Flip f) . A) /\ ((Flip f) . B)