let A be 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
( ( for X being Subset of A holds L . X c= (L . (X `)) ` ) iff L . {} = {} )
let L be Function of (bool A),(bool A); ( 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)
; ( ( 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 . {} = {} )
( L . {} = {} implies for X being Subset of A holds L . X c= (L . (X `)) ` )
assume
L . {} = {}
; 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; 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; verum