As you note, $1\rightarrow \bar 2$ is straightforward:
$$
\begin{align}
Ax &= b \\
x'A' &= b' \\
x'A'y &= b'y \\
\end{align}
$$
Since $x\geq0$, it is impossible to simultaneously have $A'y\geq 0$ and $b'y < 0$.
For $\bar 1\rightarrow 2$, first note that $Ax = b, x\geq 0$ (the system that is infeasible due to $\bar 1$) is equivalent to $Dx \leq d$, where we define
$$
D = \left( \begin{array}{c}
A \\ -A \\ -I \end{array} \right), d = \left( \begin{array}{c}
b \\ -b \\ 0 \end{array} \right).
$$
We can now apply Fourier-Motzkin Elimination (FME) on the system $Dx\leq d$, removing all variables $1, 2, \ldots, n$ in order. Define $U^i$ to be the matrix used to remove variable $i$ from the system of equations; I will use $U^i\geq 0$ to indicate that each entry in $U^i$ is non-negative. From FME we have $U^nU^{n-1}\ldots U^1D = 0$. Defining $U = U^nU^{n-1}\ldots U^1$ we have $UD = 0$; note that from $U^1\geq 0, U^2\geq 0, \ldots, U^n\geq 0$ we also have $U\geq 0$.
Because $Dx\leq d$ is infeasible, there must be some row $u'\geq 0$ of $U$ such that $u'D = 0'$ and $u'd < 0$. Letting $p\geq 0$ be the first $m$ elements of $u$, $q\geq 0$ be the next $m$ elements of $u$, and $r\geq 0$ be the last $n$ elements of $u$, we have:
$$
\begin{align}
u'D &= 0' \\
\left( \begin{array}{ccc}
p' & q' & r' \end{array} \right) \left( \begin{array}{c}
A \\ -A \\ -I \end{array} \right) &= 0' \\
(p-q)'A &= r' \\
(p-q)'A &\geq 0' \\
A'(p-q) &\geq 0
\end{align}
$$
and
$$
\begin{align}
u'd &< 0 \\
\left( \begin{array}{ccc}
p' & q' & r' \end{array} \right) \left( \begin{array}{c}
b \\ -b \\ 0 \end{array} \right) &< 0 \\
(p-q)'b &< 0 \\
b'(p-q) &< 0
\end{align}
$$
By setting $y = p-q$, we have used FME to construct a vector $y\in\mathbb{R}^m$ such that $A'y \geq 0$ and $b'y < 0$.
Best Answer
Farkas' Lemma comes in different variants. I prefer the following variant.
The system (1) $A\mathbf x \leq \mathbf b$ has no solution if and only if (2) there exists some $\mathbf u \geq \mathbf 0$ with $\mathbf u^TA = \mathbf 0^T$ and $\mathbf b^T\mathbf u < 0$.
But what does this lemma say? It says that (1) has no solution if and only if it implies the inequality $0 < 0$.
Explanation: The vector $\mathbf u$ consists of non-negative coefficients and (3) $\mathbf u^TA\mathbf x \leq \mathbf u^T\mathbf b$ is a non-negative combination of the inequalities of (1). Moreover (3) is implied by (1) as any solution of (1) is also a solution of (3). In (2) we additionally stipulate that $\mathbf u^TA = \mathbf 0$ and $\mathbf u^T\mathbf b < 0$. Hence, we have $\mathbf 0^T\mathbf x < 0$. Moreover, since $\mathbf 0^T\mathbf x = 0$, we have shown that (1) implies the inequality $0 < 0$.
--- Addition
In practice, one uses the following linear program to check for the solvability of $A \mathbf x \leq \mathbf b$: $$\text{maximize } \mathbf 0^T\mathbf x \text{ s.t. } A\mathbf x \leq \mathbf b.$$ By duality this linear program is infeasible if and only if the dual program $$\text{minimize } \mathbf b^T\mathbf u \text{ s.t. } A^T\mathbf u = \mathbf 0 \text{ and } \mathbf u \geq \mathbf 0$$ is unbounded. But the later is equivalent to Farkas' Lemma as a simple exercise shows.