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 object ; :: 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 ex x being LTL-formula st
( y = x & ex u being LTL-formula st
( u in W & x = 'X' u ) ) ;
hence y in LTL_WFF by 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