theorem T88a: :: RING_4:40

for R being domRing
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