let A be non empty finite set ; :: thesis: 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); :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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) <> {}

proof

let y be Element of R; :: thesis: Class ( the InternalRel of R,y) <> {}
assume Class ( the InternalRel of R,y) = {} ; :: thesis: contradiction
then y in { z where z is Element of R : Class ( the InternalRel of R,z) c= {} } ;
hence contradiction by A7, A6, Th27; :: thesis: verum

end;

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; :: thesis: 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; :: thesis: verum