theorem LT1: :: FIELD_11:7

for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R
for b being bag of n st b in Support p holds
( b = Lt p iff for b1 being bag of n st b1 in Support p holds
b1 <=' b )