Earlier title was : 'Equivalence between infimum's definitions'. But, that changed as failure occurred in proof as shown below.
I am sorry, if naive, but this is my experience with proving the part (ii) that lead to change in title.
My main assertion below is that cannot take an element smaller than infimum, as tinkering to prove an axiomatic definition is not possible.
Based on $\epsilon$ have a "new definition" of infimum. It is based on the fact that given a lower bound of a non-empty set $X$ over reals, can add any $\epsilon\gt 0$ to get an element of the set.
Given a nonempty set $X$, $i'$ is an infimum if $i'$ is a lower bound of a non-empty set $X\in \mathbb{R}$ and $\forall \epsilon\gt 0, X\cap [i', i'+ \epsilon)\ne \emptyset$.
The conventional definition is given by:
Let there be a nonempty set $X$ with infimum $i$, then $i$ the highest lower bound.
Let, the conventional definition be denoted by 'Def. 1', while the "new definition" by 'Def. 2'.
Need establish relation between the magnitudes of $i,i′$.
Q: Need show that the two definitions are equivalent by proving the following two conditional statements:
(i) If $i = inf(X)$, as given by Defn. 1, then $i$ is the infimum, as given by Defn. 2. Here, assume that Defn. 1 holds, and use this assumption to prove that Defn. 2 holds.
Since $i'$ is a lower bound of $X, i \ge i'$. Now, suppose that $i \gt i'$. Let $\epsilon := i-i'$. Then $X\cap [i', i' +\epsilon) \ne \emptyset \implies [i', i) \,\, \ne \emptyset$, which contradicts the assumption that $i$ is a lower bound for $X$, which should have implied $i\le i'$. So, combining the two facts get: $i'=i$
(ii) If $i' = inf(X)$, as given by Defn. 2, then $i$ is the infimum, as given by Defn. 1. Here, assume that Defn. 2 holds, and use this assumption to prove that Defn. 1 holds.
Given $i'$ is the infimum, let $i$ also be a lower bound of $X$. So, $X\cap[i, i+\epsilon) \ne \emptyset, \,\, \forall \epsilon \gt 0$. Suppose, for contradiction, there is another lower bound, let $t$, such that $t \gt i$.
Let $\epsilon:= t-i$. Then, $X\cap [i, i +\epsilon) \ne \emptyset \implies X\cap [i, t)\ne \emptyset$.
But, want a better proof in part (ii), that considers $t$ to be a still lower bound than $i$.
But then $\epsilon:= i-t$.
So, $X\cap [i, i +\epsilon) \ne \emptyset \implies [i, 2i-t)\ne \emptyset$. Hence, need $2i -t \gt i$. This implies $i \gt t $, but there is no proof by contradiction here, just a restatement.
------------ My guess is that the failure comes from attempt to prove an axiom (i.e., the infimum is the $glb$ of a non-empty set, bounded from below), & the solution is to directly use the axiom.
Also, have alternate proof that takes a simpler approach assuming the infimum property of a non-empty set, bounded from below, as an axiom, & request its vetting:
(i) By assuming Defn. 1, can state that the lower bound of Defn. 1 must match that of Defn. 2. Hence, the lower bound $i=i'$.
But, by this cannot impose any restriction on the open upper bound $i+\epsilon$ (for Defn. 1) $wrt$ $i′+\epsilon$ (for Def. 2).
(ii) By assuming Defn. 2, $X\cap [i', i'+ \epsilon)\ne \emptyset, \,\, \forall \epsilon \gt 0$. It implies that for $X \cap [i, i+ \epsilon)\ne \emptyset, \,\, \forall \epsilon \gt 0$ if $i−i'\lt \epsilon$. This condition is needed to have the higher end of the interval $[i, i+ \epsilon) \le i'+ \epsilon$. This is shown by the below proof by contradiction:
Let $i-i'=\epsilon, \epsilon \gt 0 \implies i=i'+\epsilon \implies i$ is not infimum.
But, have assumed by Defn. 1, that $i$ is infimum. So, the only possible value is $\epsilon=0$.
The whole text is just about definition of infimum and prove that an alternative definition is equivalent. The text is not about completeness of the real number.
When you ask if something is an axiom, state clearly what is the "something" that you are referring to. While there are some axioms that involve supremum, it doesn't mean anything involving supremum is an axiom. A noun can't be an axiom.
When you mention upper bound or lower bound, try to associate it with a set. Be as clear as possible.
Only use a notation after you define it, $t$ is used before it was defined.
In the proof of $(i)$, you started the proof assuming that an element $i'$ that satisfies Definition $2$ exists. Why should it exists?
Assuming that you have established the existence of $i'$. From $X \cap [i',i'+\epsilon) \neq \emptyset$, you wrote $[i',i)\ne \emptyset$, even though it is a true statement but I believe, you intend to write $X \cap [i',i) \ne \emptyset.$
Now, moving on to Definition $2$ and show that Definition $1$ is equivalent, let $i$ be a lower bound, it shouldn't have the guarantee that $X \cap [i, i+\epsilon) \ne \emptyset, \forall \epsilon >0.$ What is this $i$ that you are using?
I have no idea what you are talking about infimum property as an axiom.