:: deftheorem Def5 defines is_mediate_in ROUGHS_2:def 5 :
for R being Relation
for X being set holds
( R is_mediate_in X iff for x, y being object st x in X & y in X & [x,y] in R holds
ex z being object st
( z in X & [x,z] in R & [z,y] in R ) );