Theorem Ordinal.principal_add_omega0

Modification history