theorem Th22: :: ROUGHS_2:22

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)