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