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 . (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); ( 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) ) )
; 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
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 A0:
(
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 A1:
[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 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
x in { t where t is Element of R : Class ( the InternalRel of R,t) meets UAp Y }
by ROUGHS_1:def 5;
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;
verum
end;
then
R is mediate
by ROUGHS_2:def 7, ROUGHS_2:def 5;
hence
ex R being non empty finite transitive mediate RelStr st
( the carrier of R = A & U = UAp R )
by a1; verum