Counterexample. Guarantee properties are not closed under infinite intersection [ltp-000H]

Consider the family of properties P_{i \in \mathbb {N}} = \{ \sigma \in \Sigma ^\omega \mid \sigma _i \neq \texttt {a}\}, i.e. the property where the ith state is not \texttt {a}. Each P_i is a guarantee property, as all satisfying behaviours are extensions of good prefixes ending in a non-\mathtt {a} state of length i. Their intersection \bigcap _{i \in \mathbb {N}} P_i, however, is not a guarantee property, as any finite prefix can be extended to a bad prefix by appending an \texttt {a}-state, and therefore cannot be a good prefix.