deg <%x%> <= 1 - 1 by XREAL_1:9, ALGSEQ_1:def 5;
hence deg <%x%> <= 0 ; :: according to RATFUNC1:def 2 :: thesis: verum