theorem lemlowp1a1: :: REALALG1:9

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