theorem :: ROUGHS_2:43

for A being non empty finite set
for L being Function of (bool A),(bool A) st L . A = A & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds
( ( for X being Subset of A holds L . X c= (L . (X `)) ` ) iff L . {} = {} )