theorem lemlowp2: :: REALALG1:8

for R being non degenerated Ring
for p being Polynomial of R holds min* { i where i is Nat : (- p) . i <> 0. R } = min* { i where i is Nat : p . i <> 0. R }