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 c= 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 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 c= 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 RelStr st

( the carrier of R = A & L = LAp R ) )

assume A0: ( L . A = A & ( for X being Subset of A holds L . X c= 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 RelStr st

( the carrier of R = A & L = LAp R )

set H = Flip L;

LL: L = Flip (Flip L) by ROUGHS_2:23;

C1: (Flip L) . {} = {} by A0, ROUGHS_2:19;

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

then consider R being non empty finite RelStr such that

A1: ( the carrier of R = A & LAp R = L & UAp R = Flip L & ( for x, y being Element of R holds

( [x,y] in the InternalRel of R iff x in (Flip L) . {y} ) ) ) by YaoTh3, LL, C1;

for x, y, z being object st x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in the InternalRel of R & [y,z] in the InternalRel of R holds

[x,z] in the InternalRel of R

hence ex R being non empty finite transitive RelStr st

( the carrier of R = A & L = LAp R ) by A1; :: thesis: verum

ex R being non empty finite transitive 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 c= 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 RelStr st

( the carrier of R = A & L = LAp R ) )

assume A0: ( L . A = A & ( for X being Subset of A holds L . X c= 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 RelStr st

( the carrier of R = A & L = LAp R )

set H = Flip L;

LL: L = Flip (Flip L) by ROUGHS_2:23;

C1: (Flip L) . {} = {} by A0, ROUGHS_2:19;

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

then consider R being non empty finite RelStr such that

A1: ( the carrier of R = A & LAp R = L & UAp R = Flip L & ( for x, y being Element of R holds

( [x,y] in the InternalRel of R iff x in (Flip L) . {y} ) ) ) by YaoTh3, LL, C1;

for x, y, z being object st x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in the InternalRel of R & [y,z] in the InternalRel of R holds

[x,z] in the InternalRel of R

proof

then
R is transitive
by ORDERS_2:def 3, RELAT_2:def 8;
let x, y, z be object ; :: thesis: ( x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in the InternalRel of R & [y,z] in the InternalRel of R implies [x,z] in the InternalRel of R )

assume B1: ( x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in the InternalRel of R & [y,z] in the InternalRel of R ) ; :: thesis: [x,z] in the InternalRel of R

reconsider z = z as Element of R by B1;

reconsider xx = x as Element of R by B1;

reconsider w = x, yw = y as Element of R by B1;

reconsider XX = {xx} as Subset of R ;

zz: L is /\-preserving by A0, ROUGHS_4:def 10;

reconsider xx = {x}, yy = {y} as Subset of A by ZFMISC_1:31, A1, B1;

yy in bool A ;

then reconsider Hy = (Flip L) . {y} as Subset of A by FUNCT_2:5;

ZX: {y} c= (Flip L) . {z} by A1, ZFMISC_1:31, B1;

reconsider Hz = (Flip L) . {z} as Subset of A by A1, FUNCT_2:5;

reconsider az = {z} as Subset of A by A1;

G1: (Flip L) . yy c= (Flip L) . Hz by ROUGHS_4:def 8, zz, ZX;

(Flip L) . ((Flip L) . az) c= (Flip L) . az by R224, A0;

then BL: (Flip L) . {y} c= (Flip L) . {z} by G1, XBOOLE_1:1;

w in (Flip L) . {yw} by B1, A1;

hence [x,z] in the InternalRel of R by A1, BL; :: thesis: verum

end;assume B1: ( x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in the InternalRel of R & [y,z] in the InternalRel of R ) ; :: thesis: [x,z] in the InternalRel of R

reconsider z = z as Element of R by B1;

reconsider xx = x as Element of R by B1;

reconsider w = x, yw = y as Element of R by B1;

reconsider XX = {xx} as Subset of R ;

zz: L is /\-preserving by A0, ROUGHS_4:def 10;

reconsider xx = {x}, yy = {y} as Subset of A by ZFMISC_1:31, A1, B1;

yy in bool A ;

then reconsider Hy = (Flip L) . {y} as Subset of A by FUNCT_2:5;

ZX: {y} c= (Flip L) . {z} by A1, ZFMISC_1:31, B1;

reconsider Hz = (Flip L) . {z} as Subset of A by A1, FUNCT_2:5;

reconsider az = {z} as Subset of A by A1;

G1: (Flip L) . yy c= (Flip L) . Hz by ROUGHS_4:def 8, zz, ZX;

(Flip L) . ((Flip L) . az) c= (Flip L) . az by R224, A0;

then BL: (Flip L) . {y} c= (Flip L) . {z} by G1, XBOOLE_1:1;

w in (Flip L) . {yw} by B1, A1;

hence [x,z] in the InternalRel of R by A1, BL; :: thesis: verum

hence ex R being non empty finite transitive RelStr st

( the carrier of R = A & L = LAp R ) by A1; :: thesis: verum