theorem :: MODELC_2:39

for F, H being LTL-formula st F is_proper_subformula_of 'not' H holds
F is_subformula_of H