let A be non empty finite set ; :: thesis: 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 )

let L be Function of (bool A),(bool A); :: thesis: ( L . A = A & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) implies ex R being non empty finite RelStr st
( the carrier of R = A & L = LAp R ) )

assume that
A1: L . A = A and
A2: for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ; :: thesis: ex R being non empty finite RelStr st
( the carrier of R = A & L = LAp R )

set U = Flip L;
A3: (Flip L) . {} = {} by ;
A4: for X, Y being Subset of A holds (Flip L) . (X \/ Y) = ((Flip L) . X) \/ ((Flip L) . Y) by ;
consider R being non empty finite RelStr such that
A5: ( the carrier of R = A & Flip L = UAp R ) by Th29, A3, A4;
take R ; :: thesis: ( the carrier of R = A & L = LAp R )
L = Flip (UAp R) by ;
hence ( the carrier of R = A & L = LAp R ) by ; :: thesis: verum