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