defpred S_{1}[ Element of E ^omega ] means ex p, q being Element of A st

( p in the InitS of A & q in the FinalS of A & p,$1 ==>* q,A );

{ w where w is Element of E ^omega : S_{1}[w] } c= E ^omega
from FRAENKEL:sch 10();

hence { u where u is Element of E ^omega : ex p, q being Element of A st

( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) } is Subset of (E ^omega) ; :: thesis: verum

( p in the InitS of A & q in the FinalS of A & p,$1 ==>* q,A );

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

hence { u where u is Element of E ^omega : ex p, q being Element of A st

( p in the InitS of A & q in the FinalS of A & p,u ==>* q,A ) } is Subset of (E ^omega) ; :: thesis: verum