degree K = ((degree K) + 1) - 1 by XXREAL_3:24;
hence degree K is integer ; :: thesis: verum