:: deftheorem Def7 defines mediate ROUGHS_2:def 7 :
for R being RelStr holds
( R is mediate iff the InternalRel of R is_mediate_in the carrier of R );