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 = L . (L . X) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds
ex R being non empty finite transitive mediate 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 = L . (L . X) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) implies ex R being non empty finite transitive mediate RelStr st
( the carrier of R = A & L = LAp R ) )
assume A0: ( L . A = A & ( for X being Subset of A holds L . X = L . (L . X) ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) ) ; :: thesis: ex R being non empty finite transitive mediate RelStr st
( the carrier of R = A & L = LAp R )
then for X being Subset of A holds L . X c= L . (L . X) ;
then consider R being non empty finite transitive RelStr such that
A1: ( the carrier of R = A & L = LAp R ) by ThProposition9, A0;
for X being Subset of A holds L . (L . X) c= L . X by A0;
then consider R2 being non empty finite mediate RelStr such that
A2: ( the carrier of R2 = A & L = LAp R2 ) by ROUGHS_2:42, A0;
reconsider LL = L as Function of (bool the carrier of R2),(bool the carrier of R2) by A2;
set H = Flip LL;
F1: (Flip LL) . {} = {} by ROUGHS_2:19, A0, A2;
f2: for S, T being Subset of the carrier of R2 holds (Flip LL) . (S \/ T) = ((Flip LL) . S) \/ ((Flip LL) . T) by ROUGHS_2:22, A2, A0;
set Rx = GeneratedRelStr (Flip LL);
S2: UAp R2 = Flip LL by ROUGHS_2:28, A2;
S3: UAp (GeneratedRelStr (Flip LL)) = Flip LL by KeyTheorem, F1, f2, ROUGHS_4:def 9;
then S5: the InternalRel of (GeneratedRelStr (Flip LL)) = the InternalRel of R2 by S2, Corr3A;
Flip LL = UAp R by A1, ROUGHS_2:28, A2;
then the InternalRel of (GeneratedRelStr (Flip LL)) = the InternalRel of R by Corr3A, S3, A1, A2;
then reconsider RRR = RelStr(# the carrier of (GeneratedRelStr (Flip LL)), the InternalRel of (GeneratedRelStr (Flip LL)) #) as non empty finite transitive mediate RelStr by S5, Th13, A2, A1;
take RRR ; :: thesis: ( the carrier of RRR = A & L = LAp RRR )
Flip (UAp RRR) = LAp RRR by ROUGHS_2:27;
hence ( the carrier of RRR = A & L = LAp RRR ) by ROUGHS_2:27, A2, S3, S2; :: thesis: verum