Theorem Ordinal.nfp_eq_nfpFamily

Modification history