Theorem: G-Tower is Well-Ordered under Subset Relation

Let $M$ be a class.
Let $g: M \to M$ be a progressing mapping on $M$.
Let $M$ be a $g$-tower.
Then $M$ is well-ordered under the subset relation such that:
{{begin-axiom}}
{{axiom | n = 1
        | lc= Smallest Element:
        | t = $\O$ is the smallest element of $M$
}}
{{axiom | n = 2
        | lc= Immediate Successor:
        | t = the immediate successor of $x$ (if there is one) is $\map g x$
}}
{{axiom | n = 3
        | lc= Limit Element:
        | t = every limit element is the union of its set of predecessors.
}}
{{end-axiom}}

Proof:
Let $M$ be a $g$-tower.
By $g$-Tower is Nest, $M$ is a nest.
Hence {{afortiori}} $\subseteq$ is a total ordering on $M$.
It remains to be shown that $\subseteq$ is a well-ordering, by showing the following:
Let $A \subseteq M$ be an arbitrary non-empty subclass of $M$.
Let $L$ be the set of all elements $x$ which are proper subsets of ''all'' elements of $A$:
:$L = \set {x \in M: \forall z \in A: x \subsetneqq z}$
Since $L \subseteq \powerset z$ for all $z \in A$, it follows by Subclass of Set is Set that $L$ is in fact a set.
It is to be shown that the following conditions hold:
:$(1): \quad$ If $L$ is empty, then $\O$ is the smallest element of $A$.
:$(2): \quad$ If $L$ is non-empty and contains a greatest element $x$, then $\map g x$ is the smallest element of $A$.
:$(3): \quad$ If $L$ is non-empty and contains no greatest element, then its union $\bigcup L$ is the smallest element of $A$.
;Case $(1)$ -- $L$ is empty
As $L$ is empty:
:$\O \notin L$
Hence $\O$ is not a proper subset of every element of $A$.
However, $\O$ ''is'' a subset (although not necessarily proper) of every element of $A$.
Hence $\O$ must be one of the elements of $A$.
Hence $\O$ is by definition the smallest element of $A$.
{{qed|lemma}}
;Case $(2)$ -- $L$ is non-empty and contains a greatest element $x$
Let $L$ be non-empty and contain a greatest element $x$.
We have that:
:from $g$-Tower is Closed under Mapping that $M$ is closed under $g$
:{{apriori}} $g$ is a progressing mapping on $M$.
From $g$-Tower is Nest: Lemma 2 we have:
:$\forall x, y \in M: \map g x \subseteq y \lor y \subseteq x$
From Fixed Point of $g$-Tower is Greatest Element:
:if $x = \map g x$, then $x$ is the greatest element (under the subset relation) of $M$.
Hence the conditions are fulfilled for Closed Class under Progressing Mapping Lemma be applied, which gives us that:
:if:
::$x$ is a proper subset of all elements of $A$ and the greatest element of $A$ with that property,
:then:
::$\map g x \in A$ and is the smallest element of $A$.
This is statement $(2)$.
{{qed|lemma}}
;Case $(3)$ -- $L$ is non-empty and contains no greatest element
Suppose $\bigcup L$ were an element of $L$.
Then $\bigcup L$ would be the greatest element of $L$.
But $L$ contains no greatest element.
Hence $\bigcup L$ is not an element of $L$.
From Restriction of Total Ordering is Total Ordering, $\subseteq$ is a total ordering on $L$.
This makes $L$ a nest.
As $L$ is a set, $L$ is {{afortiori}} a chain.
By $g$-Tower is Closed under Chain Unions:
:$\bigcup L \in M$
Let $y \in A$.
We have by definition of $L$ that each element of $L$ is a subset of $y$.
Hence:
:$\forall y \in A: \bigcup L \subseteq y$
But {{apriori}}:
:$\bigcup L \notin L$
Hence there exists at least one $z \in A$ such that $\bigcup L$ is not a ''proper'' subset of $z$.
Hence for such a $z$ it must be that:
:$\bigcup L = z$
That is:
:$\bigcup L \in A$
and because:
:$\forall y \in A: \bigcup L \subseteq y$
it follows by definition that $\bigcup L$ is the smallest element of $A$.
{{qed|lemma}}
Thus it has been shown that every non-empty subclass of $M$ has a smallest element.
Hence by definition $M$ is well-ordered under the subset relation.
{{qed}}