Every finite non-solvable group has a minimal simple group as subquotient

Statement

Suppose $G$ is a finite group that is not solvable. Then, there exists a Minimal simple group (?) arising as a subquotient of $G$.

Facts used

1. Subquotient is transitive: A subquotient of a subquotient is a subquotient.

Proof

Given: A finite non-solvable group $G$.

To prove: There exists a minimal simple group arising as a subquotient of $G$.

Proof: We prove this by induction on the order of $G$. We assume that the result has been proved for all groups of order strictly less than the order of $G$. We make three cases:

1. $G$ is itself a minimal simple group -- it is simple non-Abelian and every proper subgroup is solvable: In this case, $G$ is itself the desired subquotient.
2. $G$ is not simple: Since $G$ is not solvable by assumption, $G$ must have a composition factor that is a simple non-Abelian group. Since any composition factor is a subquotient, $G$ has a subquotient of smaller size that is also not solvable. By induction, this subquotient has a minimal simple group as subquotient, so by fact (1), $G$ has a minimal simple subquotient.
3. $G$ is simple but not minimal simple: Since $G$ is not solvable, $G$ must be a simple non-Abelian group. Since it is not minimal simple by assumption, there is some subgroup of $G$ that is not solvable. By the inductive assumption, this subgroup has a minimal simple subquotient, so by fact (1), $G$ has a minimal simple subquotient.