theorem thirr: :: RING_4:44

for F being Field
for p being Element of the carrier of (Polynom-Ring F) st deg p = 1 holds
p is irreducible