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