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

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