let F, H be LTL-formula; :: thesis: ( F is_proper_subformula_of 'X' H implies F is_subformula_of H )
assume A1: F is_proper_subformula_of 'X' H ; :: thesis: F is_subformula_of H
A2: 'X' H is next by Def18;
then not 'X' H is negative by Lm17;
then the_argument_of ('X' H) = H by A2, Def21;
hence F is_subformula_of H by A1, A2, Th123; :: thesis: verum