theorem :: MODELC_2:33

for F, H being LTL-formula st H is_proper_subformula_of F holds
ex G being LTL-formula st G is_immediate_constituent_of F