theorem Th3: :: MODELC_2:3

for H being LTL-formula holds 1 <= len H