for A being Order holds the InternalRel of A partially_orders the carrier of A