defpred S₁[ Element of E ^omega ] means $1 -succ_of Q,A meets the FinalS of A;
{ 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 : w -succ_of Q,A meets the FinalS of A } is Subset of (E ^omega ) ; :: thesis: verum