Added invariant.

The new invariant guarantees that, if there's a Selection, there's at least a FIFO.