I have seen multiple papers cite [VW86] in saying that, for every LTL property $\phi$ and automaton $P$, if $P$ has a run $r$ violating $\phi$, then $P$ also has a run $r' = \alpha \beta^{\omega}$ violating $\phi$, where $r'$ is called a lasso and consists of a finite prefix $\alpha$ followed by infinite repetition of a loop $\beta$. However, I do not see this result anywhere in the cited paper. (Possibly it is alluded to in discussions of Büchi acceptance conditions?)
Every LTL property is the intersection of an LTL liveness property and an LTL safety property [MMD14]. If $P$ violates the safety property then the proof is straightforward: find the bad prefix $\alpha$, and then prove there must exist a run beginning with $\alpha$ and then looping forever after some time, arguing according to the finitude of the structure (assuming we only allow finite-state machines).
But what if the property is a liveness property? Although I intuitively understand why an LTL property cannot only be violated by a non-lasso run like $a b a a b a a a b a a a a b a a a a a b ...$, I do not mathematically understand why this is the case.
The language of infinite words defined by a LTL property is $\omega$-regular. The complement of a $\omega$-regular language is also $\omega$-regular. Thus the set of $\omega$-words violating a LTL-formula is $\omega$-regular. Finally, every nonempty $\omega$-regular language contains an ultimately periodic word, that is, a word of the form $uv^\omega$ for some finite words $u$ and $v$.