now :: thesis: ex p being Element of the carrier of (Polynom-Ring F) st
( p is irreducible & not p is linear )

assume A: for p being Element of the carrier of (Polynom-Ring F) st p is irreducible holds
p is linear ; :: thesis: contradiction
for p being monic Element of the carrier of (Polynom-Ring F) holds
( p is irreducible iff deg p = 1 )

proof

let p be monic Element of the carrier of (Polynom-Ring F); :: thesis: ( p is irreducible iff deg p = 1 )

now :: thesis: ( p is irreducible implies deg p = 1 )

assume p is irreducible ; :: thesis: deg p = 1
then p is linear by A;
hence deg p = 1 by FIELD_5:def 1; :: thesis: verum

end;

hence ( p is irreducible iff deg p = 1 ) by RING_4:44; :: thesis: verum

end;

hence contradiction by RING_4:46; :: thesis: verum

end;

hence ex b₁ being Element of the carrier of (Polynom-Ring F) st
( b₁ is irreducible & not b₁ is linear ) ; :: thesis: verum