Within Bishop Set Theory, a reconstruction of Bishop’s theory of sets, we study the so-called completely separated sets, that is, sets equipped with a positive notion of an inequality, induced by a given set of real-valued functions. We introduce the notion of a global family of completely separated sets over an index-completely separated set, and we describe its Sigma- and Pi-set. The free completely separated set on a given set is also presented. Purely set-theoretic versions of the classical Stone–Čech theorem (...) and the Tychonoff embedding theorem for completely regular spaces are given, replacing topological spaces with function spaces and completely regular spaces with completely separated sets. (shrink)