Proving the equivalence of two definitions of the supremum of a set Edit #1: I apologize to everyone who took their time to read and answer my question. In my book, the second definition actually states that there exists an $x$ that is GREATER than $k-\epsilon$, rather than equal to. The definitions were indeed not equivalent because of this typo.
Edit #2: The universe is the set of real numbers. I should have been more clear about this.

First of all, let's define the upper bound of a set:
k is an upper bound of set A $\iff \text{upperBound}(k, A) \iff \forall x\in A:k\geq x$
Next, I propose two definitions of least upper bound of a set:
Definition 1:
k is THE LEAST upper bound of set A $\iff \text{leastUpperBound}(k, A) \iff \text{upperBound}(k, A) \land \forall k_2(\text{upperBound}(k_2, A)\implies k\leq k_2)$
Definition 2:
k is THE LEAST upper bound of set A $\iff \text{leastUpperBound}(k, A) \iff \text{upperBound}(k, A) \land \forall \epsilon >0 \exists x\in A:x=k-\epsilon$
I have tried and failed to use the rules of first-order logic to prove the equivalence of the two definitions. Help is much appreciated!
 A: Def 2 correctly reads as: $k$ is an upper bound of $A$ and
$$ \forall\varepsilon >0,\quad \exists x\in A,\quad x>k-\varepsilon. $$
Def 1 implies Def 2. Let $\sup  A =: s$ according to Def 1. Suppose there exists $\varepsilon_0 >0$ such that $x\leqslant s-\varepsilon_0$ for every $x\in A$. Then $s-\varepsilon_0$ is an upper bound of $A$, a contradiction.
Def 2 implies Def 1. Let $\sup A =: s$ according to Def 2. Let $t$ be an upper bound of $A$, that is, $x\leqslant t$ for every $x\in A$. Suppose $s>t$. Then by Def 2, there exists $x\in A$ such that $x>t$, a contradiction. Thus, $s\leqslant t$.
A: EDIT: This answers the original version of the OP (prior to its Edit #1).

Definition 1:
$\text{leastUpperBound}(k, A) \\\iff \text{upperBound}(k, A) \land
\forall k_2(\text{upperBound}(k_2, A)\implies k\leq k_2)$

Correct.

Definition 2:
$\text{leastUpperBound}(k, A) \\\iff \text{upperBound}(k, A) \land
\forall \epsilon{>}0 \;\exists x{\in}A\:\:x=k-\epsilon$

This definition requires $A$ to be $(-\infty,p]$ for some $p.$
Is your goal to formalise the right conjunct? If so: $$\text{leastUpperBound}(k, A) \\\iff \text{upperBound}(k, A) \quad\land\quad
\forall y\;\exists x{\in}A\:\:(y<x \lor y\geq k).$$
A: After contemplating the problem for a while, I have come up with my own proof that is based purely on first-order logic. All of the following first-order sentences are equivalent to one another, so you can either read the proof from up to down or the other way around.
The "first half" of both definitions, i.e. $\forall x \in A(x\leq k)$ is already the same, so I'll try to show the equivalence of the remaining "second halves", i.e. that $\forall k_2(\forall x\in A(x\leq k_2)\implies k_2\geq k) \iff \forall\epsilon>0\exists x\in A(x>k-\epsilon)$. $T$ will symbolize a true statement and $F$ a false statement.
Starting with the second definition, we have:
$\forall\epsilon(\epsilon>0\implies\exists x\in A(x>k-\epsilon))$
$\forall\epsilon(T\implies(\epsilon>0\implies\exists x\in A(x>k-\epsilon)))$, from the definition of implication in propositional logic
$\forall\epsilon(\exists k_2(k_2=k-\epsilon)\implies(\epsilon>0\implies\exists x\in A(x>k-\epsilon)))$, $k_2$ exists because subtraction is  closed under the set of real numbers
$\forall\epsilon\forall k_2(k_2=k-\epsilon\implies(\epsilon>0\implies\exists x\in A(x>k-\epsilon)))$
$\forall\epsilon\forall k_2(\epsilon=k-k_2\implies(\epsilon>0\implies\exists x\in A(x>k-\epsilon)))$
$\forall\epsilon\forall k_2(\epsilon=k-k_2\implies(k-k_2>0\implies\exists x\in A(x>k-(k-k_2))))$
$\forall k_2(\exists\epsilon(\epsilon=k-k_2)\implies(k>k_2\implies\exists x\in A(x>k_2)))$
$\forall k_2(T\implies(k>k_2\implies\exists x\in A(x>k_2)))$, because subtraction is closed under the set of real numbers
$\forall k_2(k>k_2\implies\exists x\in A(x>k_2))$
$\forall k_2(\forall x\in A(x\leq k_2)\implies k\leq k_2)$, by taking the contraposition of the implication
Thus, the equivalence of the definitions has been proved
