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 . (X `)) ` ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds
ex R being non empty finite serial 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 . (X `)) ` ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) implies ex R being non empty finite serial RelStr st
( the carrier of R = A & L = LAp R ) )
assume that
A1:
L . A = A
and
A2:
for X being Subset of A holds L . X c= (L . (X `)) `
and
A3:
for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y)
; ex R being non empty finite serial RelStr st
( the carrier of R = A & L = LAp R )
consider R being non empty finite RelStr such that
A4:
( the carrier of R = A & L = LAp R )
by Th30, A1, A3;
set XX = {} A;
A5:
L . (({} A) `) = A
by A1;
then A6:
L . {} c= ([#] A) `
by A2;
for x being object st x in the carrier of R holds
ex y being object st
( y in the carrier of R & [x,y] in the InternalRel of R )
proof
let x be
object ;
( x in the carrier of R implies ex y being object st
( y in the carrier of R & [x,y] in the InternalRel of R ) )
assume A7:
x in the
carrier of
R
;
ex y being object st
( y in the carrier of R & [x,y] in the InternalRel of R )
reconsider Z =
[#] A as
Subset of
R by A4;
A8:
(LAp R) . {} =
LAp ({} R)
by Def10
.=
{ y where y is Element of R : Class ( the InternalRel of R,y) c= {} }
;
for
y being
Element of
R holds
Class ( the
InternalRel of
R,
y)
<> {}
then
Class ( the
InternalRel of
R,
x)
<> {}
by A7;
then consider t being
object such that A9:
t in Im ( the
InternalRel of
R,
x)
by XBOOLE_0:def 1;
A10:
[x,t] in the
InternalRel of
R
by A9, RELAT_1:169;
then
t in rng the
InternalRel of
R
by RELSET_1:25, A7;
hence
ex
y being
object st
(
y in the
carrier of
R &
[x,y] in the
InternalRel of
R )
by A10;
verum
end;
then
R is serial
by Def1;
hence
ex R being non empty finite serial RelStr st
( the carrier of R = A & L = LAp R )
by A4; verum