Theorem Ordinal.sub_isLimit

Modification history