set E = Subformulae F;
Subformulae F is Subset of (Subformulae F) by SUBSET:3;
hence Subformulae F is Subset of LTL_WFF by MODELC_2:47; :: thesis: verum