let a be set ; :: thesis: for H being LTL-formula st a is Subset of (Subformulae H) holds
a is Subset of LTL_WFF
let H be LTL-formula; :: thesis: ( a is Subset of (Subformulae H) implies a is Subset of LTL_WFF )
assume A1: a is Subset of (Subformulae H) ; :: thesis: a is Subset of LTL_WFF
for x being object st x in a holds
x in LTL_WFF

proof

let x be object ; :: thesis: ( x in a implies x in LTL_WFF )
assume x in a ; :: thesis: x in LTL_WFF
then ex F being LTL-formula st
( F = x & F is_subformula_of H ) by A1, Def24;
hence x in LTL_WFF by Th1; :: thesis: verum

end;

hence a is Subset of LTL_WFF by TARSKI:def 3; :: thesis: verum