defpred S₁[ Element of E ^omega ] means Q meets $1 -succ_of the InitS of SA,SA;
{ w where w is Element of E ^omega : S₁[w] } c= E ^omega from FRAENKEL:sch 10();
hence { w where w is Element of E ^omega : Q meets w -succ_of the InitS of SA,SA } is Subset of (E ^omega ) ; :: thesis: verum