On the existence of factor sets by external equivalences in IST

We study the possibility of defining the factor sets of the real axis by external equivalences through external formulas on using the IST axiomatics of nonstandard analysis. We consider the case of an additive convex equivalence whose equivalence classes are defined by a formula with external universal quantifiers. We show that in this case there exists an external function selecting one representative from each equivalence class if and only if the relation in question coincides up to translation and dilation with the relation of infinite proximity.