A Büchi automaton accepts an infinite word iff there is an accepting state reachable from the initial state that belongs to a directed cycle. This reduces infinite-word emptiness to finite cycle detection, witnessed by an ultimately periodic lasso word u v^omega.