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 . (U . X) = U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite transitive 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 . (U . X) = U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) implies ex R being non empty finite transitive mediate RelStr st

( the carrier of R = A & U = UAp R ) )

assume a0: ( U . {} = {} & ( for X being Subset of A holds U . (U . X) = U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) ) ; :: thesis: ex R being non empty finite transitive mediate RelStr st

( the carrier of R = A & U = UAp R )

then for X being Subset of A holds U . (U . X) c= U . X ;

then consider R being non empty finite transitive RelStr such that

a1: ( the carrier of R = A & U = UAp R ) by ThProposition9U, a0;

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 transitive mediate RelStr st

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

ex R being non empty finite transitive 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 . (U . X) = U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) implies ex R being non empty finite transitive mediate RelStr st

( the carrier of R = A & U = UAp R ) )

assume a0: ( U . {} = {} & ( for X being Subset of A holds U . (U . X) = U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) ) ; :: thesis: ex R being non empty finite transitive mediate RelStr st

( the carrier of R = A & U = UAp R )

then for X being Subset of A holds U . (U . X) c= U . X ;

then consider R being non empty finite transitive RelStr such that

a1: ( the carrier of R = A & U = UAp R ) by ThProposition9U, a0;

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 ROUGHS_2:def 7, ROUGHS_2:def 5;
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 A0: ( 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 A1: [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 A0;

( y in Class ( the InternalRel of R,x) & y in {y} ) by RELAT_1:169, A1, TARSKI:def 1;

then (Class ( the InternalRel of R,x)) /\ {y} <> {} by XBOOLE_0:def 4;

then Class ( the InternalRel of R,x) meets {y} by XBOOLE_0:def 7;

then x in { t where t is Element of R : Class ( the InternalRel of R,t) meets {y} } ;

then B1: x in UAp Y by ROUGHS_1:def 5;

x in UAp (UAp Y)

then consider t being Element of R such that

B4: ( t = x & Class ( the InternalRel of R,t) meets UAp Y ) ;

consider z being object such that

B5: z in (Class ( the InternalRel of R,t)) /\ (UAp Y) by XBOOLE_0:7, B4, XBOOLE_0:def 7;

reconsider Z = {z} as Subset of R by ZFMISC_1:31, B5;

( z in {z} & z in Class ( the InternalRel of R,t) & z in UAp Y ) by B5, XBOOLE_0:def 4, TARSKI:def 1;

then ( z in {z} /\ (Class ( the InternalRel of R,t)) & z in UAp Y ) by XBOOLE_0:def 4;

then ( Class ( the InternalRel of R,t) meets {z} & [z,y] in the InternalRel of R ) by XBOOLE_0:def 7, ROUGHS_2:5, A0;

then ( t in { w where w is Element of R : Class ( the InternalRel of R,w) meets {z} } & [z,y] in the InternalRel of R ) ;

then ( t in UAp Z & [z,y] in the InternalRel of R ) by ROUGHS_1:def 5;

then ( [t,z] in the InternalRel of R & [z,y] in the InternalRel of R ) by ROUGHS_2:5, B5;

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

end;( z in the carrier of R & [x,z] in the InternalRel of R & [z,y] in the InternalRel of R ) )

assume A0: ( 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 A1: [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 A0;

( y in Class ( the InternalRel of R,x) & y in {y} ) by RELAT_1:169, A1, TARSKI:def 1;

then (Class ( the InternalRel of R,x)) /\ {y} <> {} by XBOOLE_0:def 4;

then Class ( the InternalRel of R,x) meets {y} by XBOOLE_0:def 7;

then x in { t where t is Element of R : Class ( the InternalRel of R,t) meets {y} } ;

then B1: x in UAp Y by ROUGHS_1:def 5;

x in UAp (UAp Y)

proof

then
x in { t where t is Element of R : Class ( the InternalRel of R,t) meets UAp Y }
by ROUGHS_1:def 5;
x in U . Y
by a1, ROUGHS_2:def 11, B1;

then x in U . (U . Y) by a1, a0;

then x in U . (UAp Y) by ROUGHS_2:def 11, a1;

hence x in UAp (UAp Y) by ROUGHS_2:def 11, a1; :: thesis: verum

end;then x in U . (U . Y) by a1, a0;

then x in U . (UAp Y) by ROUGHS_2:def 11, a1;

hence x in UAp (UAp Y) by ROUGHS_2:def 11, a1; :: thesis: verum

then consider t being Element of R such that

B4: ( t = x & Class ( the InternalRel of R,t) meets UAp Y ) ;

consider z being object such that

B5: z in (Class ( the InternalRel of R,t)) /\ (UAp Y) by XBOOLE_0:7, B4, XBOOLE_0:def 7;

reconsider Z = {z} as Subset of R by ZFMISC_1:31, B5;

( z in {z} & z in Class ( the InternalRel of R,t) & z in UAp Y ) by B5, XBOOLE_0:def 4, TARSKI:def 1;

then ( z in {z} /\ (Class ( the InternalRel of R,t)) & z in UAp Y ) by XBOOLE_0:def 4;

then ( Class ( the InternalRel of R,t) meets {z} & [z,y] in the InternalRel of R ) by XBOOLE_0:def 7, ROUGHS_2:5, A0;

then ( t in { w where w is Element of R : Class ( the InternalRel of R,w) meets {z} } & [z,y] in the InternalRel of R ) ;

then ( t in UAp Z & [z,y] in the InternalRel of R ) by ROUGHS_1:def 5;

then ( [t,z] in the InternalRel of R & [z,y] in the InternalRel of R ) by ROUGHS_2:5, B5;

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

hence ex R being non empty finite transitive mediate RelStr st

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