let H be LTL-formula; :: thesis: ( ( H is negative or H is next ) implies the_argument_of H is_subformula_of H )
set G = the_argument_of H;
assume ( H is negative or H is next ) ; :: thesis: the_argument_of H is_subformula_of H
then the_argument_of H is_immediate_constituent_of H by MODELC_2:20, MODELC_2:21;
then the_argument_of H is_proper_subformula_of H by MODELC_2:29;
hence the_argument_of H is_subformula_of H ; :: thesis: verum