defpred S_{1}[ Element of E ^omega ] means Q meets $1 -succ_of ( the InitS of SA,SA);

{ w where w is Element of E ^omega : S_{1}[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

{ w where w is Element of E ^omega : S

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