set X = { x where x is LTL-formula : x is atomic } ;
{ x where x is LTL-formula : x is atomic } c= LTL_WFF

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is LTL-formula : x is atomic } or y in LTL_WFF )
assume y in { x where x is LTL-formula : x is atomic } ; :: thesis: y in LTL_WFF
then ex x being LTL-formula st
( y = x & x is atomic ) ;
hence y in LTL_WFF by Th1; :: thesis: verum

end;

hence { x where x is LTL-formula : x is atomic } is Subset of LTL_WFF ; :: thesis: verum