Theorem Ordinal.not_bddAbove_setOfPred_isPrincipal

Modification history