set X = { s where s is Element of E ^omega : w ==>* s,S } ;
{ s where s is Element of E ^omega : w ==>* s,S } c= E ^omega

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Element of E ^omega : w ==>* s,S } or x in E ^omega )
assume x in { s where s is Element of E ^omega : w ==>* s,S } ; :: thesis: x in E ^omega
then ex t being Element of E ^omega st
( t = x & w ==>* t,S ) ;
hence x in E ^omega ; :: thesis: verum

end;

hence { s where s is Element of E ^omega : w ==>* s,S } is Subset of (E ^omega) ; :: thesis: verum