theorem Th30: :: ROUGHS_2:30

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
ex R being non empty finite RelStr st
( the carrier of R = A & L = LAp R )