let F, G, H be LTL-formula; :: thesis: ( not F is_proper_subformula_of G 'or' H or F is_subformula_of G or F is_subformula_of H )
assume A1: F is_proper_subformula_of G 'or' H ; :: thesis: ( F is_subformula_of G or F is_subformula_of H )
A2: G 'or' H is disjunctive ;
then ( the_left_argument_of (G 'or' H) = G & the_right_argument_of (G 'or' H) = H ) by Def19, Def20;
hence ( F is_subformula_of G or F is_subformula_of H ) by A1, A2, Th38; :: thesis: verum