I have a question on the definition of Saturated Sets, as particular subset of the set of strongly normalizing terms in lambda calculus.

Here is the definition: a set $S$ of strongly normalizing $\lambda$-terms is said saturated if:

1. For all $x : var$ and for all sequences $a_{1} \dots a_{n}$ of strongly normalizing terms we have $x\, a_{1} \dots a_{n} \in S$.

2. For all strongly normalizing term strongly normalizing $a$ we have that $c[x:=a] \, a_{1} \dots a_{n} \in S$ implies $(\lambda x . c)\, a \, a_{1} \dots a_{n} \in S$.

Now, I'd like to know why this definition is the way it is. I understand that originally the definition came from Girard, in a paper on "Candidats De Reductibilité". Can anyone give me a general insight of the reason of this particular definition?