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

ex R being non empty finite transitive RelStr st

( the carrier of R = A & U = UAp R )

let U be Function of (bool A),(bool A); :: thesis: ( U . {} = {} & ( for X being Subset of A holds U . (U . X) c= U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) implies ex R being non empty finite transitive RelStr st

( the carrier of R = A & U = UAp R ) )

assume A0: ( U . {} = {} & ( for X being Subset of A holds U . (U . X) c= U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) ) ; :: thesis: ex R being non empty finite transitive RelStr st

( the carrier of R = A & U = UAp R )

set L = Flip U;

a1: (Flip U) . A = A by ROUGHS_2:18, A0;

a2: for X being Subset of A holds (Flip U) . X c= (Flip U) . ((Flip U) . X) by ROUGHS_2:24, A0;

for X, Y being Subset of A holds (Flip U) . (X /\ Y) = ((Flip U) . X) /\ ((Flip U) . Y) by A0, ROUGHS_2:21;

then consider R being non empty finite transitive RelStr such that

W1: ( the carrier of R = A & Flip U = LAp R ) by a1, a2, ThProposition9;

U = Flip (Flip U) by ROUGHS_2:23;

then U = UAp R by W1, ROUGHS_2:28;

hence ex R being non empty finite transitive RelStr st

( the carrier of R = A & U = UAp R ) by W1; :: thesis: verum

ex R being non empty finite transitive RelStr st

( the carrier of R = A & U = UAp R )

let U be Function of (bool A),(bool A); :: thesis: ( U . {} = {} & ( for X being Subset of A holds U . (U . X) c= U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) implies ex R being non empty finite transitive RelStr st

( the carrier of R = A & U = UAp R ) )

assume A0: ( U . {} = {} & ( for X being Subset of A holds U . (U . X) c= U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) ) ; :: thesis: ex R being non empty finite transitive RelStr st

( the carrier of R = A & U = UAp R )

set L = Flip U;

a1: (Flip U) . A = A by ROUGHS_2:18, A0;

a2: for X being Subset of A holds (Flip U) . X c= (Flip U) . ((Flip U) . X) by ROUGHS_2:24, A0;

for X, Y being Subset of A holds (Flip U) . (X /\ Y) = ((Flip U) . X) /\ ((Flip U) . Y) by A0, ROUGHS_2:21;

then consider R being non empty finite transitive RelStr such that

W1: ( the carrier of R = A & Flip U = LAp R ) by a1, a2, ThProposition9;

U = Flip (Flip U) by ROUGHS_2:23;

then U = UAp R by W1, ROUGHS_2:28;

hence ex R being non empty finite transitive RelStr st

( the carrier of R = A & U = UAp R ) by W1; :: thesis: verum