A finite lattice has a bottom and a top, and every element is the join of the join-irreducible elements below it

Since $L$ is nonempty and finite, [L1] lets us choose $m$ for which the principal ideal $\downarrow m$ has least cardinality. If $y<m$, then $\downarrow y$ is a proper subset of $\downarrow m$ and [L1] makes its cardinality strictly smaller, contradicting that choice, so $m$ is minimal. If $m^{\mathrm{\prime }}$ is another minimal element, then $m\wedge m^{\mathrm{\prime }}\le m,m^{\mathrm{\prime }}$, so minimality gives $m\wedge m^{\mathrm{\prime }}=m=m^{\mathrm{\prime }}$. Thus the minimal element is unique and lies below every $x\in L$, because $m\wedge x\le m$ forces $m\wedge x=m$. Call it $0_L$.

Dually, choosing an element whose principal filter has least cardinality gives a unique maximal element $1_L$, and every $x\in L$ lies below it.

We prove the decomposition of $x$ by induction on the cardinality of its principal ideal $\downarrow x=\{y:y\le x\}$. For $x=0_L$, the empty join is $0_L$.

Assume every element with a smaller principal ideal is the join of the join-irreducibles below it.

If $x\mathrm{\ne }{0}_L$ is join-irreducible, then $x$ itself is the required one-term join.

If $x\mathrm{\ne }{0}_L$ is not join-irreducible, there are $a,b<x$ with $x=a\vee b$. The principal ideals of $a$ and $b$ are proper subsets of $\downarrow x$, so [L1] gives each strictly smaller cardinality and the induction hypothesis writes each as a join of join-irreducibles below it. Joining those two finite families writes $x=a\vee b$ as a join of join-irreducibles below $x$.

In every case, steps 2.1, 4.1 and 4.2 give a finite subfamily ${\mathcal{D}}_x$ of the join-irreducibles below $x$ whose join is $x$. Let ${\mathcal{J}}_x$ be the set of all join-irreducibles below $x$. Since every member of ${\mathcal{J}}_x$ is at most $x$, its finite join is at most $x$; since ${\mathcal{D}}_x\subseteq {\mathcal{J}}_x$, that join is also at least $\bigvee {\mathcal{D}}_x=x$. Hence $x$ is the join of all members of ${\mathcal{J}}_x$.

Step 5.1 proves the decomposition for every $x\in L$, while steps 1.1 and 1.2 provide the bottom and top.