now :: thesis: for p being irreducible Element of (Polynom-Ring R) holds p in IRR (Polynom-Ring R)

let p be irreducible Element of (Polynom-Ring R); :: thesis: p in IRR (Polynom-Ring R)
p in { x where x is Element of (Polynom-Ring R) : x is irreducible } ;
hence p in IRR (Polynom-Ring R) by RING_2:def 10; :: thesis: verum

end;

hence not IRR (Polynom-Ring R) is empty ; :: thesis: verum