Theorem SuccOrder.prelimitRecOn_succ_of_not_isMax

Modification history