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
( ( for X being Subset of A holds L . X c= (L . (X `)) ` ) iff L . {} = {} )
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 ( ( for X being Subset of A holds L . X c= (L . (X `)) ` ) iff L . {} = {} ) )
assume that
A1: L . A = A and
A2: for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ; :: thesis: ( ( for X being Subset of A holds L . X c= (L . (X `)) ` ) iff L . {} = {} )
thus ( ( for X being Subset of A holds L . X c= (L . (X `)) ` ) implies L . {} = {} ) :: thesis: ( L . {} = {} implies for X being Subset of A holds L . X c= (L . (X `)) ` )

proof

assume for X being Subset of A holds L . X c= (L . (X `)) ` ; :: thesis: L . {} = {}
then consider R being non empty finite serial RelStr such that
A3: ( the carrier of R = A & L = LAp R ) by A1, Th33, A2;
L . {} = LAp ({} R) by Def10, A3;
hence L . {} = {} ; :: thesis: verum

end;

assume L . {} = {} ; :: thesis: for X being Subset of A holds L . X c= (L . (X `)) `
then consider R being non empty serial RelStr such that
A4: ( the carrier of R = A & L = LAp R ) by A1, Th31, A2;
let X be Subset of A; :: thesis: L . X c= (L . (X `)) `
reconsider Xa = X as Subset of R by A4;
set U = Flip L;
A5: Flip L = UAp R by A4, Th28;
LAp Xa c= UAp Xa by Th17;
then LAp Xa c= (UAp R) . X by Def11;
then (LAp R) . X c= (UAp R) . X by Def10;
hence L . X c= (L . (X `)) ` by Def14, A4, A5; :: thesis: verum