# Distance Function for Distinct Elements in Metric Space is Strictly Positive

## Theorem

Let $A$ be a set.

Let $d: A \times A \to \R$ be a real-valued function on $A$ with the following properties:

 $(\text M 1')$ $:$ $\ds \forall x, y \in A:$ $\ds \map d {x, y} = 0 \iff x = y$ $(\text M 2)$ $:$ $\ds \forall x, y, z \in A:$ $\ds \map d {x, y} + \map d {y, z} \ge \map d {x, z}$ $(\text M 3)$ $:$ $\ds \forall x, y \in A:$ $\ds \map d {x, y} = \map d {y, x}$

which can be considered as being an alternative formulation of the metric space axioms.

Then:

$\forall x, y \in A: x \ne y \implies \map d {x, y} > 0$

which is Metric Space Axiom $(\text M 4)$.

Thus $d$ is a distance function, so making $M := \struct {A, d}$ a metric space.

## Proof

 $\ds \forall x, y \in A: \,$ $\ds \map d {x, y} + \map d {y, x}$ $\ge$ $\ds \map d {x, x}$ from Metric Space Axiom $(\text M 2)$ $\ds \leadsto \ \$ $\ds 2 \map d {x, y}$ $\ge$ $\ds 0$ from Axiom $(\text M 1')$ above and Metric Space Axiom $(\text M 3)$ $\ds \leadsto \ \$ $\ds \map d {x, y}$ $\ge$ $\ds 0$

$\blacksquare$