I'm studying the proof of the famous "$5B$ covering lemma":
let $\mathcal{G}$ be a family of closed balls in $\mathbb{R}^n$ satisfying: $$ \sup\{ \text{diam}(B) : B \in \mathcal{G} \} < +\infty $$ then there exists a disjoint, at most countable subfamily $\mathcal{F} \subset \mathcal{G}$ such that $$ \bigcup_{B \in \mathcal{G}} B \subset \bigcup_{B \in \mathcal{F}} 5B $$ The proof starts defining the sequence $(\mathcal{G}_i)_i$: $$ \mathcal{G}_i := \{ B \in \mathcal{G}: \frac{S}{2^{i}} < \text{diam}(B)\le \frac{S}{2^{i-1}} \} $$ where $S=\sup\{ \text{diam}(B) : B \in \mathcal{G} \}$. Now, by means of the Haussdorf's maximal principle, we extract a disjoint subfamily $\mathcal{F}_1 \subset \mathcal{G}_1$ (if $\mathcal{G}_1$ is non empty), which is maximal w.r.t inclusion. Haussdorf's maximal principle (equivalent to the axiom of choice) states that:
Given a family of sets or a family of collection of sets $\mathcal{S}$ such that every subfamily $\mathcal{S}_0$ totally ordered w.r.t inclusion has the property $\cup \{ E : E \in \mathcal{S}_0 \} \in \mathcal{S}$, then there exists an element $S^{*} \in \mathcal{S}$ which is maximal w.r.t inclusion order.
Back to the proof, we consider:
$$ \mathcal{S}= \{ \mathcal{E} \subset \mathcal{G} : \mathcal{E} \ \text{contains disjoint balls} \} $$ it is immediate to see that $\mathcal{S}$ satisfies the hypothesis of Haussdorf's maximal principle (in fact, the totally ordered subsets of $\mathcal{S}$ are those formed by "chains" of elements) , hence there is a maximal element $\mathcal{E}^{*} \in \mathcal{S}$, which contains disjoint balls by definition. We then set $\mathcal{F}_1= \mathcal{E}^{*}$.
I've got two questions in mind: is the previous application of Haussdorf's maximal principle correct (the hypothesis seems to be trivially verified, but maybe I'm missing something)? Is the principle even necessary to extract such maximal subfamily?