set X = { x where x is LTL-formula : ex u being LTL-formula st
( u in W & x = 'X' u ) } ;
{ x where x is LTL-formula : ex u being LTL-formula st
( u in W & x = 'X' u ) } c= LTL_WFF

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is LTL-formula : ex u being LTL-formula st
( u in W & x = 'X' u ) } or y in LTL_WFF )
assume y in { x where x is LTL-formula : ex u being LTL-formula st
( u in W & x = 'X' u ) } ; :: thesis: y in LTL_WFF
then consider x being LTL-formula such that
A1: y = x and
ex u being LTL-formula st
( u in W & x = 'X' u ) ;
thus y in LTL_WFF by A1, Th1; :: thesis: verum

end;

hence { x where x is LTL-formula : ex u being LTL-formula st
( u in W & x = 'X' u ) } is Subset of LTL_WFF ; :: thesis: verum