let R be domRing; :: thesis: for p being Element of the carrier of (Polynom-Ring R) st ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p ) holds
p is reducible
let p be Element of the carrier of (Polynom-Ring R); :: thesis: ( ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p ) implies p is reducible )
set K = Polynom-Ring R;
reconsider pp = p as Polynomial of R ;
assume ex q being Element of the carrier of (Polynom-Ring R) st
( q divides p & 1 <= deg q & deg q < deg p ) ; :: thesis: p is reducible
then consider q being Element of the carrier of (Polynom-Ring R) such that
A0: ( q divides p & 1 <= deg q & deg q < deg p ) ;
A1: q is not Unit of (Polynom-Ring R) by T88, A0;

now :: thesis: not q is_associated_to p

assume q is_associated_to p ; :: thesis: contradiction
then consider r being Element of (Polynom-Ring R) such that
A2: ( r is unital & q * r = p ) by GCD_1:18;
reconsider rr = r as Element of the carrier of (Polynom-Ring R) ;
A5: p = q *' rr by A2, POLYNOM3:def 10;
then A4: r <> 0_. R by HURWITZ:20, A0, POLYNOM3:34;
q <> 0_. R by A5, A0, POLYNOM3:34;
then deg p = (deg q) + (deg rr) by A4, A5, HURWITZ:23
.= (deg q) + 0 by A2, T88 ;
hence contradiction by A0; :: thesis: verum

end;

hence p is reducible by A0, A1, RING_2:def 9; :: thesis: verum