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 )
proof
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 ;
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
A8: x in U . Y by ;
x in U . (U . Y) by ;
then x in U . (UAp Y) by ;
hence x in UAp (UAp Y) by ; :: thesis: verum
end;
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 ;
reconsider Z = {z} as Subset of R by ;
A11: ( z in {z} & z in Class ( the InternalRel of R,t) & z in UAp Y ) by ;
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 ; :: thesis: 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; :: thesis: verum