Theorem Set.Finite.eq_of_subset_of_card_le

Modification history