theorem lemlowp1a2: :: REALALG1:10

for R being non degenerated Ring
for p, q being non zero Polynomial of R st p + q <> 0_. R & 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 : p . i <> 0. R }