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