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