Let $P$ be a D1687: Inclusion-ordered collection of sets such that

(i) | $\max(P)$ is the D4464: Set of maximal elements in $P$ |

Then
\begin{equation}
|\max(P)| \geq 1
\end{equation}

Result R1406
on D1687: Inclusion-ordered collection of sets

Collection of sets ordered by inclusion contains a maximal element

Formulation 0

Let $P$ be a D1687: Inclusion-ordered collection of sets such that

(i) | $\max(P)$ is the D4464: Set of maximal elements in $P$ |

Then
\begin{equation}
|\max(P)| \geq 1
\end{equation}

Subresults

▶ | R4291: Vector space always has an inclusion-maximal linearly independent set |

Proofs

Let $P$ be a D1687: Inclusion-ordered collection of sets such that

(i) | $\max(P)$ is the D4464: Set of maximal elements in $P$ |

If $C \subseteq P$ is a D848: Chain in $X$, then result R4142: Union is an upper bound to each set in the union shows that the D77: Set union $\cup C$ is an upper bound for $C$ in $P$. Hence, the claim is a consequence of R447: Zorn's lemma. $\square$