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