defpred S₁[ 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₁[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