for H being LTL-formula ex L being FinSequence st Subformulae H = rng L