assume not subdivision P,KX is finite-degree ; :: thesis: contradiction
then ( (degree KX) + 1 in REAL & degree (subdivision P,KX) = +infty ) by Def12, XREAL_0:def 1;
hence contradiction by Th51, XXREAL_0:9; :: thesis: verum