Theorem Finset.nonempty_of_ne_empty

Modification history