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 . (U . X) ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds
ex R being non empty finite mediate 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 . (U . X) ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) implies ex R being non empty finite mediate 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 . (U . X)
and
A3:
for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y)
; ex R being non empty finite mediate 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, y being object st x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R holds
ex z being object st
( z in the carrier of R & [x,z] in the InternalRel of R & [z,y] in the InternalRel of R )
proof
let x,
y be
object ;
( x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R implies ex z being object st
( z in the carrier of R & [x,z] in the InternalRel of R & [z,y] in the InternalRel of R ) )
assume A5:
(
x in the
carrier of
R &
y in the
carrier of
R )
;
( not [x,y] in the InternalRel of R or ex z being object st
( z in the carrier of R & [x,z] in the InternalRel of R & [z,y] in the InternalRel of R ) )
then reconsider Y =
{y} as
Subset of
R by ZFMISC_1:31;
assume A6:
[x,y] in the
InternalRel of
R
;
ex z being object st
( z in the carrier of R & [x,z] in the InternalRel of R & [z,y] in the InternalRel of R )
reconsider x =
x as
Element of
R by A5;
(
y in Class ( the
InternalRel of
R,
x) &
y in {y} )
by A6, TARSKI:def 1, RELAT_1:169;
then
Class ( the
InternalRel of
R,
x)
meets {y}
by XBOOLE_0:def 4;
then A7:
x in UAp Y
;
x in UAp (UAp Y)
then consider t being
Element of
R such that A9:
(
t = x &
Class ( the
InternalRel of
R,
t)
meets UAp Y )
;
consider z being
object such that A10:
z in (Class ( the InternalRel of R,t)) /\ (UAp Y)
by A9, XBOOLE_0:def 1;
reconsider Z =
{z} as
Subset of
R by ZFMISC_1:31, A10;
A11:
(
z in {z} &
z in Class ( the
InternalRel of
R,
t) &
z in UAp Y )
by A10, XBOOLE_0:def 4, TARSKI:def 1;
then
Class ( the
InternalRel of
R,
t)
meets {z}
by XBOOLE_0:def 4;
then
t in UAp Z
;
then
(
[t,z] in the
InternalRel of
R &
[z,y] in the
InternalRel of
R )
by A11, A5, Th5;
hence
ex
z being
object st
(
z in the
carrier of
R &
[x,z] in the
InternalRel of
R &
[z,y] in the
InternalRel of
R )
by A9, A10;
verum
end;
then
R is mediate
by Def5;
hence
ex R being non empty finite mediate RelStr st
( the carrier of R = A & U = UAp R )
by A4; verum