set X = { x where x is LTL-formula : ( x is atomic & x in the LTLold of N ) } ;
{ x where x is LTL-formula : ( x is atomic & x in the LTLold of N ) } 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 & x in the LTLold of N ) } or y in LTL_WFF )
assume y in { x where x is LTL-formula : ( x is atomic & x in the LTLold of N ) } ; :: thesis: y in LTL_WFF
then ex x being LTL-formula st
( y = x & x is atomic & x in the LTLold of N ) ;
hence y in LTL_WFF by MODELC_2:1; :: thesis: verum

end;

hence { x where x is LTL-formula : ( x is atomic & x in the LTLold of N ) } is Subset of LTL_WFF ; :: thesis: verum