Theorem Set.encard_tsub_one_le_encard_sdiff_singleton

Modification history