let R be RelStr ; :: thesis: ( R is reflexive implies R is mediate )
assume A1: R is reflexive ; :: thesis: 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 ; :: 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 A2: ( 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 ) )
assume A3: [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 )
[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; :: thesis: verum

end;

hence R is mediate by Def5; :: thesis: verum