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