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 . (L . X) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds
ex R being non empty finite transitive RelStr st
( the carrier of R = A & L = LAp R )