Theorem Ordinal.isNormal_preOmega

Modification history