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 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); ( 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) ) )
; 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
let x,
y,
z be
object ;
( 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 )
;
[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;
verum
end;
then
R is transitive
by ORDERS_2:def 3, RELAT_2:def 8;
hence
ex R being non empty finite transitive RelStr st
( the carrier of R = A & L = LAp R )
by A1; verum