let A be non empty finite set ; 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); ( 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) ) )
; 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
; ( 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; verum