  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-\v{C}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.
