theorem thirr0: :: RING_4:42

for R being domRing
for p being monic Element of the carrier of (Polynom-Ring R) st deg p = 1 holds
p is irreducible