theorem Th28: :: MODELC_2:28

for F, H being LTL-formula st H is_immediate_constituent_of F holds
len H < len F