theorem Th33: :: ROUGHS_2:33

for A being non empty finite set
for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . X c= (L . (X `)) ` ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds
ex R being non empty finite serial RelStr st
( the carrier of R = A & L = LAp R )