field the InternalRel of R = the carrier of R
by ORDERS_1:12;

hence the InternalRel of R is mediate by ROUGHS_2:def 6, ROUGHS_2:def 7; :: thesis: verum

hence the InternalRel of R is mediate by ROUGHS_2:def 6, ROUGHS_2:def 7; :: thesis: verum