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