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 . (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); :: thesis: ( 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) ; :: thesis: 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 )

hence ex R being non empty finite mediate RelStr st

( the carrier of R = A & U = UAp R ) by A4; :: thesis: verum

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); :: thesis: ( 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) ; :: thesis: 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

then
R is mediate
by Def5;
let x, y be object ; :: thesis: ( 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 ) ; :: thesis: ( 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 ; :: thesis: 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)

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

end;( 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 ) ; :: thesis: ( 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 ; :: thesis: 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)

proof

then consider t being Element of R such that
A8:
x in U . Y
by A4, Def11, A7;

x in U . (U . Y) by A2, TARSKI:def 3, A4, A8;

then x in U . (UAp Y) by Def11, A4;

hence x in UAp (UAp Y) by Def11, A4; :: thesis: verum

end;x in U . (U . Y) by A2, TARSKI:def 3, A4, A8;

then x in U . (UAp Y) by Def11, A4;

hence x in UAp (UAp Y) by Def11, A4; :: thesis: verum

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

hence ex R being non empty finite mediate RelStr st

( the carrier of R = A & U = UAp R ) by A4; :: thesis: verum