let F, G, H be LTL-formula; :: thesis: ( not F is_proper_subformula_of G 'R' H or F is_subformula_of G or F is_subformula_of H )
assume A1: F is_proper_subformula_of G 'R' H ; :: thesis: ( F is_subformula_of G or F is_subformula_of H )
set G1 = G 'R' H;
A2: G 'R' H is Release by Def17;
then A3: not G 'R' H is Until by Lm21;
( not G 'R' H is conjunctive & not G 'R' H is disjunctive ) by A2, Lm21;
then ( the_left_argument_of (G 'R' H) = G & the_right_argument_of (G 'R' H) = H ) by A2, A3, Def19, Def20;
hence ( F is_subformula_of G or F is_subformula_of H ) by A1, A2, Th38; :: thesis: verum