Theorem Cardinal.mk_le_mk_of_subset

Modification history