Proof that sup S ≤ inf T by predicate logic Let S and T be subsets of $\mathbb R$ such that s < t for each s ∈ S and each t ∈ T. Prove
carefully that sup S ≤ inf T.
Now I understand how to prove this as a natural language proof like,
a = sup S, b = inf T
For all t in T, t is an upper bound of S.
Hence, a being the least of the upper bounds, a ≤ t, for all t in T.
But then a is a lower bound of T.
Hence, b being the greatest of the lower bounds, b ≥ a.
Thus, sup S ≤ inf T
But I am struggling to write this as a step by step predicate logic proof while justifying each step. 
Can someone please help?
 A: We know that sup and inf exist and are unique for bounded-from-the-right-side subsets of $\mathbb{R}$, let's call this property $\star$, so it's ok to name them (sup and inf) like you did (a and b), but let's just prove that $S$ and $T$ really are bounded above and below, respectively. We do need an additional assumption: that these subsets are not empty. Our domain is $\mathbb{R}$


*

*$\forall s(s \in S \rightarrow \forall t(t \in T \rightarrow s < t))$ (assume) 

*$\exists x(x \in S) \land \exists x(x \in T)$ (assume)

*$\exists x(x \in S)$ (from 2)

*$s_0 \in S$ (special as.)

*$s_0 \in S \rightarrow \forall t(t \in T \rightarrow s_0 < t)$ (from 1)

*$\forall t(t \in T \rightarrow s_0 < t)$ (from 4, 5)

*$\exists x \forall t(t \in T \rightarrow x < t)$ (existential elimination of 3, by 4-6)
Similarly for $S$. The first two steps in the proof below are by 7th steps in the proof above and its $S$-version, by $\star$.


*

*$\forall s (s \in S \rightarrow s \leq a) 
\land 
\forall a' (a' < a \rightarrow \neg \forall s (s \in S \rightarrow s \leq a'))$

*$\forall t (t \in T \rightarrow b \leq t) 
\land 
\forall b' (b < b' \rightarrow \neg \forall t (t \in T \rightarrow b' \leq t))$

*$\forall s(s \in S \rightarrow \forall t(t \in T \rightarrow s < t))$ (assume)

*b < a (assume for reductio ad absurdum)

*$\forall a' (a' < a \rightarrow \neg \forall s (s \in S \rightarrow s \leq a'))$ (from 1)

*$b < a \rightarrow \neg \forall s (s \in S \rightarrow s \leq b)$ (from 5)

*$\neg \forall s (s \in S \rightarrow s \leq b)$ (from 4, 6)

*$\exists s(s \in S \land b \lt s)$ (from 7)

*$s_0 \in S \land b \lt s_0$ (special as.)

*$\forall b' (b < b' \rightarrow \neg \forall t (t \in T \rightarrow b' \leq t))$ (from 2)

*$b < s_0 \rightarrow \neg \forall t (t \in T \rightarrow s_0 \leq t)$ (from 10)

*$b \lt s_0$ (from 9)

*$\neg \forall t (t \in T \rightarrow s_0 \leq t)$ (from 11, 12)

*$\exists t (t \in T \land t \lt s_0)$ (from 13)

*$s_0 \in S$ (from 9)

*$s_0 \in S \land \exists t (t \in T \land t \lt s_0)$ (from 14, 15)

*$\exists s (s \in S \land \exists t (t \in T \land t \lt s))$ (existential elimination of 8 by 9-16)

*$\neg (b < a)$ (3, 17 contradiction)
A: As a really really late answer, here is an alternative way of writing down this proof, which certainly is "a step by step predicate logic proof while justifying each step".$
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}}
\newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} }
\newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{\Ref}[1]{\text{(#1)}}
\newcommand{\then}{\Rightarrow}
\newcommand{\when}{\Leftarrow}
\newcommand{\true}{\text{true}}
\newcommand{\false}{\text{false}}
$
As a commenter said, let's start by making the definitions explicit.  The simplest definitions for $\;\sup\;$ and $\;\inf\;$ I know are that
\begin{align}
\tag{0}
\sup S \le z &\;\equiv\; \langle \forall s : s \in S : s \le z \rangle \\
\tag{1}
z \le \inf T &\;\equiv\; \langle \forall t : t \in T : z \le t \rangle \\
\end{align}
for every $\;z\;$, for any non-empty upper-bounded $\;S\;$ and non-empty lower-bounded $\;T\;$.
Now we can start to calculate, starting from the statement we need to prove, working to expand the definitions, and seeing where this leads us:
$$\calc
    \sup S \le \inf T
\op\equiv\hints{ordering -- the simplest way I see to allow}\hint{using the above definitions}
    \langle \forall z : z \le \sup S : z \le \inf T \rangle
\op\equiv\hint{definition $\Ref{1}$ of $\;\inf\;$ -- the only definition which applies}
    \langle \forall z : z \le \sup S : \langle \forall t : t \in T : z \le t \rangle \rangle
\op\equiv\hints{exchange quantifications -- to bring the $\;z\;$'s back}\hint{together}
    \langle \forall t : t \in T : \langle \forall z :: z \le \sup S : z \le t \rangle \rangle
\op\equiv\hint{ordering -- simplify again}
    \langle \forall t : t \in T : \sup S \le t \rangle
\op\equiv\hint{definition $\Ref{0}$ of $\;\sup\;$}
    \langle \forall t : t \in T : \langle \forall s : s \in S : s \le t \rangle \rangle
\op\when\hint{weaken using $\;\lt \;\then\; \le\;$ -- to achieve the desired goal}
    \langle \forall t : t \in T : \langle \forall s : s \in S : s \lt t \rangle \rangle
\endcalc$$
This completes the proof.
