set Y = { s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } ;
{ s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } c= the carrier of TS

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } or y in the carrier of TS )
assume y in { s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } ; :: thesis: y in the carrier of TS
then ex s being Element of TS st
( s = y & ex t being Element of TS st
( t in X & t,x ==>* s,TS ) ) ;
hence y in the carrier of TS ; :: thesis: verum

end;

hence { s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } is Subset of TS ; :: thesis: verum