Least fix point of CTL formula

Question

In the book Logic in Computer Science on page 244, there is a proof that $[[E(\phi U\psi)]]$ is the least fixed point of $G(X)=[[\psi]] \cup ([[\phi]]\cap\mathop{\textrm{pre}}_\exists(X))$. I don't get the idea of point 2. I tried to understand why this proof says that $[[E(\phi U\psi)]]$ is the least fixed point of $G$.

They prove that $G^{k+1}(\emptyset)\subseteq[[E(\phi U\psi)]]$ for each $k\geq0$.
This is fine, I understand each step on their the proof, I just don't understand why this proves that $[[E(\phi U\psi)]]$ is the least fixed point of $G$...

I can prove that $G^{k+1}(\emptyset)\subseteq S$ when $S$ is the group of all the states. $G$ is still the same function, and of course that for each such $i\geq0, G^i(\emptyset)\subseteq S$. This doesn't mean that $S$ is the least fixed point, or that each fixed point contains $S$.

So why this proof claims that $[[E(\phi U\psi)]]$ is the least fixed point of $G$?