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

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

proof

hence
{ s where s is Element of E ^omega : w ==>* s,S } is Subset of (E ^omega)
; :: thesis: verum
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;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