set K = Polynom-Ring R;
reconsider x = rpoly (1,(0. R)) as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
deg (rpoly (1,(0. R))) = 1 by HURWITZ:27;
then x is irreducible by thirr0;
hence ex b₁ being Element of the carrier of (Polynom-Ring R) st b₁ is irreducible ; :: thesis: verum