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