Theorem Set.exists_ne_of_one_lt_encard

Modification history