"Any finite poset has a maximal element." How to formalize the proof that is given?

The given proof glosses over some details, but it's basically complete.

You could use induction on the cardinality of $X$. If $|X|=1$ there's nothing to prove. So let's assume $|X|=n>1$ and that the result holds for posets having cardinality less than $n$.

Pick an element of $X$, call it $a$; if $a$ is maximal, then we're done. Otherwise there's at least an element $b$ such that $a<b$. Consider $Y=\{x\in X: a<x\}$. Then $Y$, with the induced order relation, is a finite poset and $a\notin Y$, so that $|Y|<|X|$. By the induction hypothesis, $Y$ has a maximal element $c$. Let's show that $c$ is also maximal in $X$. If $d\in X$ and $c<d$, then we have $a<c<d$, so $a<d$ and hence $d\in Y$, contradicting the fact that $c$ is maximal in $Y$.