Invariant that the last committed anchor has at least a certain number of successors: proof that it holds in every reachable state.
This completes last-anchor-voters-def-and-init-and-next by showing that the invariant holds in every reachable state.
