:: deftheorem defines mediate ROUGHS_2:def 6 :
for R being Relation holds
( R is mediate iff R is_mediate_in field R );