theorem Th13: :: MODELC_3:13

for H being LTL-formula holds len ({} H) = 0