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