let a be set ; :: thesis: ( a is LTL-formula iff a in LTL_WFF )
thus ( a is LTL-formula implies a in LTL_WFF ) :: thesis: ( a in LTL_WFF implies a is LTL-formula )

proof

assume a is LTL-formula ; :: thesis: a in LTL_WFF
then a is Element of LTL_WFF by Def10;
hence a in LTL_WFF ; :: thesis: verum

end;

assume a in LTL_WFF ; :: thesis: a is LTL-formula
hence a is LTL-formula by Def9, Def10; :: thesis: verum