let R be non degenerated Ring; :: thesis: for n being Ordinal
for p being Polynomial of n,R holds
( Support (LM p) = {} or Support (LM p) = {(Lt p)} )
let n be Ordinal; :: thesis: for p being Polynomial of n,R holds
( Support (LM p) = {} or Support (LM p) = {(Lt p)} )
let p be Polynomial of n,R; :: thesis: ( Support (LM p) = {} or Support (LM p) = {(Lt p)} )
set m = LM p;

per cases ( Support (LM p) = {} or ex b being bag of n st Support (LM p) = {b} ) by POLYNOM7:6;

suppose Support (LM p) = {} ; :: thesis: ( Support (LM p) = {} or Support (LM p) = {(Lt p)} )

hence ( Support (LM p) = {} or Support (LM p) = {(Lt p)} ) ; :: thesis: verum

end;

suppose ex b being bag of n st Support (LM p) = {b} ; :: thesis: ( Support (LM p) = {} or Support (LM p) = {(Lt p)} )

then consider b being bag of n such that
H: Support (LM p) = {b} ;

per cases ( Support p = {} or Support p <> {} ) ;

suppose Support p = {} ; :: thesis: ( Support (LM p) = {} or Support (LM p) = {(Lt p)} )

then p = 0_ (n,R) by YY;
then ( Lt p = EmptyBag n & 0. R = p . b ) by defLT, POLYNOM1:22;
then not b in Support p by POLYNOM1:def 4;
then not b in Support (LM p) by YZ, TARSKI:def 3;
hence ( Support (LM p) = {} or Support (LM p) = {(Lt p)} ) by H, TARSKI:def 1; :: thesis: verum

end;

suppose Support p <> {} ; :: thesis: ( Support (LM p) = {} or Support (LM p) = {(Lt p)} )

then p <> 0_ (n,R) by YY;
then I: not LC p is zero by Y0;
{b} = {(term (LM p))} by H, POLYNOM7:7;
then b in {(term (LM p))} by TARSKI:def 1;
then b = term (LM p) by TARSKI:def 1
.= Lt p by I, POLYNOM7:10 ;
hence ( Support (LM p) = {} or Support (LM p) = {(Lt p)} ) by H; :: thesis: verum

end;

end;

end;

end;