let R be RelStr ; ( R is reflexive implies R is mediate )
assume A1:
R is reflexive
; R is mediate
set IR = the InternalRel of R;
set X = the carrier of R;
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 A2:
(
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 ) )
assume A3:
[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 )
[x,x] in the
InternalRel of
R
by A2, RELAT_2:def 1, A1, ORDERS_2:def 2;
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 A2, A3;
verum
end;
hence
R is mediate
by Def5; verum