# Topologies of open complemented subsets

Iosif Petrakis
Department of Computer Science, University of Verona
<EMAIL_ADDRESS>
###### Abstract

We introduce $\mathrm{cs}$-topologies, or topologies of complemented subsets,
as a new approach to constructive topology that preserves the duality between
open and closed subsets of classical topology. Complemented subsets were used
successfully by Bishop in his constructive formulation of the Daniell approach
to measure and integration. Here we use complemented subsets in topology, in
order to describe simulataneously an open set, the first-component of an open
complemented subset, and its complement as a closed set, the second component
of an open complemented subset. We analyse the canonical
$\mathrm{cs}$-topology induced by a metric, and we introduce the notion of a
mudulus of openness for a $\mathrm{cs}$-open subset of a metric space.
Pointwise and uniform continuity of functions between metric spaces are
formulated with respect to the way these functions inverse open complemented
subsets together with their moduli of openness. The addition of moduli of
openness in the concept of an open subset, given a base for the
$\mathrm{cs}$-topology, makes possible to define the notion of uniform
continuity of functions between csb-spaces, that is $\mathrm{cs}$-spaces with
a given base. In this way, the notions of pointwise and uniform continuity of
functions between metric spaces are directly generalised to the notions of
pointwise and uniform continuity between csb-topological spaces. Constructions
and facts from the classical theory of topologies of open subsets are
translated to our constructive theory of topologies of open complemented
subsets.
Keywords: topological spaces, constructive mathematics, complemented subsets,
pointwise and uniform continuity

##  1 Introduction

Roughly speaking, there are two main ways to constructivise the classical
notion of a topological space. The first is to “mimic” the definition of a
topological space as a starting point, and then to develop topology according
to the chosen constructive requirements. Certainly one will use
intuitionisitic logic, one may also want to use a point-free approach, or
start with a base of a topology, instead of a topology, and study neighborhood
spaces. The second way is to start from a notion of space other than that of a
topological space and generate one a posteriori. E.g., one can start from a
Bishop space, a constructive notion of $C(X)$, or from a constructive uniform
space. For a comprehensive account of the various approaches to constructive
topology see [42].

In a series of papers (see [26]-[31], [35, 36], and [41, 42]) we have
elaborated the theory of Bishop spaces. A motivation for the study of Bishop
spaces, an approach within the second way, was the realisation that the
classical duality between open and closed subsets cannot be preserved
constructively. The standard, weak complement $F^{c}$ of a closed subset $F$
need not be open constructively (take e.g., $F:=\\{0\\}\subset{\mathbb{R}}$).
If one starts from a topology of open subsets and define a closed subset to be
the strong complement $F^{\neq_{X}}:=\\{x\in X\mid\forall_{y\in
F}(x\neq_{X}y)\\}$, where $x\neq_{X}x{{}^{\prime}}$ is an extensional
inequality on a set $(X,=_{X})$, then the finite intersection of closed
subsets may not be provable constructively to be closed. All approaches to
constructive topology within the first way start from the properties of the
open subsets, which, in our view, is a “historical accident”. Classically, one
could start equivalently from a topology of closed subsets and define the open
subsets as certain complements of closed subsets. If one would start
constructively from the properties of closed subsets and define the open
subsets as weak or strong complements of closed ones, then some classical
properties of open subsets wouldn’t hold constructively. Although classically
the two starting points lead to the same theory, constructively this is not
the case, but at the same time there is no conceptual reason, other than the
power of the classical tradition of beginning with a topology of open subsets,
to base constructive topology to open or closed subsets. While within
classical logic the difference between open and closed subsets “collapses”,
within constructive logic this is not the case.

Here we explain how to develop constructive topology within the aforementioned
first way and preserve the classical duality between open and closed subsets.
The distinctive feature of our approach here is that we propose a shift from a
topology of open (or closed) subsets to a topology of open complemented
subsets. Moreover, we reformulate the notion of a point in a complemented
subsets-way and define complemented points as certain complemented subsets.
Topology in classical mathematics $\mathrm{CLASS}$ is usually described as
point-set topology. Here we introduce an approach to topology within
constructive mathematics $(\mathrm{CM})$ that can be described as complemented
point-complemented set topology.

$\frac{\mbox{(Point-Set) Topology}}{\mathrm{CLASS}}\ \sim\
\frac{\mbox{(Complemented Point-Complemented Set) Topology}}{\mathrm{CM}}$

Bishop’s central tool to the development of constructive measure theory was
the use of complemented subsets, in order to recover constructively the
classical duality between subsets and boolean-valued total functions, a
fundamental duality in the classical Daniell approach to measure theory. He
developed what we call Bishop Measure Theory (BMT) in [2], and together with
Cheng in [4], what we call Bishop-Cheng Measure Theory (BCMT). In both
theories complemented subsets are first-class citizens. Recently, a programme
of a predicative reformulation of BCMT is undertaken in [33, 51, 45, 15, 16].
Some connections between topology of Bishop spaces and constructive measure
theory, especially BMT, are studied in [30, 34]. In order to avoid the use of
the principle of the excluded middle (PEM) in the definition of the
characteristic function $\chi_{A}$ of a subset $A$ of $X$, Bishop employed
_complemented subsets_ $\bm{A}\coloneqq(A^{1},A^{0})$ of $X$, where
$A^{1},A^{0}$ are disjoint subsets of $X$ in a strong sense: $a^{1}\neq
a^{0}$, for every $a^{1}\in A^{1}$ and $a^{0}\in A^{0}$. The characteristic
function $\chi_{\bm{A}}\colon A^{1}\cup A^{0}\to\\{0,1\\}$ of a complemented
subset $\bm{A}$, defined by

$\chi_{\bm{A}}(x):=\left\\{\begin{array}[]{ll}1&\mbox{, $x\in A^{1}$}\\\
0&\mbox{, $x\in A^{0}$,}\end{array}\right.$

is a partial, boolean-valued function on $X$, as it is defined on the subset
$A^{1}\cup A^{0}$ of $X$, without though, the use of PEM! The totality of
complemented subsets of a set with an inequality $X$ is a swap algebra, a
generalisation of a Boolean algebra (see Definition 4.8 in this paper), while
the totality of boolean-valued, partial functions on $X$ is a swap ring, a
generalisation of a Boolean ring (see [44, 18]). The main category of sets in
constructive measure theory is the category111We denote categories as pairs
(Objects, Arrows), as we define later various subcategories of the category
$(\mathrm{\mathbf{Set}},\textnormal{{Fun}})$ of sets and functions.
$(\textnormal{{SetExtIneq}},\textnormal{{StrExtFun}})$ of sets with an
extensional inequality and strongly extensional functions (see Definition
2.4). For such sets the extensional empty set $/{}\square_{X}$ of an object
$X$ is positively defined.

Here we introduce the notions of a $\mathrm{cs}$-topological space and
$\mathrm{cs}$-continuous function between them, as constructive counterparts
to the notions of a topological space and continuous function between
them222The letters $\mathrm{cs}$ refer to complemented subsets.. The
introduced $\mathrm{cs}$-spaces are sets in SetExtIneq together with a so-
called topology of open complemented subsets, or a $\mathrm{cs}$-topology. The
main advantage of these concepts is the preservation of the dualities found in
classical point-set topology. The category
$(\textnormal{{csTop}},\textnormal{{csCont}})$ of $\mathrm{cs}$-spaces and
$\mathrm{cs}$-continuous functions is the constructive counterpart to the
category $(\mathrm{\mathbf{Top}},\textnormal{{Cont}})$ of topological spaces
and continuous functions and a subcategory of
$(\textnormal{{SetExtIneq}},\textnormal{{StrExtFun}})$.

The study of the canonical $\mathrm{cs}$-topology induced by a metric on a set
$X$ in section 6 reveales the importance of “concept-mining” in constructive
mathematics. By that we mean the accommodation of the definition of many
classical concepts, such as the notion of a base for a topology, with
“witnesses” of the related properties. These witnesses are moduli of
continuity, of convergence etc., that instantiate what usually we get
classically from the axiom of choice. The notion of an open set in the
$\mathrm{cs}$-topology induced by a metric (see Definition 9.8) comes with a
modulus of openness that witnesses the main property of a set being open. This
enriched concept of open set in a metric space allows more informative proofs,
from the computational point of view, of facts on metric topologies. Moreover,
the presentation of pointwise and uniform continuity between metric spaces in
section 7, is strongly influenced by the presence of the moduli of openness
associated with open sets. Pointwise continuous functions between metric
spaces inverse open sets together with their moduli of openness in a certain
“pointwise” way, while uniformly continuous functions between metric spaces
inverse open sets together with their moduli of openness in a certain
“uniform” way. Generalising these concepts within the theory of
$\mathrm{cs}$-topological spaces with a given base, the so-called here csb-
spaces, gives us a way to translate pointwise and uniform continuity of
functions between metric spaces to abstract csb-spaces. In this way, the
theory of $\mathrm{cs}$-topological spaces, or of csb-spaces, is not only a
constructive counterpart to classical topology that reveals its computational
content, but also a new theory that is interesting also from the classical
point of view. Pointwise and uniform continuity of functions between
topological spaces can be formulated classically for topologies of open
subsets with a base, in a way similar to that found in section 10. The theory
of $\mathrm{cs}$-spaces introduced here is another major application of
Bishop’s deep idea to work with complemented subsets instead of subsets.
Moreover, it is a non-trivial example of a theory that has its origin to
constructivism and at the same time reveals new concepts, useful to classical
mathematics too. In our view, another such example is the theory of swap
algebras and swap rings, which is also rooted to Bishop’s concept of a
complemented subset and generalises in a new way the notion of a Boolean
algebra.

We structure this paper as follows:

  * •

In section 2 we include a brief introduction to $\mathrm{BST}$, the theory of
sets that accommodates Bishop-style constructive mathematics
$(\mathrm{BISH})$. We also introduce the basic categories of sets with an
extensional inequality and strongly extensional functions that accommodate the
theory of $\mathrm{cs}$-topologies.

  * •

In section 3 we develop the basic theory of (extensional) subsets of a given
set with an extensional inequality. Here we restrict our attention to
extensional subsets i.e., subsets of a set $X$ defined by separation through
an extensional property on $X$. The use of extensional subsets of $X$ only,
and not categorical ones (i.e., pairs $(A,i_{A})$, where $A$ is a set and
$i_{A}\colon A\hookrightarrow X$ is an embedding), allows a smoother
constructive treatment of the empty subset and a calculus of subsets closer to
the classical one. Moreover, we introduce various notions of tightness for an
extensional subset of a set with an extensional inequality
$(X,=_{X},\neq_{X})$. Tight subsets are formed by connecting (weak) negation
of an equality and an inequality with the given inequality and equality.

  * •

In section 4 we present the basic theory of (extensional) complemented subsets
of a given set with an extensional inequality. The basic operations on them
are defined, and their abstraction, the notion of a swap algebra of type (I),
is included.

  * •

In section 5 we introduce the notion of a complemented point, which is the
complemented version of a singleton, and the notion of a canonical
complemented point. The latter is the notion of complemented point that suits
better to the formulation of local versions of topological notions related to
$\mathrm{cs}$-spaces.

  * •

In section 6 we define the canonical $\mathrm{cs}$-topology induced by a
metric on a set $X$, and we introduce moduli of openness for the open subsets
of $X$ with respect to its canonical base of complemented balls. Moduli of
openness are going to be generalised to $\mathrm{cs}$-topological spaces with
a given base and are crucial to our study of continuity.

  * •

In section 7 we explain how pointwise and uniformly continuous functions
between metric spaces inverse open sets together with their given moduli of
openness (Proposition 7.6 and Proposition 7.10, respectively). Conversely, the
inversion of opens together with their moduli implies pointwise continuity
(Proposition 7.7), and under a certain condition, also uniform continuity
(Proposition 7.11). The corresponding constructions are inverse to each other
(Proposition 7.8 and Proposition 7.12, respectively).

  * •

In section 8 we define the notions of a $\mathrm{cs}$-topological space, and
of a $\mathrm{cs}$-continous function between them, the arrow in the category
$(\textnormal{{csTop}},\textnormal{{csCont}})$ of $\mathrm{cs}$-topological
spaces. The clopen complemented subsets of a $\mathrm{cs}$-space form a swap
algebra of type (I) (Corollary 8.5), a fact that is the complemented
counterpart to the Boolean-algebra structure of the clopen subsets of a
standard topological space. The relative $\mathrm{cs}$ topology and the
quotient $\mathrm{cs}$-topology are presented. The formulation of the relative
$\mathrm{cs}$-topology is not identical to the standard relative topology of
open subsets, and the reason behind this slight difference is that a certain
distributivity property of complemented subsets (this is property $(D_{I})$,
given in section 4) cannot be accepted constructively. Instead, Bishop’s
distributivity property for complemented subsets is used to the proof of
Proposition 8.10.

  * •

In section 9 we define the notion of a $\mathrm{cs}$-topology induced by a
base, in a way that generalises the canonical $\mathrm{cs}$-topology induced
by a metric and the base of the complemented balls in section 6 (Remark 9.5).
A base for a $\mathrm{cs}$-topology is a proof-relevant version of the
classical notion of a topology of open subsets, as the definitional properties
of a base are witnessed by the corresponding base-moduli (Definition 9.4). We
call $\mathrm{cs}$-spaces with a base csb-spaces, and these are the
$\mathrm{cs}$-spaces that generalise metric spaces.

  * •

In section 10 we generalise the notions of pointwise and uniform continuity of
functions between metric spaces to pointwise and uniformly continuous
functions between csb-spaces. It is common belief, both in classical and on
constructive mathematics, that uniform continuity between metric spaces has no
direct formulation within topological spaces, and one has to define other
structures, such as uniform spaces, in order to express uniform continuity.
This belief was also one of the reasons why Bishop didn’t expect to find a
useful constructive counterpart to classical topology (see also section 12).
The constructive reformulation though, of a base for a topology and an open
set with respect to that base that reveals all necessary witnessing data and
avoids the axiom of choice offers a solution to this long-standing problem. We
introduce csb-continuous functions i.e., $\mathrm{cs}$-continuous functions
that inverse also the corresponding moduli of openness, and we define
pointwise and uniformly continuous csb-continuous functions in a way that
generalises the definition of pointwise and uniformly continuous functions
between metric spaces (Definition 10.1).

  * •

In section 11 we define the product of two csb-spaces, and we explain how our
choice of bases affect the pointwise or uniform continuity of the projection-
functions (Proposition 11.2, and Proposition 11.4). We also define the weak
csb-topology and show that it is the least csb-topology that turns all given
functions into uniformly continuous ones (Proposition 11.5).

  * •

In section 12 we provide a list of open questions and topics for future work
within the theory of $\mathrm{cs}$-topological spaces.

We work within the extensional framework of _Bishop Set Theory_ (BST), a
minimal extension of Bishop’s theory of sets333The relation of BST to Bishop’s
original theory of sets is discussed in [33], section 1.2. that behaves like a
high-level programming language. In the extensional fragment of BST only
extensional subsets are considered, which are defined by separation on a given
set through an extensional property. Moreover, the totality of extensional
subsets of a set, or the extensional powerset, is considered to be an
impredicative set444The categorical subsets of a set $X$ i.e., arbitrary sets
with an embedding in $X$, form the categorical powerset of $X$, which is a
proper class, as its membership-condition requires quantification over the
universe of predicative sets $\mathbb{V}_{0}$. The relation between the two
powersets involves Myhill’s axiom of non-choice and it is studied in [18]., in
accordance to the (impredicative) Bridges-Richman Set Theory (BRST) in [7, 20,
8]. The type-theoretic interpretation of Bishop sets as setoids is developed
mainly by Palmgren (see e.g., [22]-[25]). Other formal systems for
$\mathrm{BISH}$ are Myhill’s system CST [19] and Aczel’s system CZF [1].
Categorical approaches to Bishop sets are found e.g., in the work of Palmgren
[21] and Coquand [10]. For all notions and results of BST that we use without
explanation or proof we refer to [33, 36, 39, 41]. For all notions and facts
from constructive analysis that we use without explanation or proof, we refer
to [2, 6, 7]. For all notions and facts from classical topology that we use
without explanation or proof, we refer to [12]. In a proof of a theorem we may
write $(\mathrm{INT})$ to indicate that intuitionisitic logic i.e., Ex Falso
quodlibet, is needed. If in a proof the Ex Falso quodlibet is not used, then
our proof is within minimal logic $(\mathrm{MIN})$ (see [48]). If a proof
employs Myhill’s unique choice principle, a very weak form of choice, this is
also indicated accordingly.

##  2 Sets with an extensional inequality

Bishop Set Theory (BST) is an informal, constructive theory of _totalities_
and _assignment routines_ between totalities that accommodates Bishop’s
informal system BISH and serves as an intermediate step between Bishop’s
original theory of sets and an adequate and faithful formalisation of BISH in
Feferman’s sense [13]. Totalities, apart from the basic, undefined set of
natural numbers $\mathbb{N}$, are defined through a membership-condition. The
_universe_ $\mathbb{V}_{0}$ of predicative sets is an open-ended totality,
which is not considered a set itself, and every totality the membership-
condition of which involves quantification over the universe is not considered
a set, but a proper class. _Sets_ are totalities the membership-condition of
which does not involve quantification over $\mathbb{V}_{0}$, and are equipped
with an equality relation i.e., an equivalence relation. An equality relation
$x=_{X}x{{}^{\prime}}$ on a defined set $X$ is defined through a formula
$E_{X}(x,x{{}^{\prime}})$ (see Definition 2.2). Assignment routines are of two
kinds: _non-dependent_ ones and _dependent_ ones.

######  Definition 2.1.

If $(X,=_{X})$ and $(Y,=_{Y})$ are sets, a function $f\colon X\to Y$ is a non-
dependent assignment routine $f\colon X\rightsquigarrow Y$ i.e., for every
$x\in X$ we have that $f(x)\in Y$, such that $x=_{X}x{{}^{\prime}}\Rightarrow
f(x)=_{Y}f(x{{}^{\prime}})$, for every $x,x{{}^{\prime}}\in X$. A function
$f:X\to Y$ is an embedding, if for all $x,x^{\prime}$ in $X$ we have that
$f(x)=_{Y}f(x^{\prime})$ implies $x=_{X}x^{\prime}$, and we write
$f:X\hookrightarrow Y$, while it is a surjection, if $\forall_{y\in
Y}\exists_{x\in X}(f(x)=_{Y}y)$. We denote by $\mathbb{F}(X,Y)$ the set of
functions from $X$ to $Y$, and by $\mathrm{id}_{X}$ the identity function on
$X$. Let $(\mathrm{\mathbf{Set}},\textnormal{{Fun}})$ be the category of sets
and functions, $(\mathrm{\mathbf{Set}},\textnormal{{Emb}})$ its subcategory
with embeddings and $(\mathrm{\mathbf{Set}},\textnormal{{Surj}})$ its
subcategory with surjections. Two sets are equal in $\mathbb{V}_{0}$ if there
is $g\colon Y\to X$, such that555With this equality the universe in
$\mathrm{BST}$ can be called _univalent_ in the sense of Homotopy Type Theory
[47, 50], as, by definition, an equivalence between sets is an equality.
Similarly, the type-theoretic function-extensionality axiom is incorporated in
BST as the canonical equality of the function space. $g\circ
f=_{\mathbb{F}(X,X)}\mathrm{id}_{X}$ and $f\circ
g=_{\mathbb{F}(Y,Y)}\mathrm{id}_{Y}$.

In $\mathrm{BST}$ a set is usually equipped not only with a given equality,
but also with a given inequality relation, $x\neq_{X}x{{}^{\prime}}$ defined
through a formula $I_{X}(x,x{{}^{\prime}})$ (see Definition 2.2). The
primitive set of natural numbers ${\mathbb{N}}$ has a given equality
$=_{{\mathbb{N}}}$ and inequality $\neq_{{\mathbb{N}}}$. We consider
$s\neq_{{\mathbb{N}}}t$ as primitive, rather than defined, as one could,
through weak negation, as we want to avoid the use of weak negation in the
foundations of BISH. For every basic or defined set in $\mathrm{BST}$ we have
variables of that set. Next we define formulas within $\mathrm{BST}$. In the
unpublished work [3] of Bishop formulas of $\mathrm{BISH}$ are translated in
his fofrmal system $\Sigma$ in almost exactly the same way.

######  Definition 2.2 (Formulas in $\mathrm{BST}$).

Prime formulas: $s=_{{\mathbb{N}}}t$, $s\neq_{{\mathbb{N}}}t$, where
$s,t\in{\mathbb{N}}$.
Complex formulas: If $A,B$ are formulas, then $A\vee B,A\wedge B,A\Rightarrow
B$ are formulas, and if $S$ is a set and $\phi(x)$ is a formula, for every
variable $x$ of set $S$, then $\exists_{x\in S}\big{(}\phi(x)\big{)}$ and
$\forall_{x\in S}\big{(}\phi(x)\big{)}$ are formulas. Let
$\top:=0\neq_{{\mathbb{N}}}1,\bot:=0=_{{\mathbb{N}}}1$ and $\neg
A:=A\Rightarrow\bot$.

Constructively, $\neg A$ has a weak behaviour, as the negation of a
conjunction $\neg(A\wedge B)$ does not generally imply the disjunction $\neg
A\vee\neg B$, and similarly the negation of a universal formula
$\neg\forall_{x}A(x)$ does not generally imply the existential formula
$\exists_{x}\neg A(x)$. Even if $A$ and $B$ are stable i.e., $\neg\neg A\to A$
and $\neg\neg B\to B$, we only get $\neg(A\wedge B)\vdash\neg\neg(\neg
A\vee\neg B)$ and $\neg\forall_{x}A(x)\vdash\neg\neg\exists_{x}\neg A(x)$,
where $\vdash$ is the derivability relation in minimal logic. For this reason,
$\neg A$ is called the weak negation of $A$, which, according to Rasiowa [46],
p. 276, is not constructive, exactly due to its aforementioned behaviour. The
critique of weak negation in constructive mathematics $(\mathrm{CM})$ goes
back to Griss [14]. Despite the use of weak negation in Brouwer’s
intuitionistic mathematics and Bishop’s system $\mathrm{BISH}$, both, Brouwer
and Bishop, developed a positive and strong approach to many classically
negatively defined concepts. Recently, Shulman [49] showed that most of the
strong concepts of $\mathrm{BISH}$ “arise automatically from an “antithesis”
translation of affine logic into intuitionistic logic via a “Chu/Dialectica
construction”. Motivated by this work of Shulman, and in relation to our
reconstruction of the theory of sets underlying $\mathrm{BISH}$ (see [33, 36,
39] and [44, 18]), we develop in [43] a treatment of strong negation within
$\mathrm{BST}$, arriving in a heuristic method for the definition of strong
concepts in $\mathrm{BISH}$, similar to Shulman’s. For that, the equivalences
occurring in the axiom schemata related to strong negation in formal theories
of strong negation become the definitional clauses of the recursive definition
of $A^{\mathbf{N}}$, with respect to the above inductive definition of
formulas $A$ in $\mathrm{BST}$. In [17], strong negation is incorporated in
the theory of computable functionals TCF, extending the following recursive
definition of strong negation of formulas to inductively and coinductively
defined predicates.

######  Definition 2.3 (Strong negation in $\mathrm{BST}$).

Strong negation $A^{\mathbf{N}}$ of a formula $A$ in $\mathrm{BST}$ is defined
by the following clauses:
$(\mathrm{SN}_{1})$ For prime formulas related to the primitive set
$({\mathbb{N}},=_{{\mathbb{N}}},\neq_{{\mathbb{N}}})$ let

$\big{(}s=_{{\mathbb{N}}}t\big{)}^{\mathbf{N}}:=s\neq_{{\mathbb{N}}}t\ \ \&\ \
\big{(}s\neq_{{\mathbb{N}}}t\big{)}^{\mathbf{N}}:=s=_{{\mathbb{N}}}t.$

If $A,B$ are complex formulas in $\mathrm{BST}$, let
$(\mathrm{SN}_{2})\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ (A\vee B)^{\mathbf{N}}:=A^{\mathbf{N}}\wedge B^{\mathbf{N}}$,
$(\mathrm{SN}_{3})\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ (A\wedge B)^{\mathbf{N}}:=A^{\mathbf{N}}\vee B^{\mathbf{N}}$,
$(\mathrm{SN}_{4})\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ (A\Rightarrow B)^{\mathbf{N}}:=A\wedge B^{\mathbf{N}}$.
If $S$ is a set and $\phi(x)$ is a formula in $\mathrm{BST}$, where $x$ is a
varriable of $S$, let

$(\mathrm{SN}_{5})\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \big{(}\exists_{x\in
S}\phi(x)\big{)}^{\mathbf{N}}:=\forall_{x\in
S}\big{(}\phi(x)^{\mathbf{N}}\big{)},\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $ $(\mathrm{SN}_{6})\ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\big{(}\forall_{x\in S}\phi(x)\big{)}^{\mathbf{N}}:=\exists_{x\in
S}\big{(}\phi(x)^{\mathbf{N}}\big{)}.\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $

We also define $A^{\mathbf{NN}}:=(A^{\mathbf{N}})^{\mathbf{N}}$. If $A,B$ are
formulas in $\mathrm{BST}$, their strong implication666Strong implication is
defined by Rasiowa in [46] within a formal system of constructive logic with
strong negation. is defined by

$A\Rrightarrow B:=(A\Rightarrow B)\wedge(B^{\mathbf{N}}\Rightarrow
A^{\mathbf{N}}).$

######  Definition 2.4.

If $(X,=_{X})$ is a set, let the following formulas with respect to a relation
$x\neq_{X}y:$
$(\textnormal{{Ineq}}_{1})\ \forall_{x,y\in X}\big{(}x=_{X}y\ \&\
x\neq_{X}y\Rightarrow\bot\big{)}$,
$(\textnormal{{Ineq}}_{2})\ \forall_{x,x{{}^{\prime}},y,y{{}^{\prime}}\in
X}\big{(}x=_{X}x{{}^{\prime}}\ \&\ y=_{X}y{{}^{\prime}}\ \&\
x\neq_{X}y\Rightarrow x{{}^{\prime}}\neq_{X}y{{}^{\prime}}\big{)}$,
$(\textnormal{{Ineq}}_{3})\ \forall_{x,y\in
X}\big{(}\neg(x\neq_{X}y)\Rightarrow x=_{X}y\big{)}$,
$(\textnormal{{Ineq}}_{4})\forall_{x,y\in X}\big{(}x\neq_{X}y\Rightarrow
y\neq_{X}x\big{)}$,
$(\textnormal{{Ineq}}_{5})\ \forall_{x,y\in
X}\big{(}x\neq_{X}y\Rightarrow\forall_{z\in X}(z\neq_{X}x\ \vee\
z\neq_{X}y)\big{)}$,
$(\textnormal{{Ineq}}_{6})\ \forall_{x,y\in X}\big{(}x=_{X}y\vee
x\neq_{X}y\big{)}$.
If $\textnormal{{Ineq}}_{1}$ is satisfied, we call $\neq_{X}$ an inequality on
$X$, and the structure $\mathcal{X}:=(X,=_{X},\neq_{X})$ a set with an
inequality. If $(\textnormal{{Ineq}}_{6})$ is satisfied, then $\mathcal{X}$ is
discrete, if $(\textnormal{{Ineq}}_{2})$ holds, $\neq_{X}$ is called
extensional, and if $(\textnormal{{Ineq}}_{3})$ holds, it is tight. If it
satisfies $(\textnormal{{Ineq}}_{4})$ and $(\textnormal{{Ineq}}_{5})$, it is
called an apartness relation on $X$.

The primitive inequality $\neq_{{\mathbb{N}}}$ is a discrete, tight apartness
relation. In many cases, the inequality on a set is equivalent to the strong
negation of its equality and vice versa.

######  Definition 2.5.

If $\mathcal{X}:=(X,=_{X},\neq_{X})$ and $\mathcal{Y}:=(Y,=_{Y},\neq_{Y})$ are
sets with inequality, a function $f\colon X\to Y$ is strongly extensional, if
$f(x)\neq_{Y}f(x{{}^{\prime}})\Rightarrow x\neq_{X}x{{}^{\prime}}$, for every
$x,x{{}^{\prime}}\in X$, and it is an injection, if the converse implication
(also777Here we consider injections that are already strongly extensional
functions.) holds i.e., $x\neq_{X}x{{}^{\prime}}\Rightarrow
f(x)\neq_{Y}f(x{{}^{\prime}})$, for every $x,x{{}^{\prime}}\in X$. A strong
injection is an injection that is also an embedding888Classically, the
negation of equality $\neg(x=_{X}x{{}^{\prime}})$ is used instead of
$x\neq_{X}x{{}^{\prime}}$, and the corresponding implications are equivalent
with the use of double negation elimination. Constructively, we need to treat
these notions separately. Notice though, that each (constructive) implication
follows from the other by using contraposition with respect to strong
negation, if the inequality on $X$ is the strong negation of its equality and
vice versa. i.e., $x\neq_{X}x{{}^{\prime}}\Rightarrow
f(x)\neq_{Y}f(x{{}^{\prime}})$ and $f(x)=_{Y}f(x{{}^{\prime}})\Rightarrow
x=_{X}x{{}^{\prime}}$, for every $x,x{{}^{\prime}}\in X$. Let
$(\textnormal{{SetIneq}},\textnormal{{StrExtFun}})$ be the category of sets
with an inequality and strongly extensional functions, let
$(\textnormal{{SetExtIneq}},\textnormal{{StrExtFun}})$ be its subcategory with
sets with an extensional inequality, and
$(\textnormal{{SetIneq}},\textnormal{{Inj}})$ and
$(\textnormal{{SetExtIneq}},\textnormal{{Inj}})$ the corresponding
subcategories with $($strongly extensional$)$ injections. Moreover, let
$(\textnormal{{SetIneq}},\textnormal{{StrInj}})$ and
$(\textnormal{{SetExtIneq}},\textnormal{{StrInj}})$ be the corresponding
subcategories with strong injections.

######  Definition 2.6.

Let $\mathcal{X}:=(X,=_{X},\neq_{X})$ and $\mathcal{Y}:=(Y,=_{Y},\neq_{Y})$ be
sets with inequalities. The canonical inequalities on the product $X\times Y$
and the function space $\mathbb{F}(X,Y)$ are given, respectively, by

$(x,y)\neq_{X\times Y}(x{{}^{\prime}},y{{}^{\prime}}):\Leftrightarrow
x\neq_{X}x{{}^{\prime}}\vee y\neq_{Y}y{{}^{\prime}},$
$f\neq_{\mathbb{F}(X,Y)}g:\Leftrightarrow\exists_{x\in
X}\big{[}f(x)\neq_{Y}g(x)\big{]}.$

Clearly, the canonical inequalities on $X\times Y$ and $\mathbb{F}(X,Y)$ are
formed by the strong negation of their canonical equalities, respectively. The
projections $\textnormal{{pr}}_{X},\textnormal{{pr}}_{Y}$ associated to
$X\times Y$ are strongly extensional functions. It is not easy to give
examples of non strongly extensional functions, although we cannot accept in
$\mathrm{BISH}$ that all functions are strongly extensional. E.g., the strong
extensionality of all functions from a metric space to itself is equivalent to
Markov’s principle (see [11], p. 40). Even to show that a constant function
between sets with an inequality is strongly extensional, one needs
intuitionistic, and not minimal, logic. An apartness relation $\neq_{X}$ on a
set $(X,=_{X})$ is always extensional (see [33], Remark 2.2.6, p. 11).

######  Definition 2.7.

The canonical inequality on the set of reals ${\mathbb{R}}$ is given by
$a\neq_{{\mathbb{R}}}b:\Leftrightarrow|a-b|>0\Leftrightarrow a>b\vee a<b$,
which is a special case of the canonical inequality on a metric space $(Z,d)$,
given by $z\neq_{(Z,d)}z{{}^{\prime}}:\Leftrightarrow d(z,z{{}^{\prime}})>0$.
If $(X,=_{X})$ is a set and $F\subseteq\mathbb{F}(X)$, the set of real-valued
functions on $X$, the inequality on $X$ induced by $F$ is defined by
$x\neq_{(X,F)}x{{}^{\prime}}:\Leftrightarrow\exists_{f\in
F}\big{(}f(x)\neq_{{\mathbb{R}}}f(x{{}^{\prime}})\big{)}.$

The inequalities $a\neq_{{\mathbb{R}}}b$ and $z\neq_{(Z,d)}z{{}^{\prime}}$ are
tight apartness relations. E.g., cotransitivity of
$z\neq_{(Z,d)}z{{}^{\prime}}$ is shown by the fact that
$d(z,z{{}^{\prime\prime}})+d(z{{}^{\prime\prime}},z{{}^{\prime}})\geq
d(z,z{{}^{\prime}})>0$, and if $a+b>0$ in ${\mathbb{R}}$, then $a>0$ or $b>0$
(see [6], p. 26). The inequality $x\neq_{(X,F)}y$ is an apartness relation,
which is tight if and only if

$\forall_{f\in
F}\big{(}f(x)=_{{\mathbb{R}}}f(x{{}^{\prime}})\big{)}\Rightarrow
x=_{X}x{{}^{\prime}},$

for every $x,x{{}^{\prime}}\in X$. No negation of some sort is used in the
definition of the inequality $x\neq_{(X,F)}x{{}^{\prime}}$, in the proof of
its extensionality, while the last implication above can be seen as completely
positive formulation of its tightness. If $F$ is a Bishop topology of
functions (see [26, 35, 36, 40, 42]), then $x\neq_{(X,F)}x{{}^{\prime}}$ is
the canonical inequality of a Bishop space. The inequality
$a\neq_{{\mathbb{R}}}b$ is equivalent to such an inequality induced by
functions, as $a\neq_{{\mathbb{R}}}b\Leftrightarrow
a\neq_{({\mathbb{R}},\mathrm{Bic}({\mathbb{R}}))}b$, where
$\mathrm{Bic}({\mathbb{R}})$ is the topology of Bishop-continuous functions of
type ${\mathbb{R}}\to{\mathbb{R}}$ (see [26], Proposition 5.1.2.). Notice that
all Bishop-continuous functions of type ${\mathbb{R}}\to{\mathbb{R}}$,
actually all pointwise continuous functions of this type, are strongly
extensional (see [26], 2.3.12(i), p. 26), a fact that is generalised in Remark
7.2. By its extensionality, an inequality induced by functions provides a
(fully) positive definition of the extensional empty subset, and of the
extensional complement $X_{P}^{\neq_{X}}$ of an extensional subset $X_{P}$ of
$X$ (see Definition 3.2 and Definition 3.3). The following facts are used in
section 5 and are straightforward to prove.

######  Proposition 2.8.

Let $\mathcal{X},\mathcal{Y},f\colon X\to Y$ in
$(\textnormal{{SetExtIneq}},\textnormal{{StrExtFun}})$ with a left inverse
$g_{l}\colon Y\to X$

$Y$$X$$Y$.$g_{l}$$f$$\mathrm{id}_{Y}$

(i) $f$ is a surjection, and $g_{l}$ is a strong injection.
(ii) If $f$ is an injection, then $g_{l}$ is strongly extensional.
(iii) If $g_{l}$ is strongly extensional and surjective, then $f$ is an
injection.

######  Proposition 2.9.

Let $\mathcal{X},\mathcal{Y},f\colon X\to Y$ in
$(\textnormal{{SetExtIneq}},\textnormal{{StrExtFun}})$ with a right inverse
$g_{r}\colon Y\to X$

$X$$Y$$X$.$f$$g_{r}$$\mathrm{id}_{X}$

(i) $g_{r}$ is a surjection, and if $f$ is a surjection, then $g_{r}$ is an
embedding.
(ii) If $g_{r}$ is strongly extensional, then $f$ is an injection.
(iii) If $f$ is a surjection and an injection, then $g_{r}$ is strongly
extensional.

If a function $f$ has a left $g_{l}$ and a right inverse $g_{r}$, then it is
immediate to show that $g_{l}=_{\mathbb{F}(Y,X)}g_{r}$.

######  Proposition 2.10.

Let $\mathcal{X},\mathcal{Y},f\colon X\to Y$ in
$(\textnormal{{SetExtIneq}},\textnormal{{StrExtFun}})$ with an inverse
$g\colon Y\to X$

$Y$$X$$Y$$X$.$g$$f$$g$$\mathrm{id}_{Y}$$\mathrm{id}_{X}$

(i) $f$ is a surjection and $g$ is a surjective strong injection.
(ii) $f$ is an injection if and only if $g$ is strongly extensional.

######  Proposition 2.11.

Let $\mathcal{X},\mathcal{Y},f\colon X\to Y$ in
$(\textnormal{{SetExtIneq}},\textnormal{{Fun}})$ with a left inequality-
adjoint $g\colon Y\to X$, in symbols $g\dashv f$ i.e., for every $x\in X$ and
$y\in Y$ the following condition is satisfied:

$g(y)\neq_{X}x\Leftrightarrow y\neq_{Y}f(x).$

(i) If $f$ is a surjection and an injection, then $g$ is an injection, and,
dually, if $g$ is a surjection and an injection, then $f$ is an injection.
(ii) If $f$ is a strongly extensional surjection, then $g$ is strongly
extensional, and, dually, if $g$ is a strongly extensional surjection, then
$f$ is strongly extensional.

Clearly, if $f\colon X\to Y$ has a left (right) inverse one of the two
implications of the adjointness-condition holds, and if $f$ has an inverse
$g$, then $g\dashv f$. We can organise the above notions of functions into
certain subcategories of $(\textnormal{{SetIneq}},\textnormal{{Fun}})$.

######  Definition 2.12.

Let $(\mathrm{\mathbf{Set}},\textnormal{{LeftInv}})$ be the category of sets
with a left inverse, $(\mathrm{\mathbf{Set}},\textnormal{{RightInv}})$ the
category of sets with functions with a right inverse, and
$(\mathrm{\mathbf{Set}},\textnormal{{Inv}})$ the category of sets with
invertible functions. The categories
$(\textnormal{{SetIneq}},\textnormal{{LeftInv}})$,
$(\textnormal{{SetIneq}},\textnormal{{RightInv}})$,
$(\textnormal{{SetIneq}},\textnormal{{Inv}})$, and their subcategories
$(\textnormal{{SetExtIneq}},\textnormal{{LeftInv}})$,
$(\textnormal{{SetExtIneq}},\textnormal{{RightInv}})$, and
$(\textnormal{{SetExtIneq}},\textnormal{{Inv}})$ are defined accordingly. Let
$(\textnormal{{SetIneq}},\textnormal{{Adj}})$ be the category of sets with
inequality and strongly extensional functions with a left inequality-adjoint.
The category $(\textnormal{{SetExtIneq}},\textnormal{{Adj}})$ is defined
similarly.

##  3 Extensional subsets

Here we work only with extensional subsets, as in Bridges-Richman Set Theory.
The use of extensional subsets only allows a smoother treatment of the
(extensional) empty subset of a set, and hence a calculus of subsets closer to
that of subsets within classical logic. The role of Myhill’s axiom of non-
choice to the relation between extensional and categorical subsets is studied
in [18].

######  Definition 3.1 (Extensional subsets).

A formula $P(x)$, where $x$ is a variable of set $(X,=_{X})$, is an
extensional property999Notice that in $\mathrm{MLTT}$ a property on a type $X$
is described as a type family $P\colon X\to\mathcal{U}$ over $X$, where
$\mathcal{U}$ is a universe and $X\colon\mathcal{U}$, and it is always
extensional through the corresponding transport-term (see [50], section 2.3).
on $X$, if

$\forall_{x,y\in X}\big{(}[x=_{X}y\ \&\ P(x)]\Rightarrow P(y)\big{)}.$

The corresponding totality $X_{P}$ defined by the separation scheme is called
an extensional subset of $X$, if its equality is inherited from $=_{X}$. If
$\neq_{X}$ is a given inequality on $X$, then the canonical inequality
$\neq_{X_{P}}$ on $X_{P}$ is inherited from $\neq_{X}$. The totality of
extensional subsets of $X$ is denoted by $\mathcal{E}(X)$. If
$X_{P},X_{Q}\in\mathcal{E}(X)$, let $X_{P}\subseteq
X_{Q}:\Leftrightarrow\forall_{x\in X}\big{(}P(x)\Rightarrow Q(x)\big{)}$ and
$X_{P}=_{\mathcal{E}(X)}X_{Q}:\Leftrightarrow X_{P}\subseteq X_{Q}\ \&\
X_{Q}\subseteq X_{P}$. We may avoid writing the extensional property $P(x)$
determining an extensional subset $A$ of $X$, and in this case we simply write
$A\subseteq X$.

Notice that no quantification over the universe $\mathbb{V}_{0}$ is required
in the membership condition of $\mathcal{E}(X)$. In accordance to the
fundamental distinction between judgments and propositions due to Martin-Löf,
if $A,B\in\mathcal{E}(X)$, the inclusion $A\subseteq B$ is a formula that does
not employ the membership symbol i.e., we do not say that for all $x\in X$ if
$x\in A$, then $x\in B$, as such a definition would interpret the judgments
$x\in A,x\in B$ as formulas. If $A:=X_{P}$ and $B:=X_{Q}$, we only need to
prove $P(x)\Rightarrow Q(x)$, for every $x\in X$. There are non-extensional
properties on a set i.e., formulas $P(x)$, where $x$ is a variable of the set
$X$, such that $P(x)$ and $x=_{X}y$ do not imply $P(y)$. For example, let
$n\in{\mathbb{N}}$, $q\in\mathbb{Q}$ and $P_{q}(x)$, where $x$ is a variable
of set ${\mathbb{R}}$, defined by $P_{q}(x):=x_{n}=_{\mathbb{Q}}q.$ If
$y\in{\mathbb{R}}$ such that $y=_{{\mathbb{R}}}x$, then it is not necessary
that $y_{n}=_{\mathbb{Q}}q$, if $x_{n}=_{\mathbb{Q}}q$. A set $X$ is an
extensional subset of itself, in the sense that it is equal in
$\mathbb{V}_{0}$ to the extensional subset $X_{=_{X}}:=\\{x\in X\mid
x=_{X}x\\}.$ The sets $\mathbb{1}$ and $\mathbb{2}$ are defined as extensional
subsets of the primitive set ${\mathbb{N}}$:

$\mathbb{1}:=\\{x\in{\mathbb{N}}\mid x=_{{\mathbb{N}}}0\\}=:\\{0\\},\ \ \ \ \
\mathbb{2}:=\\{x\in{\mathbb{N}}\mid x=_{{\mathbb{N}}}0\ \vee
x=_{{\mathbb{N}}}1\\}=:\\{0,1\\}$

As an equality $=_{X}$ is extensional on $X\times X$, the diagonal
$D(X,=_{X}):=\\{(x,y)\in X\times X\mid x=_{X}y\\}$ of $X$ is an extensional
subset of $X\times X$. In the following definition of the extensional empty
subset of a set $X$ we do not require $X$ to be inhabited, as Bishop does in
[2], p. 65, for the categorical empty subset. We only require that $X$ is
equipped with an extensional inequality.

######  Definition 3.2 (Extensional empty subset).

If $\mathcal{X}:=(X,=_{X},\neq_{X})$ in in SetExtIneq, then

$/{}\square_{X}:=\\{x\in X\mid x\neq_{X}x\\}$

is the extensional empty subset of $\mathcal{X}$. We call
$X_{P}\in\mathcal{E}(X)$ empty, if $X_{P}\subseteq/{}\square_{X}$.

Notice that within $\mathrm{INT}$ the inclusion $\ /{}\square_{X}\subseteq
X_{P}$ holds, for every extensional property $P(x)$ on $X$. The extensionality
of an equality $=_{X}$ implies that the inequality $\neg(x=_{X}y)$ on
$(X,=_{X})$ is extensional, with associated weak empty subset the extensional
subset

$\\{x\in X\mid\neg(x=_{X}x)\\}.$

Although this definition employs negation, we can define inequalities on a
set, as we saw in Definition 2.4, and hence associated empty subsets, in a
completely positive way. Next we define the basic operations on extensional
subsets101010In [18] a different notation is used for these operations, in
order to be distinguished from the corresponding operations on categorical
subsets. As here we employ only extensional subsets, we use for them the
standard notation for the opeartions on subsets..

######  Definition 3.3.

If $(X,=_{X}),(Y,=_{Y})\in\mathrm{\mathbf{Set}}$,
$A:=X_{P},B:=X_{Q}\in\mathcal{E}(X)$, $C:=Y_{R}\in\mathcal{E}(Y)$ and $f\colon
X\to Y$, let the following operations on extensional subsets:

$A\cup B:=\\{x\in X\mid P(x)\vee Q(x)\\},\ \ \ \ \ A\cap B:=\\{x\in X\mid
P(x)\wedge Q(x)\\},$ $f(A):=\big{\\{}y\in Y\mid\exists_{x\in
X_{P}}\big{(}f(x)=_{Y}y\big{)}\big{\\}},\ \ \ \ \ f^{-1}(C):=\big{\\{}x\in
X\mid\exists_{y\in Y_{R}}\big{(}f(x)=_{Y}y\big{)}\big{\\}},$ $A\times
C:=\big{\\{}((x{{}^{\prime}},y{{}^{\prime}})\in X\times Y\mid\exists_{x\in
X_{P}}\exists_{y\in Y_{R}}\big{(}x{{}^{\prime}}=_{X}x\wedge
y{{}^{\prime}}=_{Y}y\big{)}\big{\\}}.$

If $(I,=_{I})$ is a set, a family of extensional subsets of $X$ indexed by $I$
is an assignment routine $\lambda_{0}:I\rightsquigarrow\mathbb{V}_{0}$, such
that for every $i,j\in I$ we have that $\lambda_{0}(i):=X_{P_{i}}$, where
$P_{i}(x)$ is an extensional property on $X$, and if $i=_{I}j$, then
$X_{P_{i}}=_{\mathcal{E}(X)}X_{P_{j}}$. For simplicity we denote such a family
by $\big{(}X_{P_{i}}\big{)}_{i\in I}$. Its union and intersection are given by

$\bigcup_{i\in I}\lambda_{0}(i):=\big{\\{}x\in X\mid\exists_{i\in
I}\big{(}P_{i}(x)\big{)}\big{\\}},\ \ \ \ \ \bigcap_{i\in
I}\lambda_{0}(i):=\big{\\{}x\in X\mid\forall_{i\in
I}\big{(}P_{i}(x)\big{)}\big{\\}}.$

Alternatively, if $F(X_{S})$ is an extensional property on $\mathcal{E}(X)$
and $\mathcal{F}:=\\{X_{S}\in\mathcal{E}(X)\mid F(X_{S})\\},$ let

$\bigcup\mathcal{F}:=\big{\\{}x\in
X\mid\exists_{X_{S}\in\mathcal{F}}\big{(}S(x)\big{)}\big{\\}},\ \ \ \ \
\bigcap\mathcal{F}:=\big{\\{}x\in
X\mid\forall_{X_{S}\in\mathcal{F}}\big{(}S(x)\big{)}\big{\\}}.$

If $\neq_{X}$ is an extensional inequality on $X$, let the extensional
complement $A^{\neq_{X}}$ of $A$, defined by

$A^{\neq_{X}}:=\big{\\{}x\in X\mid\forall_{y\in
X_{P}}\big{(}x\neq_{X}y)\big{)}\big{\\}}.$

Notice that the extensionality of $P(x),Q(x)$ and $R(y)$, together with the
preservation of equalities by a function, imply the extensionality of the
formulas

$(P\vee Q)(x):=P(x)\vee Q(x),\ \ \ \ \ (P\wedge Q)(x):=P(x)\wedge Q(x),$
$[f[P]](y):=\exists_{x\in X_{P}}\big{(}f(x)=_{Y}y\big{)},\ \ \ \ \
[f^{-1}[R]](x):=\exists_{y\in Y_{R}}\big{(}f(x)=_{Y}y\big{)},$ $[P\times
R](x,y):=\exists_{x{{}^{\prime}}\in X_{P}}\exists_{y{{}^{\prime}}\in
Y_{R}}\big{(}x{{}^{\prime}}=_{X}x\wedge y{{}^{\prime}}=_{Y}y\big{)}.$

The extensionality of $P_{i}(x)$, for every $i\in I$, implies the
extensionality of the formulas

$\bigg{(}\bigcup_{i\in I}P_{i}\bigg{)}(x):=\exists_{i\in
I}\big{(}P_{i}(x)\big{)},\ \ \ \ \ \bigg{(}\bigcap_{i\in
I}P_{i}\bigg{)}(x):=\forall_{i\in I}\big{(}P_{i}(x)\big{)}.$

Similalrly, the extensionality of $S$, for every $X_{S}\in\mathcal{F}$,
implies the extensionality of the formulas

$\bigg{(}\bigcup\mathcal{F}\bigg{)}(x):=\exists_{X_{S}\in\mathcal{F}}\big{(}S(x)\big{)},\
\ \ \ \
\bigg{(}\bigcap\mathcal{F}\bigg{)}(x):=\forall_{X_{S}\in\mathcal{F}}\big{(}S(x)\big{)}.$

Clearly, the extensionality of $\neq_{X}$ implies the extensionality of the
property

$[P^{\neq_{X}}](x):=\forall_{y\in X_{P}}\big{(}x\neq_{X}y)\big{)}.$

The usual properties of the inverse and direct image of subsets hold. Next we
mention only a few.

######  Proposition 3.4.

Let $\mathcal{X},\mathcal{Y},\mathcal{Z}$ in SetExtIneq, $A,B\subseteq X$,
$C,D\subseteq Y$, $f\colon X\to Y$, and $g\colon Y\to Z$.
(i) If $f$ is strongly extensional, then
$f^{-1}(/{}\square_{Y})=_{\mathcal{E}(X)}/{}\square_{X}$.
(ii) If $f$ is an injection, then
$f(/{}\square_{X})=_{\mathcal{E}(Y)}/{}\square_{Y}$.
(iii) $f^{-1}(C\cup D)=_{\mathcal{E}(X)}f^{-1}(C)\cup f^{-1}(D)$.
(iv) $f^{-1}(C\cap D)=_{\mathcal{E}(X)}f^{-1}(C)\cap f^{-1}(D)$.
(v) If ${\mathcal{H}}$ is an extensional subset of $\mathcal{E}(Y)$ and
$f^{-1}({\mathcal{H}}):=\\{f^{-1}(H)\mid H\in{\mathcal{H}}\\}$, then

$f^{-1}\bigg{(}\bigcup{\mathcal{H}}\bigg{)}=_{{\mathcal{E}(X)}}\bigcup
f^{-1}({\mathcal{H}}),\ \ \ \
f^{-1}\bigg{(}\bigcap{\mathcal{H}}\bigg{)}=_{{\mathcal{E}(X)}}\bigcap
f^{-1}({\mathcal{H}}).$

(vi) $f(A\cup B)=_{\mathcal{E}(Y)}f(A)\cup f(B)$.
(vii) $f(A\cap B)\subseteq f(A)\cap f(B)$.
(viii) If ${\mathcal{G}}$ is an extensional subset of $\mathcal{E}(X)$ and
$f({\mathcal{G}}):=\\{f(G)\mid G\in{\mathcal{G}}\\}$, then

$f\bigg{(}\bigcup{\mathcal{G}}\bigg{)}=_{{\mathcal{E}(Y)}}\bigcup
f({\mathcal{G}}),\ \ \ \ f\bigg{(}\bigcap{\mathcal{G}}\bigg{)}\subseteq\bigcap
f({\mathcal{G}}).$

(ix) $A\subseteq f^{-1}(f(A))$ and $f(f^{-1}(C))\subseteq C$.
(x) $f(f^{-1}(C)\cap A)=_{\mathcal{E}(Y)}C\cap f(A)$, and
$f(f^{-1}(C))=_{\mathcal{E}(Y)}C\cap f(X)$.
(xi) $A\times(C\cup D)=_{\mathcal{E}(X\times Y)}(A\times C)\cup(A\times D)$.
(xii) $A\times(C\cap D)=_{\mathcal{E}(X\times Y)}(A\times C)\cap(A\cap D)$.
(xiii) $A\times(C-D)=_{\mathcal{E}(X\times Y)}(A\times C)-(A\cap D)$.
(xiv) $A=_{\mathcal{E}(X)}f^{-1}(f(A))$, for every $A\in\mathcal{E}(X)$, if
and only if $f$ is an embedding.
(xv) $C=_{\mathcal{E}(Y)}f(f^{-1}(C))$, for every $C\in\mathcal{E}(Y)$, if and
only if $f$ is a surjection.
(xvi) $f(A\cap B)=_{\mathcal{E}(Y)}f(A)\cap f(B)$, for every
$A,B\in\mathcal{E}(X)$, if and only if $f$ is an embedding.
(xvii) If $f$ is an embedding and ${\mathcal{G}}$ is an extensional subset of
$\mathcal{E}(X)$, then
$f\big{(}\bigcap{\mathcal{G}}\big{)}=_{\mathcal{E}(Y)}\bigcap
f({\mathcal{G}})$.
(xviii) If $H\subseteq Z$, then $(g\circ
f)^{-1}(H)=_{\mathcal{E}(X)}f^{-1}(g^{-1}(H))$.
(xix) If $(g\circ f)(A)=_{\mathcal{E}(Z)}g(f(A))$.

###### Proof.

We show only (i) and (ii), and the rest follow in a straightforward way.
(i) Clearly, within $\mathrm{INT}$ we have that $/{}\square_{X}\subseteq
f^{-1}(/{}\square_{Y})$. Actually, if $f$ is an injection this inclusion is
shown trivially within $\mathrm{MIN}$. The converse inclusion is shown within
$\mathrm{MIN}$ as follows: if $x\in f^{-1}(/{}\square_{Y})$, let $y\in Y$ such
that $y\neq_{Y}y$ and $f(x)=_{Y}y$. By the extensionality of $\neq_{Y}$ we get
$f(x)\neq_{Y}f(x)$, and by strong extensionality of $f$ we conclude that
$x\neq_{X}x$ i.e., $x\in/{}\square_{X}$.
(ii) Within $\mathrm{INT}$ we have that $/{}\square_{Y}\subseteq
f(/{}\square_{X})$. Actually, if $f$ is only a strongly extensional
surjection, then this inclusion is shown easily within $\mathrm{MIN}$. The
converse inclusion is shown within $\mathrm{MIN}$ as follows: by definition
$f(/{}\square_{X}):=\\{y\in Y\mid\exists_{x\in\
{/{}\square_{X}}}(f(x)=_{Y}y)\\}$. Let $y\in Y$ and $x\in/{}\square_{X}$, such
that $f(x)=_{Y}y$. As $x\neq_{X}x$ and $f$ is an injection, we get
$f(x)\neq_{Y}f(x)$, and by the extensionality of $\neq_{Y}$ we get
$y\neq_{Y}y$. ∎

The inclusions in Proposition 3.5(i, ii) hold trivially within $\mathrm{INT}$,
but under certain conditions on $\neq_{X}$ they are also provable within
$\mathrm{MIN}$.

######  Proposition 3.5.

Let $\mathcal{X},\mathcal{Y}$ in SetExtIneq, $A,B,A_{i}\subseteq X$, for every
$i\in I$, $C,D\subseteq Y$, and $f\colon X\to Y$.
(i) $(\mathrm{MIN})$ $X^{\neq_{X}}\subseteq/{}\square_{X}$, and if $\neq_{X}$
is an apartness relation, or discrete, then $/{}\square_{X}\subseteq
X^{\neq_{X}}$.
(ii) $(\mathrm{MIN})$ $/{}\square_{X}^{\neq_{X}}\subseteq X$, and if
$\neq_{X}$ is an apartness relation, or discrete, then
$X\subseteq/{}\square_{X}^{\neq_{X}}$.
(iii) $\big{(}\bigcup_{i\in
I}A_{i}\big{)}^{\neq_{X}}=_{\mathcal{E}(X)}\bigcap_{i\in I}A_{i}^{\neq_{X}}$.
(iv) $\big{(}\bigcap_{i\in
I}A_{i}\big{)}^{\neq_{X}}\supseteq_{\mathcal{E}(X)}\bigcup_{i\in
I}A_{i}^{\neq_{X}}$.
(v) $A\subseteq B^{\neq_{X}}\Leftrightarrow B\subseteq A^{\neq_{X}}$.
(vi) $A\subseteq(A^{\neq_{X}})^{\neq_{X}}$ and
$A^{\neq_{X}}=_{\mathcal{E}(X)}[(A^{\neq_{X}})^{\neq_{X}}]^{\neq_{X}}$.
(vii) If $f$ is strongly extensional, then
$f^{-1}\big{(}C^{\neq_{X}}\big{)}\subseteq[f^{-1}(C)]^{\neq_{X}}$.
(viii) If $f$ is an injection and a surjection, then
$[f^{-1}(C)]^{\neq_{X}}\subseteq f^{-1}\big{(}C^{\neq_{X}}\big{)}$.
(ix) If $f$ is an injection, then
$f\big{(}A^{\neq_{X}}\big{)}\subseteq(f(A))^{\neq_{Y}}$.
(x) If $f$ is a strongly extensional surjection, then
$(f(A))^{\neq_{Y}}\subseteq f\big{(}A^{\neq_{X}}\big{)}$.

###### Proof.

We show only (i), and for (ii) we work similarly. The rest cases follow in a
straightforward way. If $x{{}^{\prime}}\in X^{\neq_{X}}:=\\{x{{}^{\prime}}\in
X\mid\forall_{x\in X}(x{{}^{\prime}}\neq_{X}x)\\}$, then
$x{{}^{\prime}}\neq_{X}x{{}^{\prime}}$ too i.e.,
$x{{}^{\prime}}\in/{}\square_{X}$. To show $/{}\square_{X}\subseteq
X^{\neq_{X}}$ under the apartness assumption for $\neq_{X}$, let
$x{{}^{\prime}}\in X$ with $x{{}^{\prime}}\neq_{X}x{{}^{\prime}}$. If $x\in
X$, by cotransitivity$(\textnormal{{Ineq}}_{5})$ we get
$x{{}^{\prime}}\neq_{X}x$ or $x\neq_{X}x{{}^{\prime}}$. If $\neq_{X}$ is
discrete, then it suffices to treat the case $x{{}^{\prime}}=_{X}x$. By the
extensionality of $\neq_{X}$ and the hypothesis
$x{{}^{\prime}}\neq_{X}x{{}^{\prime}}$ we conclude that
$x{{}^{\prime}}\neq_{X}x$. ∎

Next we introduce various notions of tight (extensional) subsets of a set with
an extensional inequality $(X,=_{X},\neq_{X})$. Clearly, the logical or weak
complement of an extensional subset $A$ of $X$

$A^{c}:=\\{x\in X\mid\forall_{a\in A}(\neg(x=_{X}a))\\}$

includes the $\neq_{X}$-complement $A^{\neq_{X}}$. If the converse inclusion
holds, we call $A$ $1$-tight.

######  Definition 3.6.

If $\mathcal{X}:=(X,=_{X},\neq_{X})\in\textnormal{{SetExtIneq}}$, and
$A\subseteq X$, we call $A$:
(a) $1$-tight, if $A^{c}\subseteq A^{\neq_{X}}$,
(b) $0$-tight, if $(A^{\neq_{X}})^{c}\subseteq A$,
(c) $\neq_{X}$-stable, if $A^{\neq_{X}\neq_{X}}\subseteq A$,
(d) $\neg$-stable, if $A^{cc}\subseteq A$,
(d) left-cotight, if $A\subseteq(A^{c})^{\neq_{X}}$,
(e) right-cotight, if $(A^{c})^{\neq_{X}}\subseteq A$.

The term tight subset is explained as follows. If
$x\neq_{X}y:=(x=_{X}y)^{\mathbf{N}}$, then tightness of $\neq_{X}$ (condition
$(\textnormal{{Ineq}}_{3})$ of Definition 2.4) takes the form

$\neg\big{[}(x=_{X}y)^{\mathbf{N}}\big{]}\Rightarrow x=_{X}y,$

which is an instance of the implication

$\neg\big{[}A^{\mathbf{N}}\big{]}\Rightarrow A.$

We call the formulas of $\mathrm{BST}$ that satisfy the above implication
tight (see also [17]). There are formulas of $\mathrm{BST}$ for which we
cannot show to be tight. For example, let the implication $\neg(x\leq
y)\Rightarrow x>y$, where $x,y\in{\mathbb{R}}$, which is equivalent to
Markov’s Principle $(\mathrm{MP})$, and hence not provable in $\mathrm{BISH}$
(see [7]). As we explain in Remark 6.1 we can show in $(\mathrm{MIN})$ that
$x\leq y\Leftrightarrow(x>y)^{\mathbf{N}}$, and hence the above implication in
${\mathbb{R}}$ is written as

$\neg\big{(}(x>y)^{\mathbf{N}}\big{)}\Rightarrow x>y.$

Consequently, the tightness of the formula corresponding to $x>y$ cannot be
shown in $\mathrm{BISH}$. The dual implication $(\neg
A)^{\mathbf{N}}\Rightarrow A$ holds, as by Definition 2.3 we have that $(\neg
A)^{\mathbf{N}}:=(A\to\bot)^{\mathbf{N}}:=A\wedge\top\Leftrightarrow A$. Now,
as $A^{\neq_{X}}:=\\{x\in X\mid\forall_{a\in A}(x\neq_{X}a)\\},$ and as

$A=_{\mathcal{E}(X)}\\{x\in X\mid\exists_{a\in A}(x=_{X}a)\\},$

the inclusion $A^{c}\subseteq A^{\neq_{X}}$ implies that for every $x\in
A^{c}$ i.e., $\neg(\exists_{a\in A}(x=_{X}a))$, we have that $x\in
A^{\neq_{X}}$ i.e., $\forall_{a\in A}(x\neq_{X}a)$, the strong negation of
which is $\exists_{a\in A}(x\neq_{X}a)^{\mathbf{N}}$. If we have that
$(x\neq_{X}a)^{\mathbf{N}}\Rightarrow x=_{X}a$, a form of strong tightness,
then the implication $x\in A^{c}\Rightarrow x\in A^{\neq_{X}}$ expresses the
following tightness

$\neg{\big{[}\big{(}\forall_{a\in
A}(x\neq_{X}a)\big{)}^{\mathbf{N}}\big{]}}\Rightarrow\forall_{a\in
A}(x\neq_{X}a).$

A similar explanation can be offered for $0$-tightness as follows. The
inclusion $(A^{\neq_{X}})^{c}\subseteq A$ implies for every $x\in X$ the
implication $\neg{(x\in A^{\neq_{X}})}\Rightarrow x\in A$ i.e.,
$\neg{(\forall_{a\in A}(x\neq_{X}a)}\Rightarrow x\in A$. Again, as $x\in
A\Leftrightarrow\exists_{a\in A}(x=_{X}a)$, $0$-tightness of $A$ takes the
form

$\neg{\big{[}(x\in A)^{\mathbf{N}}\big{]}}\Rightarrow x\in A.$

The following facts are straightforward to show.

######  Proposition 3.7.

Let $\mathcal{X}\in\textnormal{{SetExtIneq}}$, and $A,B,A_{i}$ subsets of $X$,
for every $i\in I$.
(i) $/{}\square_{X}$ is $1$-tight.
(ii) If $\neq_{X}$ is discrete, then $X$ is $1$-tight.
(iii) If $A_{i}$ is $1$-tight, for every $i\in I$, then $\bigcup_{i\in
I}A_{i}$ is $1$-tight.
(iv) If $A$ is $0$-tight, then $A$ is $\neg$-stable.
(v) If $A$ is $1$-tight and $\neg$-stable, then $A$ is $0$-tight.
(vi) If $A$ is $\neq_{X}$-stable, then $A$ is left-cotight.
(vii) If $A$ is right-cotight and $1$-tight, then $A$ is $\neq_{X}$-stable.
(viii) If $A$ is $1$-tight, then $A$ is left-cotight.

Notice that te intersection of $1$-tight sets need not be $1$-tight. The open
ball $[d_{x}<\epsilon]:=\\{y\in X\mid d(x,y)<\epsilon\\}$ of a metric space
$(X,d)$ is $1$-tight, but, in general, it is not $0$-tight. A plethora of
$1$-tight subsets of a metric space is provided by Remark 6.8(ii).

##  4 Complemented subsets

Complemented subsets are pairs of positively disjoint subsets of a set with an
inequality. As the definition of the empty subset requires that $X$ is
equipped with an extensional inequality, we work within the category
SetExtIneq, although many related concepts are definable also within SetIneq.

######  Definition 4.1.

If $\mathcal{X}:=(X,=_{X},\neq_{X})$ is in SetExtIneq and
$A:=X_{P},B:=X_{Q}\in\mathcal{E}(X)$, then the overlapping relation $A\between
B$ is defined by

$A\between B:\Leftrightarrow\exists_{x\in X_{P}}\exists_{x{{}^{\prime}}\in
X_{Q}}\big{(}x=_{X}x{{}^{\prime}}\big{)}.$

Strongly negating the above notion, we say that $A$ and $B$ are disjoint with
respect to $\neq_{X}$, if

$A\bm{)}\bm{(}B:\Leftrightarrow\forall_{x\in X_{P}}\forall_{x{{}^{\prime}}\in
X_{Q}}\big{(}x\neq_{X}x{{}^{\prime}}\big{)}.$

A complemented subset of $\mathcal{X}$ is a pair $\bm{A}:=(A^{1},A^{0})$,
where $A^{1}:=X_{P_{1}},A^{0}:=X_{P_{0}}\in\mathcal{E}(X)$ such that
$A^{1}\bm{)}\bm{(}A^{0}$. Its characteristic function
$\chi_{\bm{A}}\colon\mathrm{dom}(\bm{A}):=\\{x\in X\mid P_{1}(x)\vee
P_{0}(x)\\}\to\mathbb{2}$ is defined by

$\chi_{\bm{A}}(x):=\left\\{\begin{array}[]{ll}1&\mbox{, $P_{1}(x)$}\\\
0&\mbox{, $P_{0}(x)$.}\end{array}\right.$

If $\bm{A},\bm{B}$ are complemented extensional subsets of $X$, let
$\bm{A}\subseteq\bm{B}:\Leftrightarrow A^{1}\subseteq B^{1}\ \&\
B^{0}\subseteq A^{0}.$ We say that $\bm{A}$ is inhabited, if $A^{1}$ is
inhabited, coinhabited, if $A^{0}$ is inhabited, and total, if
$\mathrm{dom}(\bm{A})=_{\mathcal{E}(X)}X$. We call $\bm{A}$ $1$-tight, if for
every $x\in X$, we have that $\neg{(x\in A^{1})}\Rightarrow x\in A^{0}$, and
we call $\bm{A}$ $0$-tight, if for every $x\in X$, we have that $\neg{(x\in
A^{0})}\Rightarrow x\in A^{1}$. Let $\mathcal{E}^{\bm{)}\bm{(}}(X)$ be their
totality111111The totality $\mathcal{E}^{\bm{)}\bm{(}}(X)$ can also be defined
by separation as follows:
$\mathcal{E}^{\bm{)}\bm{(}}(X):=\\{(A^{1},A^{0})\in\mathcal{E}(X)\times\mathcal{E}(X)\mid
A^{1}\bm{)}\bm{(}A^{0}\\}$. The relation
$R(A^{1},A^{0}):=A^{1}\bm{)}\bm{(}A^{0}$ is extensional on
$\mathcal{E}(X)\times\mathcal{E}(X)$, and as $\mathcal{E}(X)$ is an
impredicative set, $\mathcal{E}(X)\times\mathcal{E}(X)$ and
$\mathcal{E}^{\bm{)}\bm{(}}(X)$ are also impredicative sets., equipped with
the equality
$\bm{A}=_{\mathcal{E}^{{\bm{)}\bm{(}}}(X)}\bm{B}:\Leftrightarrow\bm{A}\subseteq\bm{B}\
\&\ \bm{B}\subseteq\bm{A}$.

If $A:=X_{P}\in\mathcal{E}(X)$, then $\bm{\mu}A:=(A,A^{\neq_{X}})$ is in
$\mathcal{E}^{\bm{)}\bm{(}}(X)$, and if $\bm{A}$ is $1$-tight, then the
inclusions

$(A^{1})^{c}\subseteq A^{0}\subseteq(A^{1})^{\neq_{X}}\subseteq(A^{1})^{c}$

show that the $1$-tightness of $\bm{A}$ is equivalent to the $1$-tightness of
$A^{1}$.

######  Proposition 4.2.

Let $\mathcal{X}:=(X,=_{X},\neq_{X})$ be in SetExtIneq and
$A:=X_{P},B:=X_{Q}\in\mathcal{E}(X)$.
(i) $(\mathrm{MIN})$ If $A\bm{)}\bm{(}B$, then $A\cap
B\subseteq/{}\square_{X}$, and $(\mathrm{INT})$ $/{}\square_{X}\subseteq A\cap
B$.
(ii) $(\mathrm{MIN})$ If $\neq_{X}$ is discrete and $A\cap
B\subseteq/{}\square_{X}$, then $A\bm{)}\bm{(}B$.
(iii) $(\mathrm{MIN})$ If $\neq_{X}$ is cotransitive
$(\textnormal{{Ineq}}_{5})$ and symmetric $(\textnormal{{Ineq}}_{4})$, then
$/{}\square_{X}\bm{)}\bm{(}A$.
(iv) $(\mathrm{INT})$ $/{}\square_{X}\bm{)}\bm{(}A$.

###### Proof.

(i) By the definition of $A\bm{)}\bm{(}B$ we get $\forall_{x\in
X}\big{(}P(x)\wedge Q(x)\Rightarrow x\neq_{X}x\big{)}$, which is the required
inclusion. The converse inclusion holds trivisally by Ex Falso.
(ii) If $P(a)$ and $Q(b)$, for some $a,b\in X$, then if $a=_{X}b$, by
extensionality of $Q(x)$ we get $Q(a)$. Since than $P(a)\wedge Q(a)$, we get
$a\neq_{X}a$. Hence, by discreteness of $\neq_{X}$, we conclude that
$a\neq_{X}b$.
(iii) If $x\in/{}\square_{X}$, then $x\neq_{X}x$, and by cotransitivity
$x\neq_{X}y$ or $y\neq_{X}x$, where $y\in A$. By symmetry of $\neq_{X}$ we get
in both cases the required inequality $x\neq_{X}y$.
(iv) If $x\in/{}\square_{X}$, then $x\neq_{X}x$, and as $x=_{X}x$ by
$(\textnormal{{Ineq}}_{1})$ we get $\bot$ and by Ex Falso we conclude
$x\neq_{X}y$, where $y\in A$. ∎

All operations between extensional complemented subsets that appear in this
section are determined by the corresponding definitions of operations between
subsets in the previous section. Here we shall use only the operations of the
so-called in [44] first algebra of complemented subsets
$\mathcal{B}_{1}^{e}(X):=\big{(}\mathcal{E}^{\bm{)}\bm{(}}(X),\cup,\cap,-)$ of
$X$, as the second algebra
$\mathcal{B}_{2}^{e}(X):=\big{(}\mathcal{E}^{\bm{)}\bm{(}}(X),\vee,\wedge,-)$
does not suit well to topology (it suits well though, to Bishop-Cheng Measure
Theory).

######  Definition 4.3.

Let
$\mathcal{X}:=(X,=_{X},\neq_{X}),\mathcal{Y}:=(Y,=_{Y},\neq_{Y})\in\textnormal{{SetIneq}}$.
If $\bm{A},\bm{B}\in\mathcal{E}^{\bm{)}\bm{(}}(X)$, $(\bm{\lambda}(i))_{i\in
I}$ is a family in $\mathcal{E}^{\bm{)}\bm{(}}(X)$ indexed by some set $I$,
and if $\bm{C}\in\mathcal{E}^{\bm{)}\bm{(}}(Y)$ , let

$\bm{A}\cup\bm{B}:=(A^{1}\cup B^{1},A^{0}\cap B^{0}),\ \ \ \ \bigcup_{i\in
I}\bm{\lambda}(i):=\bigg{(}\bigcup_{i\in I}\lambda^{1}(i),\bigcap_{i\in
I}\lambda^{0}(i)\bigg{)},$ $\bm{A}\cap\bm{B}:=(A^{1}\cap B^{1},A^{0}\cup
B^{0}),\ \ \ \ \ \ \bigcap_{i\in I}\bm{\lambda}(i):=\bigg{(}\bigcap_{i\in
I}\lambda^{1}(i),\bigcup_{i\in I}\lambda^{0}(i)\bigg{)},$ $\ \ \
-\bm{A}:=(A^{0},A^{1}),\ \ \ \ \ \ \bm{A}-\bm{B}:=\bm{A}\cap(-\bm{B}),$
$\bm{A}\times\bm{C}:=\big{(}A^{1}\times C^{1},\ [A^{0}\times Y]\cup[X\times
C^{0}]\big{)}.$

With the above notion of complement of a complemented subset we recover
constructively properties of classical subsets that are based on classical
logic. Namely, we have that

$\bm{A}\subseteq\bm{B}\Leftrightarrow-\bm{B}\subseteq-\bm{A},\ \ \ \
-(-\bm{A}):=\bm{A},\ \ \ \
(X,/{}\square_{X})-\bm{A}=_{\mathcal{E}^{\bm{)}\bm{(}}(X)}\bm{A}.$

If $\bm{\lambda}(0):=\bm{A}$ and $\bm{\lambda}(1):=\bm{B}$ defines a family of
complemented subsets over $\mathbb{2}$, then

$\bigcup_{i\in\mathbb{2}}\bm{\lambda}(i)=_{{\mathcal{E}^{\bm{]}\bm{[}}(X)}}\bm{A}\cup\bm{B}\
\ \ \&\ \ \
\bigcap_{i\in\mathbb{2}}\bm{\lambda}(i)=_{{\mathcal{E}^{\bm{]}\bm{[}}(X)}}\bm{A}\cap\bm{B}.$

Alternatively, we can define the union and the intersection of a set of
complemented subsets as follows.

######  Definition 4.4.

If $F(X_{P^{1}},X_{P^{0}})$ is an extensional property on
$\mathcal{E}^{\bm{)}\bm{(}}(X)$, let

$\bm{\mathcal{F}}:=\\{(X_{P^{1}},X_{P^{0}})\in\mathcal{E}^{\bm{)}\bm{(}}(X)\mid
F(X_{P^{1}},X_{P^{0}})\\},$
$\mathcal{F}^{1}:=\big{\\{}X_{P}\in\mathcal{E}(X)\mid\exists_{X_{Q}\in\mathcal{E}(X)}\big{(}F(X_{P},X_{Q})\big{)}\big{\\}},$
$\mathcal{F}^{0}:=\big{\\{}X_{Q}\in\mathcal{E}(X)\mid\exists_{X_{P}\in\mathcal{E}(X)}\big{(}F(X_{P},X_{Q})\big{)}\big{\\}}.$

We define

$\bigcup\bm{\mathcal{F}}:=\bigg{(}\bigcup\mathcal{F}^{1},\bigcap\mathcal{F}^{0}\bigg{)},\
\ \ \ \
\bigcap\bm{\mathcal{F}}:=\bigg{(}\bigcap\mathcal{F}^{1},\bigcup\mathcal{F}^{0}\bigg{)}.$

Notice that the extensionality of $F$ implies the extensionality of the
properties

$F^{1}(X_{P}):=\exists_{X_{Q}\in\mathcal{E}(X)}\big{(}F(X_{P},X_{Q})\big{)},\
\ \ \ \
F^{0}(X_{Q}):=\exists_{X_{P}\in\mathcal{E}(X)}\big{(}F(X_{P},X_{Q})\big{)}.$

The following facts are straightforward to show and are used later in the
paper.

######  Corollary 4.5.

(i) If $\bm{A}\subseteq\bm{B}$ and $\bm{A}\subseteq\bm{C}$, then
$\bm{A}\subseteq\bm{B}\cap\bm{C}$.
(ii) If $\bm{B}\subseteq\bm{A}_{i}$, then $\bm{B}\subseteq\bigcup_{i\in
I}\bm{A}_{i}$.

In contrast to the standard one-dimensional subset theory, where only one
empty subset $/{}\square_{X}$ of a set $X$ exists, in the two dimensional
complemented subset theory there are many “empty” complemenetd subsets and
equally many “coempty” subsets. The proof of subsequent Proposition 4.7 is
straightforward.

######  Definition 4.6.

If $\mathcal{X}:=(X,=_{X},\neq_{X})$ is in SetExtIneq, and if
$\bm{A}\in\mathcal{E}^{\bm{)}\bm{(}}(X)$, let

$0_{\bm{X}}:=(/{}\square_{X},X),\ \ \ \ 1_{\bm{X}}:=(X,/{}\square_{X}),\ \ \ \
1_{\bm{A}}:=(\mathrm{dom}(\bm{A}),/{}\square_{X}),\ \ \ \
0_{\bm{A}}:=\big{(}/{}\square_{X},\mathrm{dom}(\bm{A})\big{)}.$

The complemented subsets $0_{\bm{X}}$ and of the form $0_{\bm{A}}$ are called
empty, while the complemented subsets $1_{\bm{X}}$ and of the form
$1_{\bm{A}}$ are called coempty. Let their corresponding sets

$\mathrm{Empty}(\mathcal{X}):=\\{\bm{A}:=(A^{1},A^{0})\in\mathcal{E}^{\bm{)}\bm{(}}(X)\mid
A^{1}=_{\mathcal{E}(X)}/{}\square_{X}\\},$
$\mathrm{coEmpty}(\mathcal{X}):=\\{\bm{A}:=(A^{1},A^{0})\in\mathcal{E}^{\bm{)}\bm{(}}(X)\mid
A^{0}=_{\mathcal{E}(X)}/{}\square_{X}\\}.$

######  Proposition 4.7 ($\mathrm{INT}$).

The following hold:
(i) $0_{\bm{X}}$ and $1_{\bm{X}}$ are the bottom and top elements of
$\mathcal{E}^{\bm{)}\bm{(}}(X)$, respectively.
(ii) $-0_{\bm{X}}:=1_{\bm{X}}$ and $-0_{\bm{A}}:=1_{\bm{A}}$.
(iii) $\bm{A}\cup(-\bm{A})=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}1_{\bm{A}}$ and
$\bm{A}\cap(-\bm{A})=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}0_{\bm{A}}$.
(iv)
$0_{\bm{X}}\cup\bm{A}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}\bm{A}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}0_{\bm{A}}\cup\bm{A}$.
(v) $0_{\bm{X}}\cap\bm{A}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}0_{\bm{X}}$ and
$0_{\bm{A}}\cap\bm{A}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}0_{\bm{A}}$.
(vi) $1_{\bm{X}}\cup\bm{A}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}1_{\bm{X}}$ and
$1_{\bm{A}}\cup\bm{A}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}\bm{1}_{A}$.
(vii)
$1_{\bm{X}}\cap\bm{A}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}\bm{A}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}1_{\bm{A}}\cap\bm{A}$.
(viii) $0_{-\bm{A}}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}0_{\bm{A}}$.
(ix) $0_{0_{\bm{X}}}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}0_{\bm{X}}$ and
$1_{1_{\bm{X}}}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}1_{\bm{X}}$.
(x)
$0_{0_{\bm{A}}}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}0_{\bm{A}}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}0_{1_{\bm{A}}}$.

Proposition 4.7(iii) shows that the algebra of complemented subsets cannot be,
in geberal boolean. Actually, the totality of complemented subsets of some
$\mathcal{X}:=(X,=_{X},\neq_{X})$ in SetExtIneq is a swap algebra of type (I)
(see [18] for all necessary details). The abstract version of the common
properties of the two algebras of complemented subsets
$\mathcal{B}_{1}^{e}(X)$ and $\mathcal{B}_{2}^{e}(X)$ forms the notion of a
swap algebra, while the axiom $(\textnormal{{swapa}}_{\mathrm{I}})$ is
satisfied by $\mathcal{B}_{1}^{e}(X)$ and the axiom
$(\textnormal{{swapa}}_{\mathrm{II}})$ is satisfied by
$\mathcal{B}_{2}^{e}(X)$ (see Definition 4.8). A swap algebra of type (I) does
not satisfy, in general, condition $(\textnormal{{swapa}}_{\mathrm{II}})$, and
a swap algebra of type (II) does not satisfy, in general, condition
$(\textnormal{{swapa}}_{\mathrm{II}})$. A swap agebra is a generalisation of a
Boolean algebra, as every Boolean algebra is a swap algebra. In this case the
two types of swap algebras collapse to the structure of a Boolean algebra.
Moreover, the total elements of a swap algebra from a Boolean algebra. Swap
algebras of type (II) are better related to boolean-valued partial functions
rather than swap algebras of type (I) (see [18]). The abstract version of the
boolean-valued partial functions on a set with an extensional inequality is
the notion of the so-called swap ring. The theory of swap algebras and swap
rings, which is under current development, is expected to be a generalisation
of the theory of Boolean algebras and Boolean rings that originates from
constructive mathematics. Their theory is one of the few examples of
mathematical theories that have non-trivial applications to classical
mathematics and are motivated by constructive mathematics!

######  Definition 4.8.

A swap algebra is a structure
$\mathcal{A}:=\big{(}A,\vee,\wedge,0,1,-,0_{-},1_{-}\big{)}$, where
$(A,=_{A},\neq_{A})$ is a set with an inequality, $0,1\in A$,
$\vee,\wedge,\colon A\times A\to A$ and $0_{-},1_{-}\colon A\to A$ are
functions, such that the following conditions hold:
$(\textnormal{{swapa}}_{1})$ $a\vee a=_{{A}}a$.
$(\textnormal{{swapa}}_{2})$ $a\vee b=_{{A}}b\vee a$.
$(\textnormal{{swapa}}_{3})$ $a\vee(b\vee c)=_{{A}}(a\vee b)\vee c$.
$(\textnormal{{swapa}}_{4})$ $a\vee(b\wedge c)=_{{A}}(a\vee b)\wedge(a\vee
c)$.
$(\textnormal{{swapa}}_{5})$ $0\neq_{{A}}1$.
$(\textnormal{{swapa}}_{5})$ $-0=_{{A}}1$.
$(\textnormal{{swapa}}_{7})$ $-(-a)=_{{A}}a$.
$(\textnormal{{swapa}}_{8})$ $-(a\vee b)=_{{A}}(-a)\wedge(-b)$.
$(\textnormal{{swapa}}_{9})$ $a\vee(-a)=_{{A}}1_{a}$ and
$a\wedge(-a)=_{{A}}0_{a}$.
$(\textnormal{{swapa}}_{10})$ $a=_{{A}}0_{a}\vee a$.
A swap algebra $\mathcal{A}$ is of type $($I$)$, if the following condition
holds:
$(\textnormal{{swapa}}_{\mathrm{I}})$ $(a\vee b)\wedge a=_{{A}}a$.
A swap algebra $\mathcal{A}$ is of type $($II$)$, if the following condition
holds:
$(\textnormal{{swapa}}_{\mathrm{II}})$ $0_{a}\vee b=_{{A}}1_{a}\wedge b$.
An element $a$ of $A$ is called total, if $1_{a}=_{{A}}1$.

The complemented subsets studied here form a swap algebra of type (I). To show
$0_{\bm{X}}\neq_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}1_{\bm{X}}$, we need to fix
the notion of inequality between complemented subsets. Using Definition 5.4
that involves complemented points, introduced in section 5, the inequality
$0_{\bm{X}}\neq_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}1_{\bm{X}}$ follows easily
for an inhabited set with an inequality (Corollary 5.5(i)) . Next follow some
properties of the complemented inverse image of a strongly extensional
function.

######  Proposition 4.9.

Let $\mathcal{X},\mathcal{Y},\mathcal{Z},f\colon X\to Y,g\colon Y\to
Z\in(\textnormal{{SetExtIneq}},\textnormal{{StrExtFun}})$.
(i) If $\bm{B}:=(B^{1},B^{0})\in\mathcal{E}^{\bm{)}\bm{(}}(Y)$, then
$f^{-1}(\bm{B}):=\big{(}f^{-1}(B^{1}),f^{-1}(B^{0})\big{)}\in\mathcal{E}^{\bm{)}\bm{(}}(X)$.
(ii) The assignment routine
$f^{*}\colon\mathcal{E}^{\bm{)}\bm{(}}(Y)\rightsquigarrow\mathcal{E}^{\bm{)}\bm{(}}(X)$,
$\bm{B}\mapsto f^{-1}(\bm{B})$, is a monotone function.
(iii) If $\bm{B}$ is total, then $f^{-1}(\bm{B})$ is total.
(iv)
$f^{-1}(\bm{A}\cup\bm{B})=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}f^{-1}(\bm{A})\cup
f^{-1}(\bm{B})$.
(v)
$f^{-1}(\bm{A}\cap\bm{B})=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}f^{-1}(\bm{A})\cap
f^{-1}(\bm{B})$.
(vi) $f^{-1}(-\bm{A})=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}-f^{-1}(\bm{A})$.
(vii)
$f^{-1}(\bm{A}-\bm{B})=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}f^{-1}(\bm{A})-f^{-1}(\bm{B})$.
(viii)
$f^{-1}(Y,/{}\square_{Y})=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}(X,/{}\square_{X})$
and
$f^{-1}(/{}\square_{Y},Y)=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}(/{}\square_{X},X)$.
(ix) If $\bm{\mathcal{G}}$ is an extensional subset of
$\mathcal{E}^{\bm{)}\bm{(}}(Y)$ and
$f^{-1}(\bm{\mathcal{G}}):=\\{f^{-1}(\bm{G})\mid\bm{G}\in\bm{\mathcal{G}}\\}$,
then

$f^{-1}\bigg{(}\bigcup\bm{\mathcal{G}}\bigg{)}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}\bigcup
f^{-1}(\bm{\mathcal{G}}),\ \ \ \
f^{-1}\bigg{(}\bigcap\bm{\mathcal{G}}\bigg{)}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}\bigcap
f^{-1}(\bm{\mathcal{G}}).$

(x) If $\bm{C}\in\mathcal{E}^{\bm{)}\bm{(}}(Z)$, then $(g\circ
f)^{-1}(\bm{C})=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}f^{-1}(g^{-1}(\bm{C}))$.

###### Proof.

(i) Let $x^{1}\in X$ such that $f(x^{1})=_{Y}b^{1}$, for some $b^{1}\in
B^{1}$, and let $x^{0}\in X$ such that $f(x^{0})=_{Y}b^{0}$, for some
$b^{0}\in B^{0}$. By extensionality of $\neq_{Y}$ we have that the inequality
$b^{1}\neq_{Y}b^{0}$ implies the inequality $f(x^{1})\neq_{Y}f(x^{0})$, hence
by strong extensionality of $f$ we get $x^{1}\neq_{X}x^{0}$.
(ii) Monotonicity of $f^{*}$ follows from monotonicity of the inverse image.
(iii) $\mathrm{dom}(f^{-1}(\bm{B})):=f^{-1}(B^{1})\cup
f^{-1}(B^{)}=_{\mathcal{E}(X)}f^{-1}(B^{1}\cup
B^{0})=_{\mathcal{E}(X)}f^{-1}(Y)=_{\mathcal{E}(X)}X$.
(iv, v) We show only (iv) and for (v) we work similarly. We have that

$\displaystyle f^{-1}(\bm{A}\cup\bm{B})$
$\displaystyle:=f^{-1}\big{(}A^{1}\cup B^{1},A^{0}\cap B^{0}\big{)}$
$\displaystyle:=\big{(}f^{-1}(A^{1}\cup B^{1}),f^{-1}(A^{0}\cap B^{0})\big{)}$
$\displaystyle=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}\big{(}f^{-1}(A^{1})\cup
f^{-1}(B^{1}),f^{-1}(A^{0})\cap f^{-1}(B^{0})\big{)}$
$\displaystyle=:f^{-1}(\bm{A})\cup f^{-1}(\bm{B}).\qed$

(vi) follows immediately, and (vii) follows from (v), (vi) and the definition
of $\bm{A}-\bm{B}$.
(viii) follows from Proposition 3.4(i), (ix) from Proposition 3.4(v), and (x)
from Proposition 3.4(xviii).

Next we prove the basic properties of the complemented direct image of a
strong injection.

######  Proposition 4.10.

Let $\mathcal{X},\mathcal{Y},\mathcal{Z}\in\textnormal{{SetExtIneq}}$,
$f\colon X\to Y$ and $g\colon Y\to Z$ strong injections.
(i) If $\bm{A}:=(A^{1},A^{0})\in\mathcal{E}^{\bm{)}\bm{(}}(X)$, then
$f(\bm{A}):=\big{(}f(A^{1}),f(A^{0})\big{)}\in\mathcal{E}^{\bm{)}\bm{(}}(Y)$.
(ii) The assignment routine
$f_{*}\colon\mathcal{E}^{\bm{)}\bm{(}}(X)\rightsquigarrow\mathcal{E}^{\bm{)}\bm{(}}(Y)$,
$\bm{A}\mapsto f(\bm{A})$, is a monotone function.
(iii) $f(\bm{A}\cup\bm{B})=_{{\mathcal{E}^{\bm{)}\bm{(}}(Y)}}f(\bm{A})\cup
f(\bm{B})$.
(iv) $f(\bm{A}\cap\bm{B})=_{{\mathcal{E}^{\bm{)}\bm{(}}(Y)}}f(\bm{A})\cap
f(\bm{B})$.
(v) $f(-\bm{A})=_{{\mathcal{E}^{\bm{)}\bm{(}}(Y)}}-f(\bm{A})$.
(vi) $f(\bm{A}-\bm{B})=_{{\mathcal{E}^{\bm{)}\bm{(}}(Y)}}f(\bm{A})-f(\bm{B})$.
(vii)
$f(X,/{}\square_{X})=_{{\mathcal{E}^{\bm{)}\bm{(}}(Y)}}(f(X),/{}\square_{Y})$
and
$f(/{}\square_{X},X)=_{{\mathcal{E}^{\bm{)}\bm{(}}(Y)}}(/{}\square_{Y},f(X))$.
(viii) If $\bm{\mathcal{H}}$ is an extensional subset of
$\mathcal{E}^{\bm{)}\bm{(}}(X)$ and
$f(\bm{\mathcal{H}}):=\\{f(\bm{H})\mid\bm{H}\in\bm{\mathcal{H}}\\}$, then

$f\bigg{(}\bigcup\bm{\mathcal{H}}\bigg{)}=_{{\mathcal{E}^{\bm{)}\bm{(}}(Y)}}\bigcup
f(\bm{\mathcal{H}}),\ \ \ \
f\bigg{(}\bigcap\bm{\mathcal{H}}\bigg{)}=_{{\mathcal{E}^{\bm{)}\bm{(}}(Y)}}\bigcap
f(\bm{\mathcal{H}}).$

(ix) $\bm{B}\cap f(X,/{}\square_{X})\subseteq f(f^{-1}(\bm{B}))$.
(x) $(g\circ f)(\bm{A})=_{\mathcal{E}^{\bm{)}\bm{(}}(Z)}g(f(\bm{A}))$.

###### Proof.

(i) Let $y^{1}\in Y$, such that $y^{1}=_{Y}f(a^{1})$, for some $a^{1}\in
A^{1}$, and let $y^{0}\in Y$, such that $y^{0}=_{Y}f(a^{0})$, for some
$a^{0}\in A^{0}$. As $a^{1}\neq_{X}a^{0}$, by injectivity of $f$ we have that
$f(a^{1})\neq_{Y}f(a^{0})$, and by extensionality of $\neq_{Y}$ we get
$y^{1}\neq_{Y}y^{0}$.
(ii) Monotonicity of the complemented direct image follows from monotonicity
of the direct image.
(iii, iv) We show only (iii) and for (iv) we work similarly. We have that

$\displaystyle f(\bm{A}\cup\bm{B})$ $\displaystyle:=f\big{(}A^{1}\cup
B^{1},A^{0}\cap B^{0}\big{)}$ $\displaystyle:=\big{(}f(A^{1}\cup
B^{1}),f(A^{0}\cap B^{0})\big{)}$
$\displaystyle=_{{\mathcal{E}^{\bm{)}\bm{(}}(Y)}}\big{(}f(A^{1})\cup
f(B^{1}),f(A^{0})\cap f(B^{0})\big{)}$ $\displaystyle=:f(\bm{A})\cup
f(\bm{B}).\qed$

(v) follows immediately and (vi) follows from (iv) and (v).
(vii) follows from Proposition 3.4(ii), and (viii) follows from Proposition
3.4(viii) and (xvi).
(ix) By Proposition 3.4(ix, x) we have that

$\displaystyle\bm{B}\cap f(X,/{}\square_{X})$ $\displaystyle:=\big{(}B^{1}\cap
f(X),B^{0}\cup{/{}\square_{Y}}\big{)}$
$\displaystyle:=_{{\mathcal{E}^{\bm{)}\bm{(}}(Y)}}\big{(}B^{1}\cap
f(X),B^{0}\big{)}$
$\displaystyle=_{{\mathcal{E}^{\bm{)}\bm{(}}(Y)}}\big{(}f(f^{-1}(B^{1})),B^{0}\big{)}$
$\displaystyle\subseteq\big{(}f(f^{-1}(B^{1})),f(f^{-1}(B^{0}))\big{)}$
$\displaystyle=:f(f^{-1}(\bm{B})).$

(x) It follows from Proposition 3.4(xix).

Notice that for the proof of (i) and (ii) above we need only $f$ to be an
injection, and that under our hypotheses on $f$ we get equality in Proposition
4.10(iv) and (viii). By the previous two propositions and by Proposition
3.4(xiv, xv) we get the following corollary.

######  Corollary 4.11.

Let $\mathcal{X},\mathcal{Y}\in\textnormal{{SetExtIneq}}$ and $f\colon X\to Y$
strongly extensional and a strong injection.
(i) $f^{-1}(f(\bm{A}))=_{\mathcal{E}^{\bm{)}\bm{(}}(X)}\bm{A}$, for every
$\bm{A}\in\mathcal{E}^{\bm{)}\bm{(}}(X)$.
(ii) If $f$ is also a surjection, then
$f(f^{-1}(\bm{B}))=_{\mathcal{E}^{\bm{)}\bm{(}}(Y)}\bm{B}$, for every
$\bm{B}\in\mathcal{E}^{\bm{)}\bm{(}}(X)$.

In analogy to the characterisations of injectivity and surjectivity through
Proposition 3.4(xiv, xv), we may define $f\colon X\to Y$ to be a
$\mathrm{cs}$-injection, if $f$ is strongly extensional and a strong
injection, while it is a $\mathrm{cs}$-surjection, if it is strongly
extensional, (strong) injection and surjection.

######  Proposition 4.12.

If $\mathcal{X},\mathcal{Y}\in\textnormal{{SetExtIneq}}$, the following hold:
(i) $/{}\square_{X\times Y}=_{\mathcal{E}(X\times Y)}({/{}\square_{X}}\times
Y)\cup(X\times/{}\square_{Y})$.
(ii) $(\mathrm{INT})$ $/{}\square_{X\times Y}=_{\mathcal{E}(X\times
Y)}{/{}\square_{X}}\times/{}\square_{Y}$.
(iii)
$(X,/{}\square_{X})\times(Y,/{}\square_{Y})=_{\mathcal{E}^{\bm{)}\bm{(}}(X\times
Y)}(X\times Y,/{}\square_{X\times Y})$.
(iv) $(\mathrm{INT})$
$(/{}\square_{X},X)\times(/{}\square_{Y},Y)=_{\mathcal{E}^{\bm{)}\bm{(}}(X\times
Y)}(/{}\square_{X\times Y},X\times Y)$.

###### Proof.

(i) By Definitions 3.2 and 2.6 we have that $/{}\square_{X\times
Y}:=\\{(x,y)\in X\times Y\mid x\neq_{X}x\vee y\neq_{Y}y\\}.$ Clearly,
$/{}\square_{X\times Y}\subseteq({/{}\square_{X}}\times
Y)\cup(X\times/{}\square_{Y})$. For the converse inclusion, let $x\neq_{X}x$
and $y\in Y$. Then $(x,y)\in/{}\square_{X\times Y}$. Similarly, if
$y\neq_{Y}y$ and $x\in X$, then $(x,y)\in/{}\square_{X\times Y}$.
(ii) By extensionality of $\neq_{X}$ and $\neq_{Y}$ we have that

$\displaystyle{/{}\square_{X}}\times/{}\square_{Y}$
$\displaystyle:=\\{(u,w)\times X\times Y\mid\exists_{x\in{\
/{}\square_{X}}}\exists_{y\in{\ /{}\square_{Y}}}(u=_{X}x\wedge w=_{Y}y)\\}$
$\displaystyle=\\{(u,w)\times X\times Y\mid u\neq_{X}u\wedge w\neq_{Y}w)\\},$

hence ${/{}\square_{X}}\times/{}\square_{Y}\subseteq/{}\square_{X\times Y}$.
The converse inclusion follows from Ex Falso.
(iii) By case (i) we have that

$(X,/{}\square_{X})\times(Y,/{}\square_{Y}):=(X\times
Y,({/{}\square_{X}}\times Y)\cup(X\times/{}\square_{Y}))=_{\mathcal{E}(X\times
Y)}(X\times Y,/{}\square_{X\times Y}).$

(iv) By case (ii) we have that

$\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
(/{}\square_{X},X)\times(/{}\square_{Y},Y):=({/{}\square_{X}}\times/{}\square_{Y},(X\times
Y)\cup(X\times Y))=_{\mathcal{E}(X\times Y)}(/{}\square_{X\times Y},X\times
Y).\ \ \ \ \ \ \ \ \ \ \ \ \ \ \qed$

######  Proposition 4.13.

Let $\bm{A},\bm{A}_{1},\bm{A}_{2}\in\mathcal{E}^{{\bm{)}\bm{(}}}(X)$ and
$\bm{B},\bm{B}_{1},\bm{B}_{2},\bm{C}\in\mathcal{E}^{{\bm{)}\bm{(}}}(Y)$.
(i) $\bm{A}\times(\bm{B}\cup\bm{C})=_{\mathcal{E}^{{\bm{)}\bm{(}}}(X\times
Y)}(\bm{A}\times\bm{B})\cup(\bm{A}\times\bm{C})$.
(ii) $\bm{A}\times(\bm{B}\cap\bm{C})=_{\mathcal{E}^{{\bm{)}\bm{(}}}(X\times
Y)}(\bm{A}\times\bm{B})\cap(\bm{A}\times\bm{C})$.
(iii) $\bm{A}\times(\bm{B}-\bm{C})=_{\mathcal{E}^{{\bm{)}\bm{(}}}(X\times
Y)}(\bm{A}\times\bm{B})-(\bm{A}\times\bm{C})$.
(iv)
$(\bm{A}_{1}\times\bm{B}_{1})\cap(\bm{A}_{2}\times\bm{B}_{2})=_{\mathcal{E}^{{\bm{)}\bm{(}}}(X\times
Y)}(\bm{A}_{1}\cap\bm{A}_{2})\times(\bm{B}_{1}\cap\bm{B}_{2})$.

###### Proof.

We prove only (i). We have that

$\displaystyle\bm{A}\times(\bm{B}\cup\bm{C})$
$\displaystyle:=(A^{1},A^{0})\times(B^{1}\cup C^{1},B^{0}\cap C^{0})$
$\displaystyle:=\big{(}A^{1}\times(B^{1}\cup C^{1}),(A^{0}\times
Y)\cup[X\times(B^{0}\cap C^{0})]\big{)}$
$\displaystyle=_{\mathcal{E}^{{\bm{)}\bm{(}}}(X\times Y)}\big{(}(A^{1}\times
B^{1})\cup(A^{1}\times C^{1}),[(A^{0}\times Y)\cup(X\times B^{0})]\ \cap$
$\displaystyle\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \cap[(A^{0}\times Y)\cup(X\times
C^{0})]\big{)}$
$\displaystyle:=(\bm{A}\times\bm{B})\times(\bm{A}\times\bm{C}).\qed$

The notion of a field of complemented subsets is defined by the same clauses
as the notion of a field of subsets, but with respect to the operations on
complemented subsets.

######  Definition 4.14.

If $F(\bm{A})$ is an extensional property on $\mathcal{E}^{\bm{)}\bm{(}}(X)$,
then $\bm{\mathcal{F}}:=\big{\\{}\bm{A}\in\mathcal{E}^{\bm{)}\bm{(}}(X)\mid
F(\bm{A})\big{\\}}$ is a field of complemented subsets, if
$F(X,/{}\square_{X})$, and if $F(\bm{A})$ and $F(\bm{B})$, then $F(-\bm{A})$
and $F(\bm{A}\cup\bm{B})$.

Clearly, if $\bm{\mathcal{F}}$ is a field of complemented subsets and
$\bm{A},\bm{B}\in\bm{\mathcal{F}}$, then $1_{\bm{A}},0_{\bm{A}}$ and
$\bm{A}\cap\bm{B}\in\bm{\mathcal{F}}$. The following remark is immediate to
show.

######  Remark 4.15.

If $\bm{\mathcal{F}}$ is a field of complemented subsets of $\mathcal{X}$,
then $\bm{\mathcal{F}}$ is a swap algebra of type $(I)$.

Actually, what we defined above is a field of complemented subsets of type
(I). A notion of a field of complemented subsets of type (II) is defined
similarly. If $(\bm{\lambda}(i))_{i\in I}$ is a family of complemented subsets
indexed by some set $I$, the following distributivity property of complemented
subsets was presented by Bishop in [2], p. 68:

$0_{\bm{A}}\cup\bigg{(}\bm{A}\cap\bigcup_{i\in
I}\bm{\lambda}(i)\bigg{)}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}0_{\bm{A}}\cup\bigg{[}\bigcup_{i\in
I}\big{(}\bm{A}\cap\bm{\lambda}(i)\big{)}\bigg{]},$

or

$0_{\bm{A}}\cup\bigg{(}\bm{A}\cap\bigcup\bm{\mathcal{F}}\bigg{)}=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}0_{\bm{A}}\cup\bigg{[}\bigcup(\bm{A}\cap\bm{\mathcal{F}})\bigg{]},$

where
$\bm{A}\cap\bm{\mathcal{F}}:=\big{\\{}\bm{B}\in\mathcal{E}^{\bm{)}\bm{(}}(X)\mid\exists_{\bm{F}\in\bm{\mathcal{F}}}\big{(}\bm{B}=_{\mathcal{E}^{\bm{)}\bm{(}}(X)}\bm{A}\cap\bm{F}\big{)}\big{\\}}$.
Bishop’s distributivity property is the constructive counterpart to the
classical distributivity property

$(D_{I})\ \ \ \ \ \ \ \bm{A}\cap\bigcup_{i\in
I}\bm{\lambda}(i)=_{{\mathcal{E}^{\bm{)}\bm{(}}(X)}}\bigcup_{i\in
I}\big{(}\bm{A}\cap\bm{\lambda}(i).$

Distributivity $(D_{I})$ is crucial to the classical proof that the standard
relative topology on a subset of a topological space is indeed a topology.
Constructively though, it cannot be accepted, in general. The constructive
counterpart to the definition of the relative topology within
$\mathrm{cs}$-topological spaces is presented in section 8. See [18] for the
proof of the following fact.

######  Proposition 4.16.

(i) If $X:={\mathbb{R}}$, the distributivity property $(D_{\mathbb{N}})$
implies $\mathrm{LPO}$.
(ii) $(\mathrm{INT})$ If $\bm{A}\in\mathcal{E}^{\bm{]}\bm{[}}(X)$ is total,
then $(D_{I})$ holds, for every $X\in\textnormal{{SetExtIneq}}$.

##  5 Complemented points

Standard topology is point-set topology, in which points play a crucial role
for example, in the sudy of separation axioms of topological spaces. In the
framework of complemented subsets points are certain complemented subsets that
we call complemented points. In this way we can generalise the standard
equivalence $x\in A\Leftrightarrow\\{x\\}\subseteq A$, where $\\{x\\}:=\\{y\in
X\mid y=_{X}x\\}$, to the inclusion relation between complemented points and
complemented subsets.

######  Definition 5.1.

Let $\mathcal{X}:=(X,=_{X},\neq_{X})\in\textnormal{{SetExtIneq}}$. A
complemented point is a complemented subset $\bm{x}_{P}:=(\\{x\\},P)$, where
$x\in X$. We also write $\bm{x}_{P}:=(x,P)$. If
$\bm{A}:=(A^{1},A^{0})\in\mathcal{E}^{\bm{)}\bm{(}}(X)$, where
$A^{1}:=X_{P^{1}}$ and $A^{0}:=X_{P^{0}}$, for some extensional properties
$P^{1},P^{0}$ on $X$, we define the following elementhood and non-elementhood
coditions

$(x,P)\ \varepsilon\ \bm{A}:\Leftrightarrow(x,P)\subseteq\bm{A}\Leftrightarrow
P^{1}(x)\wedge A^{0}\subseteq P,$ $(x,P)\ /{}\ \varepsilon\
\bm{A}:\Leftrightarrow(x,P)\ \varepsilon\ (-\bm{A})\Leftrightarrow
P^{0}(x)\wedge A^{1}\subseteq P.$

We call $(x,P)$ total, if it is a total complemented subset i.e., $\\{x\\}\cup
P=_{\mathcal{E}(X)}X$. Let $\mathrm{Point}(\mathcal{X})$ be the set of points
of $\mathcal{X}$, $\mathrm{Point}(x)$ the set of complemented points over $x$,
and $\mathrm{Point}(\bm{A})$ the set of points of $\bm{A}$ i.e.,

$\mathrm{Point}(\mathcal{X}):=\big{\\{}(X_{Q^{1}},X_{Q^{0}})\in\mathcal{E}^{\bm{)}\bm{(}}(X)\mid\exists_{x\in
X}\big{(}X_{Q^{1}}=_{\mathcal{E}(X)}\\{x\\}\big{)}\big{\\}},$
$\mathrm{Point}(x):=\big{\\{}(X_{Q^{1}},X_{Q^{0}})\in\mathcal{E}^{\bm{)}\bm{(}}(X)\mid
X_{Q^{1}}=_{\mathcal{E}(X)}\\{x\\}\big{\\}},$
$\mathrm{Point}(\bm{A}):=\big{\\{}(X_{Q^{1}},X_{Q^{0}})\in\mathcal{E}^{\bm{)}\bm{(}}(X)\mid\exists_{x\in
X}\big{(}X_{Q^{1}}=_{\mathcal{E}(X)}\\{x\\}\wedge P^{1}(x)\wedge
X_{P^{0}}\subseteq X_{Q^{0}}\big{)}\big{\\}}.$

If $(x,P)\in\mathrm{Point}(\mathcal{X})$, then $(P,x)$ is a complemented
copoint of $\mathcal{X}$. Let
$-\mathrm{Point}(\mathcal{X}),-\mathrm{Point}(c)$, and
$-\mathrm{Point}(\bm{A})$ be the corresponding sets. We call $(x,P)$ a
potential point of $\bm{A}$, if $A^{0}\subseteq P$. If $\bm{\mathcal{F}}$ is
an extensional subset of $\mathcal{E}^{\bm{)}\bm{(}}(X)$, then $(x,P)$ is a
potential point of $\bm{\mathcal{F}}$, if it is a potential point of every
element of $\bm{\mathcal{F}}$.

######  Definition 5.2.

If $\phi(x,P)$ is a formula in $\mathrm{BST}$, we introduce the folowing
notational conventions:

$\forall_{(x,P)\varepsilon\mathcal{X}}\phi(\bm{x}):=\forall_{(x,P)\in\mathrm{Point}(\mathcal{X})}\big{(}\phi(x,P)\big{)},\
\ \ \
\exists_{(x,P)\varepsilon\mathcal{X}}\phi(\bm{x}):=\exists_{(x,P)\in\mathrm{Point}(\mathcal{X})}\big{(}\phi(x,P)\big{)},$
$\forall_{(x,P)\varepsilon\bm{A}}\phi(\bm{x}):=\forall_{(x,P)\in\mathrm{Point}(\bm{A})}\big{(}\phi(x,P)\big{)},\
\ \ \
\exists_{(x,P)\varepsilon\bm{A}}\phi(\bm{x}):=\exists_{(x,P)\in\mathrm{Point}(\bm{A})}\big{(}\phi(x,P)\big{)}.$

Although we can prove $(x,P)\ \varepsilon\
\bm{A}\cap\bm{B}\Leftrightarrow(x,P)\ \varepsilon\ \bm{A}\wedge(x,P)\
\varepsilon\ \bm{B}$, we cannot show always that $(x,P)\ \varepsilon\
\bm{A}\cup\bm{B}\Leftrightarrow(x,P)\ \varepsilon\ \bm{A}\vee(x,P)\
\varepsilon\ \bm{B}$. If we had used the operations between complemented
subsets of type (II), then the former equivalence also fails.

######  Proposition 5.3.

Let $\mathcal{X}:=(X,=_{X},\neq_{X})\in\textnormal{{SetExtIneq}}$, $x\in X$,
$\bm{A}:=(A^{1},A^{0})\in\mathcal{E}^{\bm{)}\bm{(}}(X)$ and
$\bm{B}:=(B^{1},B^{0})\in\mathcal{E}^{\bm{)}\bm{(}}(X)$, where
$A^{1}:=X_{P^{1}},A^{0}:=X_{P^{0}}$ and $B^{1}:=X_{Q^{1}},B^{0}:=X_{Q^{0}}$,
for some extensional properties $P^{1},P^{0},Q^{1}$ and $Q^{0}$ on $X$. Let
also $\bm{\mathcal{F}}$ be an extensional subset of
$\mathcal{E}^{\bm{)}\bm{(}}(X)$.
(i)
$\bm{A}\subseteq\bm{B}\Leftrightarrow\forall_{(x,P)\varepsilon\mathcal{X}}\big{(}(x,P)\
\varepsilon\ \bm{A}\Rightarrow(x,P)\ \varepsilon\ \bm{B}\big{)}$.
(ii) $(x,P)\ \varepsilon\ \bm{A}\vee(x,P)\ \varepsilon\
\bm{B}\Rightarrow(x,P)\ \varepsilon\ \bm{A}\cup\bm{B}$.
(iii) $(x,P)\ \varepsilon\ \bm{A}\cup\bm{B}\Leftrightarrow(x,P)\ \varepsilon\
(A^{1},A^{0}\cap B^{0})\vee(x,P)\ \varepsilon\ (B^{1},A^{0}\cap B^{0})$.
(iv) If $(x,P)$ is a potential point of $\bm{A}$ and $\bm{B}$, then $(x,P)\
\varepsilon\ \bm{A}\cup\bm{B}\Rightarrow(x,P)\ \varepsilon\ \bm{A}\vee(x,P)\
\varepsilon\ \bm{B}$.
(v) $(x,P)\ \varepsilon\ \bm{A}\cap\bm{B}\Leftrightarrow(x,P)\ \varepsilon\
\bm{A}\wedge(x,P)\ \varepsilon\ \bm{B}$.
(vi) $(x,P)\ /{}\ \varepsilon\ \bm{A}\cup\bm{B}\Leftrightarrow(x,P)\ /{}\
\varepsilon\ \bm{A}\wedge(x,P)\ /{}\ \varepsilon\ \bm{B}$.
(vii) $(x,P)\ /{}\ \varepsilon\ \bm{A}\vee(x,P)\ /{}\ \varepsilon\
\bm{B}\Rightarrow(x,P)\ /{}\ \varepsilon\ \bm{A}\cap\bm{B}$.
(viii) $(x,P)\ /{}\ \varepsilon\ \bm{A}\cap\bm{B}\Leftrightarrow(x,P)\
\varepsilon\ (A^{0},A^{1}\cap B^{1})\vee(x,P)\ \varepsilon\ (B^{0},A^{1}\cap
B^{1})$.
(ix) If $(x,P)$ is a potential point of $-\bm{A}$ and $-\bm{B}$, then $(x,P)\
/{}\ \varepsilon\ \bm{A}\cap\bm{B}\Rightarrow(x,P)\ /{}\ \varepsilon\
\bm{A}\vee(x,P)\ /{}\ \varepsilon\ \bm{B}$.
(x) In general, the following hold:

$(x,P)\ \varepsilon\
\bigcup\bm{\mathcal{F}}\Leftrightarrow\exists_{X_{P^{1}}\in\mathcal{F}^{1}}\bigg{(}(x,P)\
\varepsilon\ \bigg{(}X_{P^{1}},\bigcap\mathcal{F}^{0}\bigg{)}\bigg{)},$
$(x,P)\ \varepsilon\
\bigcap\bm{\mathcal{F}}\Leftrightarrow\forall_{(X_{P^{1}},X_{P^{0}})\in\bm{\mathcal{F}}}\big{(}(x,P)\
\varepsilon\ (X_{P^{1}},X_{P^{0}})\big{)},$ $(x,P)\ /{}\ \varepsilon\
\bigcup\bm{\mathcal{F}}\Leftrightarrow\forall_{(X_{P^{1}},X_{P^{0}})\in\bm{\mathcal{F}}}\big{(}(x,P)\
/{}\ \varepsilon\ (X_{P^{1}},X_{P^{0}})\big{)},$ $(x,P)\ /{}\ \varepsilon\
\bigcap\bm{\mathcal{F}}\Leftrightarrow\exists_{X_{P^{0}}\in\mathcal{F}^{0}}\bigg{(}(x,P)\
\varepsilon\ \bigg{(}X_{P^{0}},\bigcap\mathcal{F}^{1}\bigg{)}\bigg{)}.$

(xi) If $(x,P)$ is a potential point of $\bm{\mathcal{F}}$, the following
hold:

$(x,P)\ \varepsilon\
\bigcup\bm{\mathcal{F}}\Leftrightarrow\exists_{(X_{P^{1}},X_{P^{0}})\in\bm{\mathcal{F}}}\big{(}(x,P)\
\varepsilon\ (X_{P^{1}},X_{P^{0}})\big{)},$ $(x,P)\ /{}\ \varepsilon\
\bigcap\bm{\mathcal{F}}\Leftrightarrow\exists_{(X_{P^{1}},X_{P^{0}})\in\bm{\mathcal{F}}}\big{(}(x,P)\
/{}\ \varepsilon\ (X_{P^{1}},X_{P^{0}})\big{)}.$

(xii) If $\bm{B}\in\bm{\mathcal{F}}$, then
$\bm{B}\subseteq\bigcup\bm{\mathcal{F}}$.

###### Proof.

(i) Suppose first that $A^{1}\subseteq B^{1}$ and $B^{0}\subseteq A^{0}$, and
let $(x,P)\subseteq\bm{A}$ i.e., $P^{1}(x)$ and $A^{0}\subseteq P$. As
$P^{1}(x)\Rightarrow Q^{1}(x)$ and $B^{0}\subseteq A^{0}\subseteq P$, we
conclude that $(x,P)\ \varepsilon\ \bm{B}$. For the converse inclusion let
$x\in A^{1}$. As $(x,A^{0})\ \varepsilon\ \bm{A}$, we get $(x,A^{0})\
\varepsilon\ \bm{B}$ i.e., $x\in B^{1}$ and $B^{0}\subseteq A^{0}$. As $x\in
A^{1}$ is arbitrary, we conclude that $A^{1}\subseteq B^{1}$, hence
$\bm{A}\subseteq\bm{B}$.
(ii) If $x\in A^{1}$ and $A^{0}\subseteq P$, then $x\in A^{1}\cup B^{1}$ and
$A^{0}\cap B^{0}\subseteq A^{0}\subseteq P$ i.e., $(x,P)\ \varepsilon\
\bm{A}\cup\bm{B}$. If $x\in B^{1}$ and $B^{0}\subseteq P$, we work similarly.
(iii) We have that $(x,P)\ \varepsilon\ (A^{1}\cup B^{1},A^{0}\cap
B^{0}):\Leftrightarrow x\in A^{1}\cup B^{1}\wedge A^{0}\cap B^{0}\subseteq P$.
If $x\in A^{1}$, then $(x,P)\ \varepsilon\ (A^{1},A^{0}\cap B^{0})$, while if
$x\in B^{1}$, then $(x,P)\ \varepsilon\ (B^{1},A^{0}\cap B^{0})$. Conversely,
$(x,P)\ \varepsilon\ (A^{1},A^{0}\cap B^{0})$, then $x\in A^{1}\subseteq
A^{1}\cup B^{1}$, and as $A^{0}\cap B^{0}\subseteq P$, we get $(x,P)\
\varepsilon\ \bm{A}\cup\bm{B}$. If $(x,P)\ \varepsilon\ (B^{1},A^{0}\cap
B^{0})$, we work similarly.
(iv) We have that $(x,P)\ \varepsilon\ (A^{1}\cup B^{1},A^{0}\cap
B^{0}):\Leftrightarrow x\in A^{1}\cup B^{1}\wedge A^{0}\cap B^{0}\subseteq P$.
If $x\in A^{1}$, and as $A^{0}\subseteq P$, we get $(x,P)\ \varepsilon\
\bm{A}$. Similarly, if $x\in B^{1}$, we get $(x,P)\ \varepsilon\ \bm{B}$.
(v) We have that $(x,P)\ \varepsilon\ (A^{1}\cap B^{1},A^{0}\cup
B^{0}):\Leftrightarrow x\in A^{1}\cap B^{1}\wedge A^{0}\cup B^{0}\subseteq P$,
hence $x\in A^{1}\wedge A^{0}\subseteq P$ and $x\in B^{1}\wedge B^{0}\subseteq
P$. Conversely, if $x\in A^{1}\wedge A^{0}\subseteq P$ and $x\in B^{1}\wedge
B^{0}\subseteq P$, then $x\in A^{1}\cap B^{1}\wedge A^{0}\cup B^{0}\subseteq
P$.
(vi) By the use of (v) in the third equivalence that follows we have that

$\displaystyle(x,P)\ /{}\ \varepsilon\ \bm{A}\cup\bm{B}$
$\displaystyle:\Leftrightarrow(x,P)\ \varepsilon\ -(\bm{A}\cup\bm{B})$
$\displaystyle\Leftrightarrow(x,P)\ \varepsilon\ (-\bm{A})\cap(-\bm{B})$
$\displaystyle\Leftrightarrow(x,P)\ \varepsilon\ (-\bm{A})\wedge(x,P)\
\varepsilon\ (-\bm{B})$ $\displaystyle\Leftrightarrow:(x,P)\ /{}\ \varepsilon\
\bm{A}\wedge(x,P)\ /{}\ \varepsilon\ \bm{B}.$

(vii)-(ix) We work as in the proof of (ii)-(iv).
(x)-(xi) These are obvious generalisations of the previous finite cases and
their proofs are similar.
(xii) It follows easily from the definition of $\bigcup\bm{\mathcal{F}}$. ∎

By Proposition 5.3(i) we get
$\bm{A}=_{\mathcal{E}^{\bm{)}\bm{(}}(X)}\bm{B}\Leftrightarrow\forall_{(x,P)\varepsilon\mathcal{X}}\big{(}\bm{x}\
\varepsilon\ \bm{A}\Leftrightarrow\bm{x}\ \varepsilon\ \bm{B}\big{)}.$
Complemented points help us also to define an inequality121212The inequality
between complemented subsets is treated differently in [18]. on
$\mathcal{E}^{\bm{)}\bm{(}}(X)$ applying strong negation on the previous
equality condition of complemented subsets and considering the “strong
negation” of $\bm{x}\ \varepsilon\ \bm{A}$ to be $\bm{x}\ /{}\ \varepsilon\
\bm{A}$, and vice versa.

######  Definition 5.4.

If $\bm{A},\bm{B}\in\mathcal{E}^{\bm{)}\bm{(}}(X)$, let the inequality
relation

$\bm{A}\neq_{\mathcal{E}^{\bm{)}\bm{(}}(X)}\bm{B}:\Leftrightarrow\exists_{(x,P)\varepsilon\mathcal{X}}\big{[}(\bm{x}\
\varepsilon\ \bm{A}\wedge\bm{x}\ /{}\ \varepsilon\ \bm{B})\vee(\bm{x}\
\varepsilon\ \bm{B}\wedge\bm{x}\ /{}\ \varepsilon\ \bm{A})\big{]}.$

The following iinequality is immediate to show.

######  Corollary 5.5.

If $\mathcal{X}\in\textnormal{{SetExtIneq}}$ and $X$ is inhabited, then
$0_{\bm{X}}\neq_{\mathcal{E}^{\bm{)}\bm{(}}(X)}1_{\bm{X}}$. Moroever, if
$(x,P)\neq_{\mathcal{E}^{\bm{)}\bm{(}}(X)}(y,Q)$, then $x\neq_{X}y$.

In analogy to subsets, the disjointness of two complemented subsets is derived
from strong negation of the corresponding overlapping relation, where strong
negation of the elementhood $(x,P)\ \varepsilon\ \bm{A}$ is understood to be
the non-elementhood $(x,P)\ /{}\ \varepsilon\ \bm{A}$, and vice versa.

######  Definition 5.6.

If $\mathcal{X}:=(X,=_{X},\neq_{X})\in\textnormal{{SetIneq}}$ and
$\bm{A},\bm{B}\in\mathcal{E}^{\bm{)}\bm{(}}(X)$, let

$\bm{A}\between\bm{B}:\Leftrightarrow\exists_{(x,P)\varepsilon\mathcal{X}}\big{(}(x,P)\
\varepsilon\ \bm{A}\wedge(x,P)\ \varepsilon\ \bm{B}\big{)},$
$\bm{A}\bm{)}\bm{(}\bm{B}:\Leftrightarrow\forall_{(x,P)\varepsilon\mathcal{X}}\big{(}(x,P)\
/{}\ \varepsilon\ \bm{A}\vee(x,P)\ /{}\ \varepsilon\ \bm{B}\big{)}.$

The above overlapping relation is equivalent to the following condition

$\exists_{(x,P)\varepsilon\bm{A}}\exists_{(y,Q)\varepsilon\bm{B}}\big{(}(x,P)=_{\mathcal{E}^{\bm{)}\bm{(}}(X)}(y,Q)\big{)}.$

Moreover, it is easy to show that $(x,P)\ \bm{)}\bm{(}\ (y,Q)\Rightarrow
x\neq_{X}y$.

######  Proposition 5.7.

Let
$\mathcal{X}:=(X,=_{X},\neq_{X}),\mathcal{Y}:=(Y,=_{Y},\neq_{Y})\in\textnormal{{SetExtIneq}}$,
$(x,P)\in\mathrm{Point}(\mathcal{X})$, $(y,Q)\in\mathrm{Point}(\mathcal{Y})$,
$\bm{A}:=(A^{1},A^{0})\in\mathcal{E}^{\bm{)}\bm{(}}(X)$, and
$\bm{C}:=(C^{1},C^{0})\in\mathcal{E}^{\bm{)}\bm{(}}(Y)$.
(i) $\bm{A}=_{\mathcal{E}^{\bm{)}\bm{(}(X)}}\bigcup\mathrm{Point}(\bm{A})$.
(ii) $\mathrm{Point}(x)$ is closed under $($arbitrary$)$ unions and
intersections.
(iii) If $\bm{A}$ is inhabited and $\bm{A}\subseteq(x,P)$, then
$\bm{A}\in\mathrm{Point}(x)$.
(iv) $(x,/{}\square_{X})\ \varepsilon\ \bm{A}\Leftrightarrow x\in A^{1}\wedge
A^{0}=_{\mathcal{E}(X)}/{}\square_{X}$.
(v) If $(x,P)\ \varepsilon\ \bm{A}$ and $(y,Q)\ \varepsilon\ \bm{C}$, then
$(x,P)\times(y,Q)\ \varepsilon\ \bm{A}\times\bm{C}$.
(vi) $(\mathrm{INT})$ $(x,P)\ \varepsilon\ (X,/{}\square_{X})$ and $(x,P)\
/{}\ \varepsilon\ (/{}\square_{X},X)$.
(vii) If $(x,P)\ \varepsilon\ \bm{A}$ and $\bm{A}\subseteq\bm{B}$, then
$(x,P)\ \varepsilon\ \bm{B}$.
(viii) If $(x,P)\ /{}\ \varepsilon\ \bm{B}$ and $\bm{A}\subseteq\bm{B}$, then
$(x,P)\ /{}\ \varepsilon\ \bm{A}$.

###### Proof.

(i) As $(x,A^{0})\ \varepsilon\ \bm{A}$, for every $x\in A^{1}$, we get

$\bigcup\mathrm{Point}(\bm{A}):=\bigg{(}\bigcup\mathrm{Point}^{1}(\bm{A}),\bigcap\mathrm{Point}^{0}(\bm{A})\bigg{)}=_{\mathcal{E}^{\bm{)}\bm{(}}(X)}\bm{A}.$

(ii) We use the definitions $(x,P)\cup(x,Q):=(x,P\cap Q)$ and
$(x,P)\cap(x,Q):=(x,P\cup Q)$.
(v) The hypotheses $x\in A^{1}\wedge A^{0}\subseteq P$ and $y\in C^{1}\wedge
C^{0}\subseteq Q$ imply that

$\big{(}(x,y),(P\times Y)\cup(X\times Q)\big{)}\ \varepsilon\
\big{(}A^{1}\times C^{1},(A^{0}\times Y)\cup(X\times C^{0})\big{)},$

as $(x,y)\in A^{1}\times C^{1}$, $(A^{0}\times Y)\subseteq(P\times Y)$, and
$(X\times C^{0})\subseteq(X\times Q)$. The rest cases follow easily. ∎

If the product of two complemented subsets is defined according to the second
type of operations on them (see [44, 18]), then Proposition 5.7(v) doesn’t
hold in general. The following propositions are straightforward to show.

######  Proposition 5.8.

Let $\mathcal{X},\mathcal{Y},f\colon X\to Y$ in
$(\textnormal{{SetExtIneq}},\textnormal{{StrExtFun}})$ with a left inverse
$g\colon Y\to X$.
(i) $f$ inverses points i.e., $f^{-1}(y,Q):=(g(y),f^{-1}(Q))$ is in
$\mathrm{Point}(\mathcal{X})$, for every
$(y,Q)\in\mathrm{Point}(\mathcal{Y})$.
(ii) If $\bm{B}\in\mathcal{E}^{\bm{)}\bm{(}}(Y)$, and $(y,Q)\ \varepsilon\
\bm{B}$, then $f^{-1}(y,Q)\ \varepsilon\ f^{-1}(\bm{B})$.
(iii) If $\bm{B}\in\mathcal{E}^{\bm{)}\bm{(}}(Y)$, and $(y,Q)\ /{}\
\varepsilon\ \bm{B}$, then $f^{-1}(y,Q)\ /{}\ \varepsilon\ f^{-1}(\bm{B})$.

######  Proposition 5.9.

Let $\mathcal{X},\mathcal{Y},f\colon X\to Y$ and $g\colon Y\to X$ in
$(\textnormal{{SetExtIneq}},\textnormal{{StrExtFun}})$. The following are
equivalent:
(i) $g$ is a left inequality-adjoint to $f$.
(ii) $f$ inverses points with $g$ as a modulus of inversion i.e.,
$f^{-1}(y,Q):=(g(y),f^{-1}(Q))\in\mathrm{Point}(\mathcal{X})$, for every
$(y,Q)\in\mathrm{Point}(\mathcal{Y})$, and $g$ inverses points with $f$ as a
modulus of inversion i.e.,
$g^{-1}(x,P):=(f(x),g^{-1}(P))\in\mathrm{Point}(\mathcal{Y})$, for every
$(x,P)\in\mathrm{Point}(\mathcal{X})$.

######  Proposition 5.10.

Let $\mathcal{X},\mathcal{Y}$ and $f\colon X\to Y$ in SetExtIneq. The
following are equivalent:
(i) There is $g\colon Y\to X$ in StrExtFun, such that $g\circ f$ is an
injection.
(ii) $f$ is an injection.
(iii) $f$ preserves points i.e., $f(x,P):=(f(x),f(P))$ is in
$\mathrm{Point}(\mathcal{Y})$, for every
$(x,P)\in\mathrm{Point}(\mathcal{X})$.

######  Remark 5.11.

If $f$ preserves points, $\bm{A}\in\mathcal{E}^{\bm{)}\bm{(}}(X)$ and $(x,P)\
\varepsilon\ \bm{A}$, then $f(x,P)\ \varepsilon\ f(\bm{A})$. Contrary to the
case of classical subsets, where $f(x)\notin f(A)\Rightarrow x\notin A$, we
have that if $f(x,P)\ /{}\ \varepsilon\ f(\bm{A})$, then $x\in
f^{-1}(f(A^{0}))$ and $f^{-1}(f(A^{1}))\subseteq P$, which does not imply, in
general, that $x\in A^{0}$ and $A^{1}\subseteq P$ i..e, $(x,P)\ /{}\
\varepsilon\ \bm{A}$, unless $f$ is an embedding (see Proposition 3.4(xiv)),
hence unless $f$ is a strong injection.

The behaviour of complemented points e.g., with respect to union of
complemented subsets causes several problems, especially when one wants to
pass from the union of complemented subsets to local properties, as in the
case of the local characterisation of a base in standard topology. It turns
out that we need to concentrate on fewer, more well-behaved complemented
points. For that, we introduce and study the so-called canonical complemented
points, which have a simple form and suit perfectly to the formulation of
equivalent local version of several concepts in $\mathrm{cs}$-topology.

######  Definition 5.12 (Canonical complemented points).

Let $\mathcal{X}:=(X,=_{X},\neq_{X})\in\textnormal{{SetExtIneq}}$. A
complemented point of the form $(x,\\{x\\}^{\neq_{X}})$, where $x\in X$, is
called canonical. Its complement is a canonical copoint. We also denote the
canonical point by $\bm{x}$, and the corresponding copoint by $-\bm{x}$. Their
sets are denoted by $\mathrm{cPoint}(X)$ and $-\mathrm{cPoint}(\mathcal{X})$,
respectively. If $\bm{A}\in\mathcal{E}^{\bm{)}\bm{(}}(X)$, the sets of
canonical points and copoints of $\bm{A}$ are denoted by
$\mathrm{cPoint}(\bm{A})$ and $-\mathrm{cPoint}(\bm{A})$, respectively.

It is imeediate to see that for canonical complemented points, and in
connection to Corollary 5.5, we have that
$\bm{x}\neq_{\mathcal{E}^{\bm{)}\bm{(}}(X)}\bm{y}\Leftrightarrow x\neq_{X}y$.
Next propoeition shows how much better the behaviour of canonical complemented
points is in comparison to arbitrary complemented points. Furthermore, case
(viii) is used in the proof of Proposition 11.5.

######  Proposition 5.13.

Let
$\mathcal{X}:=(X,=_{X},\neq_{X}),\mathcal{Y}:=(Y,=_{Y},\neq_{Y})\in\textnormal{{SetExtIneq}}$,
$x\in X$, $\bm{A}\in\mathcal{E}^{\bm{)}\bm{(}}(X)$, $(\bm{G}_{i})_{i\in I}$ a
family of complemented subsets of $\mathcal{X}$ indexed by some set
$(I,=_{I})$, and $f\colon X\to Y$ strongly extensional.
(i) $\bm{x}\ \varepsilon\ \bm{A}\Leftrightarrow x\in A^{1}$ and $\bm{x}\ /{}\
\varepsilon\ \bm{A}\Leftrightarrow x\in A^{0}$.
(ii) $\bm{x}\subseteq(x,P)\subseteq(x,/{}\square_{X})$, for every
$(x,P)\in\mathrm{Point}(\mathcal{X})$.
(iii) $\bm{A}\subseteq\bigcup\mathrm{cPoint}(\bm{A})$.
(iv) $\bm{x}\ \varepsilon\ \bm{A}\cup\bm{B}\Rightarrow\bm{x}\ \varepsilon\
\bm{A}\vee\bm{x}\ \varepsilon\ \bm{B}$.
(v) $\bm{x}\ /{}\ \varepsilon\ \bm{A}\cap\bm{B}\Rightarrow\bm{x}\ /{}\
\varepsilon\ \bm{A}\vee\bm{x}\ /{}\ \varepsilon\ \bm{B}$.
(vi) $\bm{x}\ \varepsilon\ \bigcup_{i\in
I}\bm{G}_{i}\Leftrightarrow\exists_{i\in I}(\bm{x}\ \varepsilon\ \bm{G}_{i})$.
(vii) $\bm{x}\ /{}\ \varepsilon\ \bigcap_{i\in
I}\bm{G}_{i}\Leftrightarrow\exists_{i\in I}(\bm{x}\ /{}\ \varepsilon\
\bm{G}_{i})$.
(viii) If $\bm{H}\in\mathcal{E}^{\bm{)}\bm{(}}(Y)$ and $x\in X$, then $\bm{x}\
\varepsilon\ f^{-1}(\bm{H})\Leftrightarrow\bm{f(x)}\ \varepsilon\ \bm{H}$.

###### Proof.

(i) $(x,\\{x\\}^{\neq_{X}})\ \varepsilon\ (A^{1},A^{0}):\Leftrightarrow x\in
A^{1}\wedge A^{0}\subseteq\\{x\\}^{\neq_{X}}\Leftrightarrow x\in A^{1}$. Case
(ii) is trivial, and (iii) follows from the observation
$A^{0}\subseteq\bigcap_{x\in A^{1}}\\{x\\}^{\neq_{X}}=(A^{1})^{\neq_{X}}$.
Cases (iv) and follow immediately from (i), while (vi) and (vii) are trivial
generalisations of (iv) and (v), respectively. Condition $\bm{x}\ \varepsilon\
f^{-1}(\bm{H})$ in (viii) is the conjunction $x\in f^{-1}(H^{1})$ and
$f^{-1}(H^{0})\subseteq\\{x\\}^{\neq_{X}}$, while $\bm{f(x)}\ \varepsilon\
\bm{H}$ is the conjunction $f(x)\in H^{1}$ and
$H^{0}\subseteq\\{f(x)\\}^{\neq_{X}}$. Clearly, $x\in
f^{-1}(H^{1})\Leftrightarrow f(x)\in H^{1}$. If $y\in H^{0}$, then
$y\neq_{Y}f(x)$, as $f(x)\in H^{1}$ i.e., in this proof we didn’t use the
hypothesis $f^{-1}(H^{0})\subseteq\\{x\\}^{\neq_{X}}$. If $x{{}^{\prime}}\in
f^{-1}(H^{0})$ i.e., there is some $y\in H^{0}$ with
$f(x{{}^{\prime}})=_{Y}y$, then by the hypothesis
$H^{0}\subseteq\\{f(x)\\}^{\neq_{X}}$ and the extensionality of $\neq_{Y}$ we
get $f(x{{}^{\prime}})\neq_{Y}f(x)$, and, as $f$ is strongly extensional, we
conclude that $x{{}^{\prime}}\neq_{X}x$. ∎

######  Definition 5.14.

If $\phi(x,\\{x^{\neq_{X}}\\})$ is a formula in $\mathrm{BST}$, let notational
conventions:

$\forall_{\bm{x}\varepsilon\mathcal{X}}\phi(\bm{x}):=\forall_{(x,\\{x^{\neq_{X}}\\})\in\mathrm{cPoint}(\mathcal{X})}\big{(}\phi(x,\\{x^{\neq_{X}}\\})\big{)},\
\ \ \
\exists_{\bm{x}\varepsilon\mathcal{X}}\phi(\bm{x}):=\exists_{(x,\\{x^{\neq_{X}}\\})\in\mathrm{cPoint}(\mathcal{X})}\big{(}\phi(x,\\{x^{\neq_{X}}\\})\big{)},$
$\forall_{\bm{x}\varepsilon\bm{A}}\phi(\bm{x}):=\forall_{(x,\\{x^{\neq_{X}}\\})\in\mathrm{cPoint}(\bm{A})}\big{(}\phi(x,\\{x^{\neq_{X}}\\})\big{)},\
\ \ \
\exists_{\bm{x}\varepsilon\bm{A}}\phi(\bm{x}):=\exists_{(x,\\{x^{\neq_{X}}\\})\in\mathrm{cPoint}(\bm{A})}\big{(}\phi(x,\\{x^{\neq_{X}}\\})\big{)}.$

Understanding $\bm{x}\ /{}\ \varepsilon\ \bm{A}$ as a sort of strong negation
of $\bm{x}\ \varepsilon\ \bm{A}$, then the canonical complemented points
characterise the inclusion relation between complemeneted subsets, if we
interpret the implication in Proposition 5.3(i) in the strong way. Next fact
follows immediately from Proposition 5.13(i).

######  Proposition 5.15.

If $\mathcal{X}:=(X,=_{X},\neq_{X})\in\textnormal{{SetExtIneq}}$ and
$\bm{A},\bm{B}\in\mathcal{E}^{\bm{)}\bm{(}}(X)$, then

$\bm{A}\subseteq\bm{B}\Leftrightarrow\forall_{\bm{x}\varepsilon\mathcal{X}}\big{[}(\bm{x}\
\varepsilon\ \bm{A}\Rightarrow\bm{x}\ \varepsilon\ \bm{B})\wedge(\bm{x}\ /{}\
\varepsilon\ \bm{B}\Rightarrow\bm{x}\ /{}\ \varepsilon\ \bm{A})\big{)}.$

##  6 The canonical $\mathrm{cs}$-topology induced by a metric

Metric spaces are important examples of a topological space in classical
topology, and crucial case-studies to all approaches to constructive topology.
Many of the concepts of $\mathrm{cs}$-topological spaces introduced in later
sections need to be tested on metric spaces first. In this section we combine
classical topological notions, within the constructive complemented subsets-
point of view, with the constructive theory of metric spaces.

######  Remark 6.1.

Two facts from the basic constructive theory of real numbers that are provable
within $\mathrm{MIN}$ are the following: the condition $a\geq b$ is equivalent
to the formula $\neg{(a<b)}$ (Lemma 2.18 in [6], p. 26), and the constructive
version of trichotomy of reals, according to which if $a<b$, then for every
$c\in{\mathbb{R}}$ either $c<b$ or $c>a$ (Corollary 2.17 in [6], p. 26).

First we define the canonical $\mathrm{cs}$-topology induced by some metric
$d$ on a set $(X,=_{X})$. In accordance to the canonical inequality
$\neq_{(X,d)}$ (see Definition 2.7), the empty subset of a metric space is
defined by

$/{}\square_{(X,d)}:=\\{y\in X\mid d(y,y)>0\\}.$

If $A\subseteq X$, its $\neq_{(X,d)}$-complement is defined by

$A^{\neq_{(X,d)}}:=\\{x\in X\mid\forall_{a\in A}(d(x,a)>0)\\}.$

Only a small part of the proof of the next proposition requires
$\mathrm{INT}$. The use of the extensional $/{}\square_{(X,d)}$ allows us to
provide several proofs concerning it, but not all, within $\mathrm{MIN}$.
Throughout this section $(X,=_{X},d)$, or simply $X$, is a metric space with a
metric $d$, and $\epsilon\in{\mathbb{R}}$ with $\epsilon>0$.

######  Definition 6.2 (Complemented ball).

If $x\in X$, the $\epsilon$-complemented ball around $x$ is defined by

$\bm{B}(x,\epsilon):=\big{(}[d_{x}<\epsilon],[d_{x}\geq\epsilon]\big{)},$

where

$[d_{x}<\epsilon]:=\\{x{{}^{\prime}}\in X\mid
d(x,x{{}^{\prime}})<\epsilon\\},\ \ \ \
[d_{x}\geq\epsilon]:=\\{x{{}^{\prime\prime}}\in X\mid
d(x,x{{}^{\prime\prime}})\geq\epsilon\\}.$

######  Remark 6.3.

(i) $\bm{B}(x,\epsilon)$ is a complemented subset of $(X,=_{X},\neq_{(X,d)})$
with $\bm{x}\ \varepsilon\ \bm{B}(x,\epsilon)$.
(ii) $[d_{x}\geq\epsilon]=_{\mathcal{E}(X)}[d_{x}<\epsilon]^{\neq_{(X,d)}}$,
and $\bm{B}(x,\epsilon)$ is a $1$-tight complemented subset.
(iii) If $\epsilon_{1},\epsilon_{2}>0$, then we have that
$\epsilon_{1}\leq\epsilon_{2}\Rightarrow\bm{B}(x,\epsilon_{1})\subseteq\bm{B}(x,\epsilon_{2})$.

###### Proof.

(i) If $x{{}^{\prime}}\in[d_{x}<\epsilon]$ and
$x{{}^{\prime\prime}}\in[d_{x}\geq\epsilon]$, then by the triangle inequality
we have that $(x,x{{}^{\prime\prime}})\leq
d(x,x{{}^{\prime}})+d(x{{}^{\prime}},x{{}^{\prime\prime}})$, hence
$d(x{{}^{\prime}},x{{}^{\prime\prime}})\geq
d(x,x{{}^{\prime\prime}})-d(x,x{{}^{\prime}})>0$. Clearly, $\bm{x}\
\varepsilon\ \bm{B}(x,\epsilon)$ if and only if $x\in[d_{x}<\epsilon]$, which
is trivially the case.
(ii) The inclusion
$[d_{x}\geq\epsilon]\subseteq[d_{x}<\epsilon]^{\neq_{(X,d)}}$ follows by case
(i). For the converse inclusion, let $y\in[d_{x}<\epsilon]^{\neq_{(X,d)}}$
with $d(x,y)<\epsilon$ i.e., $y\in[d_{x}<\epsilon]$. By hypothesis on $y$ we
get $d(y,y)>0$, which is impossible, hence, $d(x,y)\geq\epsilon$.
$1$-tightness of $\bm{B}(x,\epsilon)$ follows from the implication
$\neg{(d(x,x{{}^{\prime}})<\epsilon)}\Rightarrow
d(x,x{{}^{\prime}})\geq\epsilon$.
(iii) If $\epsilon_{1}\leq\epsilon_{2}$, then
$[d_{x}<\epsilon_{1}]\subseteq[d_{x}<\epsilon_{2}]$ and
$[d_{x}\geq\epsilon_{2}]\subseteq[d_{x}\geq\epsilon_{1}]$. ∎

######  Definition 6.4 (The canonical $\mathrm{cs}$-topology induced by a
metric).

If $\bm{G}\in\mathcal{E}^{\bm{)}\bm{(}}(X)$, let the formula

$T_{d}(\bm{G}):=\forall_{\bm{x}\varepsilon\bm{G}}\exists_{\epsilon>0}\big{(}\bm{B}(x,\epsilon)\subseteq\bm{G}\big{)}:\Leftrightarrow\forall_{\bm{x}\varepsilon\bm{G}}\exists_{\epsilon>0}\big{(}[d_{x}<\epsilon]\subseteq
G^{1}\wedge G^{0}\subseteq[d_{x}\geq\epsilon]\big{)}.$

If $T_{d}(\bm{G})$, we call $\bm{G}$ a $\bm{\mathcal{T}}_{d}$-open
complemented subset of $X$. Let their set $\bm{\mathcal{T}}_{d}$ be the
canonical $\mathrm{cs}$-topology on $X$ induced by its metric $d$. If $\bm{G}$
is a $\bm{\mathcal{T}}_{d}$-open complemented subset of $X$, a modulus of
openness $\mathrm{op}_{\bm{G}}$ for $\bm{G}$ is a function
$\mathrm{op}_{\bm{G}}\colon G^{1}\to(0,+\infty)$, such that

$\forall_{\bm{x}\varepsilon\bm{G}}\big{(}\bm{B}(x,\mathrm{op}_{\bm{G}}(x))\subseteq\bm{G}\big{)}.$

If $\bm{G},\bm{H}\in\bm{\mathcal{T}}_{d}$, such that
$\bm{G}=_{\mathcal{E}^{\bm{)}\bm{(}}(X)}\bm{H}$, we require that
$\mathrm{op}_{\bm{G}}=_{\mathbb{F}\big{(}G^{1},(0,+\infty)\big{)}}\mathrm{op}_{\bm{H}}$.

The extensionality of the relations $<,\leq$ in ${\mathbb{R}}$ and the
function-property of the assignment routine $d_{x}\colon
X\rightsquigarrow{\mathbb{R}}$, where
$d_{x}(x{{}^{\prime}}):=d(x,x{{}^{\prime}})$, for every $x{{}^{\prime}}\in X$,
imply that $T_{d}(\bm{G})$ is an extensional property on
$\mathcal{E}^{\bm{)}\bm{(}}(X)$. By Proposition 5.15(iii) quantification on
the canonical points of $\bm{G}$ in the formula $T_{d}(\bm{G})$ and in the
definition of the modulus $\mathrm{op}_{\bm{G}}$ can be replaced by
quantification on $G^{1}$. The introduction of a modulus of openness is an
instance of the so-called“modular” approach within the constructive theory of
metric space, according to which functions that are induced by the axiom of
choice are part of the witnessing data that accompany a fully constructive
formulation of the related concept.

######  Proposition 6.5.

The set $\bm{\mathcal{T}}_{d}$-open complemented subsets of $X$ contains
$(X,/{}\square_{X}),(/{}\square_{X},X)$, it is closed under finite unions and
arbitrary unions of set-indexed familes of $\bm{\mathcal{T}}_{d}$-open
complemented subsets of $X$.

###### Proof.

To show $T_{d}(X,/{}\square_{(X,d)})$, let $\bm{x}\ \varepsilon\
(X,/{}\square_{X})$ and take e.g., $\epsilon:=1$. Clearly, we have that
$[d_{x}<1]\subseteq X$. The inclusion $/{}\square_{(X,d)}\subseteq[d_{x}\geq
1]$ follows trivially in $\mathrm{INT}$. The proof though, of
$T_{d}(/{}\square_{(X,d)},X)$ can be given within $\mathrm{MIN}$ as follows.
Let $\bm{x}\ \varepsilon\ (/{}\square_{(X,d)},X)$ i.e., $x\in/{}\square_{X}$
and $X\subseteq\\{x\\}^{\neq_{X}}$. If $\epsilon_{x}:=\frac{d(x,x)}{2}>0$, we
show that $[d_{x}<\epsilon_{x}]\subseteq/{}\square_{X}$ and
$X\subseteq[d_{x}\geq\epsilon_{x}]$. For the first inclusion, if
$x{{}^{\prime}}\in X$ with $d(x,x{{}^{\prime}})<\frac{d(x,x)}{2}$, then
$2d(x{{}^{\prime}},x)<d(x,x)\Leftrightarrow d(x,x)-2d(x{{}^{\prime}},x)>0.$ As

$d(x,x)\leq d(x,x{{}^{\prime}})+d(x{{}^{\prime}},x)\leq
d(x,x{{}^{\prime}})+d(x{{}^{\prime}},x{{}^{\prime}})+d(x{{}^{\prime}},x),$

we get $d(x,x)-2d(x,x{{}^{\prime}})\leq d(x{{}^{\prime}},x{{}^{\prime}})$,
hence $0<d(x,x)-2d(x{{}^{\prime}},x)\leq d(x{{}^{\prime}},x{{}^{\prime}})$
i.e., $x{{}^{\prime}}\in/{}\square_{(X,d)}$. For the second inclusion, if
$x{{}^{\prime\prime}}\in X$, the required inequality
$d(x{{}^{\prime\prime}},x)\geq\frac{d(x,x)}{2}$ follows immediately by the
triangle inequality. Next we show that if $T_{d}(\bm{G})$ and $T_{d}(\bm{H})$,
then $T_{d}(\bm{G}\cap\bm{H})$. If $\bm{x}\ \varepsilon\ \bm{G}\cap\bm{H}$,
then $\bm{x}\ \varepsilon\ \bm{G}$ and $\bm{x}\ \varepsilon\ \bm{H}$. Let
$\epsilon_{1}>0$ with $\bm{B}(x,\epsilon_{1})\subseteq\bm{G}$, and let
$\epsilon_{2}>0$ with $\bm{B}(x,\epsilon_{2})\subseteq\bm{H}$. If

$\epsilon:=\min\\{\epsilon_{1},\epsilon_{2}\\}=:\epsilon_{1}\wedge\epsilon_{2},$

then $\epsilon>0$ too (see [8], p. 57). By Remark 6.8(iii) and since
$\epsilon\leq\epsilon_{1}$ and $\epsilon\leq\epsilon_{2}$, we have that
$\bm{B}(x,\epsilon)\subseteq\bm{B}(x,\epsilon_{1})\subseteq\bm{G}$ and
$\bm{B}(x,\epsilon)\subseteq\bm{B}(x,\epsilon_{2})\subseteq\bm{H}$, and hence
by Corollary 4.5(i) $\bm{B}(x,\epsilon)\subseteq\bm{G}\cap\bm{H}$. If
$T_{d}(\bm{G}_{i})$, for every $i\in I$, and $\bm{x}\ \varepsilon\
\bigcup_{i\in I}\bm{G}_{i}$, then by Proposition 5.15(vi) $\exists_{i\in
I}(\bm{x}\ \varepsilon\ \bm{G}_{i})$. If $\epsilon>0$ with
$\bm{B}(x,\epsilon)\subseteq\bm{A}_{i}$, then by Corollary 4.5(ii) we get
$\bm{B}(x,\epsilon)\subseteq\bigcup_{i\in I}\bm{G}_{i}$. ∎

By inspection of the previous proof, we get the following moduli of openness.
Notice that for the modulus of openness for $(X,\ /{}\square_{X})$ any
constant function to $(0,+\infty)$ would do.

######  Remark 6.6.

(i) Let $\mathrm{op}_{(X,\ /{}\square_{X})}\colon X\to(0,+\infty)$ be the
constant function $1$.
(ii) Let $\mathrm{op}_{(\
/{}\square_{X},X)}\colon/{}\square_{X}\to(0,+\infty)$ be defined by the rule
$x\mapsto\frac{d(x,x)}{2}$, for every $x$ $\in$ $/{}\square_{(X,d)}$.
(iii) If $\mathrm{op}_{\bm{G}}$ and $\mathrm{op}_{\bm{H}}$ are is a moduli of
openness for $\bm{G}$ and $\bm{H}$ , respectively, let
$\mathrm{op}_{\bm{G}\cap\bm{H}}:=\mathrm{op}_{\bm{G}}\wedge\mathrm{op}_{\bm{H}}$
be a modulus of openness for $\bm{G}\cap\bm{H}$, where
$(\mathrm{op}_{\bm{G}}\wedge\mathrm{op}_{\bm{H}})(x):=\mathrm{op}_{\bm{G}}(x)\wedge\mathrm{op}_{\bm{H}}(x)$,
for every $x\in G^{1}\cap H^{1}$.

Notice that the assignment routine $x\mapsto d(x,x)$, where
$x\in/{}\square_{(X,d)}$, takes values in (or is a term of set) $(0,+\infty)$,
as by hypothesis $x$ is a variable of set $/{}\square_{(X,d)}$. What the axiom
of metric space $\forall_{x\in X}\big{(}d(x,x)=_{{\mathbb{R}}}0\big{)}$
guarantees is that there will be no constant of set $/{}\square_{(X,d)}$, but
the assignment routine $x\mapsto d(x,x)$ is only a rule that transforms a
variable of set $/{}\square_{(X,d)}$ to a term of set $(0,+\infty)$,
independently from the fact that domain of this rule cannot be inhabited by
some constant. To determine a modulus of openness for the union $\bigcup_{i\in
I}\bm{G}_{i}$ with $\mathrm{op}_{\bm{G}_{i}}$ a modulus of openness for
$\bm{G}_{i}$, for every $i\in I$, we need to add more information to the
union. One can add, for example, a projection function
$\textnormal{{pr}}\colon\bigcup_{i\in I}G^{1}_{i}\to I$, such that $x\in
G_{\textnormal{{pr}}(x)}^{1}$, for every $x\in\bigcup_{i\in I}G^{1}_{i}$. In
this way the original union $\bigcup_{i\in I}G^{1}_{i}$ is equal to the
disjoint union $\bigcup_{x\in\bigcup_{i\in
I}G_{i}^{1}}G_{\textnormal{{pr}}(x)}$. And then one can define
$\mathrm{op}_{\bigcup_{i\in
I}G^{1}_{i}}(x):=\mathrm{op}_{G_{\textnormal{{pr}}(x)}}(x)$, for every
$x\in\bigcup_{i\in I}G^{1}_{i}$. Another approach will be presented in Remark
6.13.

######  Definition 6.7.

Let $\bm{\mathcal{T}}_{d}:=\\{\bm{G}\in\mathcal{E}^{\bm{)}\bm{(}}(X)\mid
T_{d}(\bm{G})\\}$ be the canonical $\mathrm{cs}$-topology on $X$ induced by
$d$, and

$\bm{B}(X):=\\{\bm{G}\in\mathcal{E}^{\bm{)}\bm{(}}(X)\mid\exists_{x{{}^{\prime}}\in
X}\exists_{\epsilon{{}^{\prime}}>0}\big{(}\bm{G}=_{\mathcal{E}^{\bm{)}\bm{(}}(X)}\bm{B}(x{{}^{\prime}},\epsilon{{}^{\prime}})\\}$

the set of complemented balls of $X$. If $\bm{G}$ is an arbitrary open
complemented subset in $\bm{\mathcal{T}}_{d}$, we call a function
$\beta_{\bm{G}}\colon G^{1}\to\bm{B}(X)$ satisfying $\bm{y}\ \varepsilon\
\beta_{\bm{G}}(y)$ and
$\beta_{\bm{B}(x,\epsilon)}(y)\subseteq\bm{B}(x,\epsilon)$, for every $y\in
G^{1}$, a base-module for $\bm{G}$, or a $\bm{B}(X)$-module for $\bm{G}$. We
call such a base-module covering, if

$\bm{G}=_{\mathcal{E}^{\bm{)}\bm{(}}(X)}\bigcup_{y\in
G^{1}}\beta_{\bm{G}}(y).$

A family $(\beta_{\bm{G}})_{\bm{G}\in\bm{\mathcal{T}}_{d}}$ with
$\beta_{\bm{G}}$ a $\bm{B}(X)$-module for $\bm{G}$, for every
$\bm{G}\in\bm{\mathcal{T}}_{d}$, is $\bm{B}(X)$-module for
$\bm{\mathcal{T}}_{d}$. If $\mathrm{op}_{\bm{G}}$ is a module of openness for
$\bm{G}$, the canonical $\bm{B}(X)$-module for $\bm{G}$ induced by
$\mathrm{op}_{\bm{G}}$ is defined by
$\beta_{\bm{G}}(x):=\bm{B}(x,\mathrm{op}_{\bm{G}}(x))$, for every $x\in
G^{1}$.

Clearly, a base-modulus $\beta_{\bm{G}}$ for $\bm{G}$ defines a module of
openness $\mathrm{op}_{\bm{G}}$ for $\bm{G}$ by taking the radius of the
corresponding complemented ball i.e., the two concepts are equivalent for
metric spaces.

######  Remark 6.8.

(i) The complemented ball $\bm{B}(x,\epsilon)$ is a
$\bm{\mathcal{T}}_{d}$-open complemented subset.
(ii) The canonical $\bm{B}(X)$-module for $\bm{B}(x,\epsilon)$ is covering.

###### Proof.

(i) If $y\in[d_{x}<\epsilon]$, let
$\mathrm{op}_{\bm{B}(x,\epsilon)}(y):=\epsilon-d(x,y)>0$. For
$\bm{B}(y,\mathrm{op}_{\bm{B}(x,\epsilon)}(y))$ we have that

$[d_{y}<\mathrm{op}_{\bm{B}(x,\epsilon)}(y)]\subseteq[d_{x}<\epsilon]\ \ \&\ \
[d_{x}\geq\epsilon]\subseteq[d_{y}\geq\mathrm{op}_{\bm{B}(x,\epsilon)}(y)].$

For the first inclusion we have that, if
$d(y,z)<\mathrm{op}_{\bm{B}(x,\epsilon)}(y)$, then $d(x,z)\leq
d(x,y)+d(y,z)<d(x,y)+\epsilon-d(x,y)<\epsilon$, and for the second inclusion,
if $d(x,z)\geq\epsilon$, then $\epsilon-d(x,y)\leq d(x,z)-d(x,y)\leq d(y,z)$.
(ii) Let the assignment routine
$y\mapsto\beta_{\bm{B}(x,\epsilon)}(y):=\mathrm{op}_{\bm{B}(x,\epsilon)}(y)$,
which is a function, as $d$ is a function. Clearly, $\bm{y}\ \varepsilon\
\bm{B}(y,\mathrm{op}_{\bm{B}(x,\epsilon)}(y))$, and by case (i)
$\bm{B}(y,\mathrm{op}_{\bm{B}(x,\epsilon)}(y))\subseteq\bm{B}(x,\epsilon)$. By
definition of the canonical base-module for $\bm{B}(x,\epsilon)$ we have that

$\bigcup_{y\in[d_{x}<\epsilon]}\beta_{\bm{B}(x,\epsilon)}(y):=\bigcup_{y\in[d_{x}<\epsilon]}\bm{B}(y,\mathrm{op}_{\bm{B}(x,\epsilon)}(y)):=\bigg{(}\bigcup_{y\in[d_{x}<\epsilon]}[d_{y}<\mathrm{op}_{\bm{B}(x,\epsilon)}(y)],\bigcap_{y\in[d_{x}<\epsilon]}[d_{y}\geq\mathrm{op}_{\bm{B}(x,\epsilon)}(y)]\bigg{)}.$

If $y\in[d_{x}<\epsilon]$, then
$[d_{x}<\epsilon]=_{\mathcal{E}(X)}\bigcup_{y\in[d_{x}<\epsilon]}[d_{y}<\mathrm{op}_{\bm{B}(x,\epsilon)}(y)]$,
and as by (i)
$[d_{y}<\mathrm{op}_{\bm{B}(x,\epsilon)}(y)]\subseteq[d_{x}<\epsilon]$ and
$[d_{x}\geq\epsilon]\subseteq[d_{y}\geq\mathrm{op}_{\bm{B}(x,\epsilon)}(y)]$,
we get
$[d_{x}\geq\epsilon]\subseteq\bigcap_{y\in[d_{x}<\epsilon]}[d_{y}\geq\mathrm{op}_{\bm{B}(x,\epsilon)}(y)].$
Next we show the converse inclusion

$\bigcap_{y\in[d_{x}<\epsilon]}[d_{y}\geq\mathrm{op}_{\bm{B}(x,\epsilon)}(y)]\subseteq[d_{x}\geq\epsilon].$

Let
$z\in\bigcap_{y\in[d_{x}<\epsilon]}[d_{y}\geq\mathrm{op}_{\bm{B}(x,\epsilon)}(y)]$
and suppose that $d(x,z)<\epsilon$ i.e., $z\in[d_{x}<\epsilon]$. By the
hypothesis on $z$ we get $z\in[d_{z}\geq\mathrm{op}_{\bm{B}(x,\epsilon)}(z)]$
i.e., $d(z,z)\geq\mathrm{op}_{\bm{B}(x,\epsilon)}(z)>0$, which is absurd,
hence $d(x,z)\geq\epsilon$. ∎

######  Remark 6.9.

If $\bm{G}$ is an element of $\bm{\mathcal{T}}_{d}$ and $\beta_{\bm{G}}\colon
G^{1}\to\bm{B}(X)$ is a base-module for $\bm{G}$, then in order to show that
the family of complemented balls $\big{(}\beta_{\bm{G}}(y))_{y\in G^{1}}$
covers $\bm{G}$ i.e.,

$\bm{G}=_{\mathcal{E}^{\bm{)}\bm{(}}(X)}\bigcup_{y\in
G^{1}}\beta_{\bm{G}}(y):=\bigg{(}\bigcup_{y\in
G^{1}}[d_{y}<\mathrm{op}_{\bm{G}}(y)],\bigcap_{y\in
G^{1}}[d_{y}\geq\mathrm{op}_{\bm{G}}(y)]\bigg{)},$

we only need to show, as all other inclusions follow easily, the so-called
here covering-inclusion for $\beta_{\bm{G}}$:

$(\mathrm{CI}_{\bm{G}})\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \bigcap_{y\in
G^{1}}[d_{y}\geq\mathrm{op}_{\bm{G}}(y)]\subseteq G^{0}.\ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ $

If $(\mathrm{CI}_{\bm{G}})$ holds, then we say that $\beta_{\bm{G}}$ is a
covering base-module for $\bm{G}$.

######  Remark 6.10.

Even if $\beta_{\bm{G}}$ and $\beta_{\bm{H}}$ are covering base-modules for
$\bm{G}$ and $\bm{H}$, respectively, we cannot show, in general, that these
modules induce a covering base-module for $\bm{G}\cap\bm{H}$ by the method
generated in the proof of Proposition 6.5. Suppose that

$\bm{H}=_{\mathcal{E}^{\bm{)}\bm{(}}(X)}\bigcup_{z\in
H^{1}}\beta_{\bm{H}}(z):=\bigg{(}\bigcup_{z\in
H^{1}}[d_{z}<\mathrm{op}_{\bm{H}}(z)],\bigcap_{z\in
H^{1}}[d_{z}\geq\mathrm{op}_{\bm{H}}(z)]\bigg{)}.$

In order to show the crucial inequality

$\bigcap_{w\in G^{1}\cap
H^{1}}[d_{w}\geq\mathrm{op}_{\bm{G}}(w)\wedge\mathrm{op}_{\bm{H}}(w)]\subseteq
G^{0}\cup H^{0},$

it suffices that $\bm{G}\cap\bm{H}$ is $1$-tight i.e., $\neg{(x\in G^{1}\cap
H^{1})}\Rightarrow x\in G^{0}\cup H^{0}$. To show this, suppose
$k\in\bigcap_{w\in G^{1}\cap
H^{1}}[d_{w}\geq\mathrm{op}_{\bm{G}}(w)\wedge\mathrm{op}_{\bm{H}}(w)]$ and
$k\in x\in G^{1}\cap H^{1}$. Then
$k\in[d_{w}\geq\mathrm{op}_{\bm{G}}(w)\wedge\mathrm{op}_{\bm{H}}(w)]\Leftrightarrow
d(k,k)\geq\mathrm{op}_{\bm{G}}(k)\wedge\mathrm{op}_{\bm{H}}(k)>0$, which is
absurd, hence $k\in G^{0}\cup H^{0}$.

As we show next, the covering inclusion holds for many elements of
$\bm{\mathcal{T}}_{d}$. For the case of intersection of two complemented balls
in Proposition 6.12(iii) we need case (ii) of the following lemma, while for
the union of two complemented balls we need its case (iv).

######  Lemma 6.11.

If $x,x{{}^{\prime}},y,y{{}^{\prime}}\in{\mathbb{R}}$, the following hold:
(i) $\neg{(x<0\wedge y<0)}\Rightarrow(x\geq 0\vee y\geq 0)$.
(ii) $\neg{(x<y\wedge x{{}^{\prime}}<y{{}^{\prime}})}\Rightarrow(x\geq y\vee
x{{}^{\prime}}\geq y{{}^{\prime}})$.
(iii) $\neg{(x<0\vee y<0)}\Rightarrow(x\geq 0\wedge y\geq 0)$.
(iv) $\neg{(x<y\vee x{{}^{\prime}}<y{{}^{\prime}})}\Rightarrow(x\geq y\wedge
x{{}^{\prime}}\geq y{{}^{\prime}})$.

###### Proof.

(i) For all properties on the order of reals used in this proof we refer to
[8], p. 57, Ex. 3. We have that $x<0\wedge y<0\Leftrightarrow x\vee
y:=\max\\{x,y\\}<0$, hence $\neg{(x<0\wedge y<0)}\Rightarrow\neg{(x\vee
y<0)}$. By Remark 6.1 we get $x\vee y\geq 0$, which in turn implies $x\geq 0$
or $y\geq 0$.
(ii) The hypothesis is equivalent to $\neg{(x-y<0\wedge
x{{}^{\prime}}-y{{}^{\prime}}<0)}$, and we use case (i).
(iii) We suppose $x<0$, and we get $x<0\vee y<0$, hence $\bot$. We get $x\geq
0$ by Remark 6.1. We work similarly, if we suppose $y<0$.
(iv) The hypothesis is equivalent to $\neg{(x-y<0\vee
x{{}^{\prime}}-y{{}^{\prime}}<0)}$, and we use case (iii). ∎

######  Proposition 6.12.

Let $\mathcal{I}:=(I,=_{I},\neq_{I})\in\textnormal{{SetExtIneq}}$, such that
$i\neq_{I}j$ is discrete $(\textnormal{{Ineq}}_{6})$, and let $\bm{G}_{i}$ be
$\bm{\mathcal{T}}_{d}$-open, every $i\in I$, such that
$\bm{G}_{i}\cap\bm{G}_{j}\subseteq(/{}\square_{X},X)$, for every $i,j\in I$
with $i\neq_{I}j$.
(i) The canonical $\bm{B}(X)$-modules for $(X,/{}\square_{X})$ and
$(/{}\square_{X},X)$ are covering.
(ii) $($Myhill’s unique choice principle$)$ If for every $i\in I$ the
canonical $\bm{B}(X)$-module for $\bm{G}_{i}$ is covering, then it is covering
for $\bigcup_{i\in I}\bm{G}_{i}$.
(iii) The canonical $\bm{B}(X)$-module for
$\bm{B}(x,\epsilon)\cap\bm{B}(y,\delta)$ is covering.
(iv) The canonical modulus of opennes for
$\bm{B}(x,\epsilon)\cup\bm{B}(y,\delta)$ is defined by the rule

$\mathrm{op}_{\bm{B}(x,\epsilon)\cup\bm{B}(y,\delta)}(z):=[\epsilon-d(x,z)]\vee[\delta-d(y,z)]=:\eta_{\zeta},$

for every $z\in[d_{x}<\epsilon]\cup[d_{y}<\delta]$, and the canonical
$\bm{B}(X)$-module for $\bm{B}(x,\epsilon)\cup\bm{B}(y,\delta)$ is covering.
(v) A canonical complemented copoint $(x^{\neq_{(X,d)}},x)$ is
$\bm{\mathcal{T}}_{d}$-open with a covering $\bm{B}(X)$-module for it.

###### Proof.

(i) $(\mathrm{MIN})$ We need to show the covering-inclusion $\bigcap_{x\in
X}[d_{x}\geq 1]\subseteq/{}\square_{X}$. Let $y\in X$ such that $d(x,y)\geq
1$, for every $x\in X$. Consequently, $d(y,y)\geq 1>0$, hence
$y\in/{}\square_{X}$. For the case of $(/{}\square_{X},X)$, the proof of the
covering-inclusion $\bigcap_{y\in\
{/{}\square_{X}}}[d_{y}\geq\frac{d(y,y)}{2}]\subseteq X$ is shown in the proof
of Proposition 6.5. For the following left inclusion

$\bigcup_{y\in\
{/{}\square_{X}}}\bigg{[}d_{y}<\frac{d(y,y)}{2}\bigg{]}\subseteq{/{}\square_{X}}\
\ \&\ \ /{}\square_{X}\subseteq\bigcup_{y\in\
{/{}\square_{X}}}\bigg{[}d_{y}<\frac{d(y,y)}{2}\bigg{]},$

we use the fact shown in the proof of Proposition 6.5 that
$[d_{y}<\frac{d(y,y)}{2}]\subseteq/{}\square_{X}$, for every
$y\in/{}\square_{X}$. For the second inclusion, each element $y$ of
$/{}\square_{X}$ is in $[d_{y}<\frac{d(y,y)}{2}]$, and hence in their union.
(ii) For every $i\in I$ let the covering-inclusion $\bigcap_{y_{i}\in
G_{i}^{1}}[d_{y_{i}}\geq\mathrm{op}_{\bm{G}_{i}}(y_{i})]\subseteq G_{i}^{0}$.
We define $\mathrm{op}_{\bigcup}\colon\bigcup_{i\in I}G_{i}^{1}\to(0,+\infty)$
by $\mathrm{op}_{\bigcup}(x):=\mathrm{op}_{\bm{G}_{i}}(x)$, where $i$ is the
unique (up to equality) element of $I$ sith $x\in G_{i}^{1}$. If $x\in
G_{j}^{1}$ with $G_{i}^{1}\cap G_{j}^{1}\subseteq/{}\square_{X}$, then we get
a contradiction i.e., $\neg{(i\neq_{I}j)}$, hence by
$(\textnormal{{Ineq}}_{6})$ $i=_{I}j$. By our requirement in Definition 9.8 we
get $\mathrm{op}_{\bm{G}_{i}}(x)=_{{\mathbb{R}}}\mathrm{op}_{\bm{G}_{j}}(x)$.
The required covering-inclusion is

$\bigcap_{z\in\bigcup_{i\in
I}G_{i}^{1}}[d_{z}\geq\mathrm{op}_{\bigcup}(z)]\subseteq\bigcap_{i\in
I}G_{i}^{0}.$

If $k\in\bigcap_{z\in\bigcup_{i\in
I}G_{i}^{1}}[d_{z}\geq\mathrm{op}_{\bigcup}(z)]$, then for every $z\in
G_{i}^{1}$ we get $d(z,k)\geq\mathrm{op}_{\bm{G}_{i}}(z)$, hence $k\in
G_{i}^{0}$. As $i\in I$ is arbitray, the required covering-inclusion follows.
(iii) The covering-inclusion for
$\bm{B}(x,\epsilon)\cap\bm{B}(y,\delta)=\big{(}[d_{x}<\epsilon]\cap[d_{y}<\delta],[d_{x}\geq\epsilon]\cup[d_{y}\geq\delta]$
is

$\bigcap_{v\in[d_{x}<\epsilon]\cap[d_{y}<\delta]}[d_{v}\geq\mathrm{op}_{\bm{B}(x,\epsilon)}(v)\wedge\mathrm{op}_{\bm{B}(y,\delta)}(v)]\subseteq[d_{x}\geq\epsilon]\cup[d_{y}\geq\delta].$

Let
$k\in\bigcap_{v\in[d_{x}<\epsilon]\cap[d_{y}<\delta]}[d_{v}\geq\mathrm{op}_{\bm{B}(x,\epsilon)}(v)\wedge\mathrm{op}_{\bm{B}(y,\delta)}(v)]$,
and suppose that $k\in[d_{x}<\epsilon]\cap[d_{y}<\delta]\Leftrightarrow
d(x,k)<\epsilon\wedge d(y,k)<\delta$. Then
$k\in[d_{k}\geq\mathrm{op}_{\bm{B}(x,\epsilon)}(k)\wedge\mathrm{op}_{\bm{B}(y,\delta)}(k)]$
i.e.,
$d(k,k)\geq\mathrm{op}_{\bm{B}(x,\epsilon)}(k)\wedge\mathrm{op}_{\bm{B}(y,\delta)}(k)>0$,
which is impossible. Hence, $\neg{\big{(}d(x,k)<\epsilon\wedge
d(y,k)<\delta\big{)}}$. By Lemma 6.11(ii) we get the required disjunction
$d(x,k)\geq\epsilon$ or $d(y,k)\geq\delta$.
(iv) As $z\in[d_{x}<\epsilon]\cup[d_{y}<\delta]$, we have that
$\epsilon-d(x,z)>0$ or $\delta-d(y,z)>0$, hence $\eta_{z}>0$. First we show
that $[d_{z}<\eta_{z}]\subseteq[d_{x}<\epsilon]\cup[d_{y}<\delta]$. Let $w\in
X$ with $d(z,w)<\eta_{z}$. By the property of real numbers $a\vee
b>c\Leftrightarrow a>c\vee b>c$ (see [8], p. 57) we get

$d(z,w)<\epsilon-d(x,z)\ \vee\ d(z,w)<\delta-d(y,z).$

In the first case we have that $d(x,w)\leq d(x,z)+d(z,w)<\epsilon$, and hence
$w\in[d_{x}<\epsilon]$, while in the second we have that $d(y,w)\leq
d(y,z)+d(z,w)<\delta$, and hence $w\in[d_{y}<\delta]$. Notice that for this
inclusion we didn’t use the infromation $z\in[d_{x}<\epsilon]$ or
$z\in[d_{y}<\delta]$. Next we show that
$[d_{x}<\epsilon]\cap[d_{y}<\delta]\subseteq[d_{z}\geq\eta_{z}]$. Let
$u\in[d_{x}<\epsilon]\cap[d_{y}<\delta]$, and we suppose that
$d(z,u)<\eta_{z}$. By the same argument $d(z,u)<\epsilon-d(x,z)$ or
$d(z,u)<\delta-d(y,z)$, which implies $d(x,u)<\epsilon$ or $d(y,u)<\delta$. In
both cases we get a contradiction, hence $d(z,u)\geq\eta_{z}$. To show that
the canonical $\bm{B}(X)$-module for $\bm{B}(x,\epsilon)\cup\bm{B}(y,\delta)$
is covering, it suffices to show the inclusion

$\bigcap_{z\in[d_{x}<\epsilon]\cup[d_{y}<\delta]}[d_{z}\geq\eta_{z}]\
\subseteq\ [d_{x}<\epsilon]\cap[d_{y}<\delta].$

Let $k\in\bigcap_{z\in[d_{x}<\epsilon]\cup[d_{y}<\delta]}[d_{z}\geq\eta_{z}]$.
We show that

$\neg{\big{[}d(x,k)<\epsilon\vee d(y,k)<\delta\big{]}}.$

If $d(x,k)<\epsilon\vee d(y,k)<\delta$, then by our hypothesis in $k$ we get
$d(k,k)\geq\eta_{k}>0$, which is a contradiction. Hence by Lemma 6.11(iv) we
get the required conjunction $d(x,k)\geq\epsilon$ and $d(y,k)\geq\delta$.
(v) Let the modulus of opennes $\mathrm{op}_{(x^{\neq_{(X,d)}},x)}\colon
x^{\neq_{(X,d)}}\to(0,+\infty)$, defined by the rule
$y\mapsto\frac{d(x,y)}{2}$. We show that if $z\in X$ with
$d(z,y)<\frac{d(x,y)}{2}$, then $d(z,x)>0$. As $0<d(x,y)\leq d(x,z)+d(y,z)$,
we get

$d(x,z)\geq d(x,y)-d(y,z)>d(x,y)-\frac{d(x,y)}{2}=\frac{d(x,y)}{2}>0.$

The corresponding covering inclusion for this copoint is

$\bigcap_{y\in