theorem Th29: :: MODELC_2:29

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