let A be non empty finite set ; :: thesis: for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . X c= X ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

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

( the carrier of R = A & L = LAp R ) )

assume that

A1: L . A = A and

A2: for X being Subset of A holds L . X c= X and

A3: for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ; :: thesis: ex R being non empty finite reflexive RelStr st

( the carrier of R = A & L = LAp R )

set U = Flip L;

A4: (Flip L) . {} = {} by A1, Th19;

A5: for X being Subset of A holds X c= (Flip L) . X

then consider R being non empty finite reflexive RelStr such that

A6: ( the carrier of R = A & Flip L = UAp R ) by Th37, A4, A5;

L = Flip (UAp R) by Th23, A6;

then L = LAp R by Th27;

hence ex R being non empty finite reflexive RelStr st

( the carrier of R = A & L = LAp R ) by A6; :: thesis: verum

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

( the carrier of R = A & L = LAp R ) )

assume that

A1: L . A = A and

A2: for X being Subset of A holds L . X c= X and

A3: for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ; :: thesis: ex R being non empty finite reflexive RelStr st

( the carrier of R = A & L = LAp R )

set U = Flip L;

A4: (Flip L) . {} = {} by A1, Th19;

A5: for X being Subset of A holds X c= (Flip L) . X

proof

for X, Y being Subset of A holds (Flip L) . (X \/ Y) = ((Flip L) . X) \/ ((Flip L) . Y)
by A3, Th22;
let X be Subset of A; :: thesis: X c= (Flip L) . X

(X `) ` c= (L . (X `)) ` by A2, SUBSET_1:12;

hence X c= (Flip L) . X by Def14; :: thesis: verum

end;(X `) ` c= (L . (X `)) ` by A2, SUBSET_1:12;

hence X c= (Flip L) . X by Def14; :: thesis: verum

then consider R being non empty finite reflexive RelStr such that

A6: ( the carrier of R = A & Flip L = UAp R ) by Th37, A4, A5;

L = Flip (UAp R) by Th23, A6;

then L = LAp R by Th27;

hence ex R being non empty finite reflexive RelStr st

( the carrier of R = A & L = LAp R ) by A6; :: thesis: verum