for A being LinearOrder holds the InternalRel of A linearly_orders the carrier of A