theorem Th31: :: E_TRANS2:28

for u being Element of the carrier of (Polynom-Ring INT.Ring)
for a, b being Element of INT.Ring holds eval ((a * (~ u)),b) in {a} -Ideal