\renewcommand{\arraystretch}{1.5}
\begin{array}{rl}
a_0=\inf\emptyset&\leftrightarrow(\forall a)(a\in\emptyset\Rightarrow a_0\leq a)\wedge (\forall a_0')\Big((\forall a)(a\in\emptyset\Rightarrow a_0'\leq a)\Rightarrow a_0'\leq a_0\Big)\leftrightarrow(\forall a)(\bot\Rightarrow a_0\leq a)\wedge (\forall a_0')\Big((\forall a)(\bot\Rightarrow a_0'\leq a)\Rightarrow a_0'\leq a_0\Big)\\
&\leftrightarrow\top\wedge (\forall a_0')(\top\Rightarrow a_0'\leq a_0)\leftrightarrow(\forall a_0')(a_0'\leq a_0)\leftrightarrow a_0=\infty\end{array}