let A be non empty finite set ; :: thesis: for U being Function of (bool A),(bool A) st U . {} = {} & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds
( ( for X being Subset of A holds (U . (X `)) ` c= U . X ) iff U . A = A )
let U be Function of (bool A),(bool A); :: thesis: ( U . {} = {} & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) implies ( ( for X being Subset of A holds (U . (X `)) ` c= U . X ) iff U . A = A ) )
assume that
A1: U . {} = {} and
A2: for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ; :: thesis: ( ( for X being Subset of A holds (U . (X `)) ` c= U . X ) iff U . A = A )
thus ( ( for X being Subset of A holds (U . (X `)) ` c= U . X ) implies U . A = A ) :: thesis: ( U . A = A implies for X being Subset of A holds (U . (X `)) ` c= U . X )

proof

assume for X being Subset of A holds (U . (X `)) ` c= U . X ; :: thesis: U . A = A
then consider R being non empty serial RelStr such that
A3: ( the carrier of R = A & U = UAp R ) by Th34, A1, A2;
(UAp R) . ([#] R) = UAp ([#] R) by Def11;
hence U . A = A by A3; :: thesis: verum

end;

assume U . A = A ; :: thesis: for X being Subset of A holds (U . (X `)) ` c= U . X
then consider R being non empty finite serial RelStr such that
A4: ( the carrier of R = A & U = UAp R ) by A1, Th32, A2;
let X be Subset of A; :: thesis: (U . (X `)) ` c= U . X
reconsider Xa = X as Subset of R by A4;
set L = Flip U;
A5: Flip U = LAp R by A4, Th27;
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 (U . (X `)) ` c= U . X by Def14, A4, A5; :: thesis: verum