let F, H be LTL-formula; :: thesis: ( F is_subformula_of H implies {F} is Subset of (Subformulae H) )
set E = Subformulae H;
assume F is_subformula_of H ; :: thesis: {F} is Subset of (Subformulae H)
then F in Subformulae H by MODELC_2:45;
hence {F} is Subset of (Subformulae H) by SUBSET_1:41; :: thesis: verum