Theorem Ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub

Modification history