let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds 0_ (n,L) <= p,T
let T be connected TermOrder of n; :: thesis: for L being non empty ZeroStr
for p being Polynomial of n,L holds 0_ (n,L) <= p,T
let L be non empty ZeroStr ; :: thesis: for p being Polynomial of n,L holds 0_ (n,L) <= p,T
let p be Polynomial of n,L; :: thesis: 0_ (n,L) <= p,T
set sp0 = Support (0_ (n,L));
set sp = Support p;
set R = RelStr(# (Bags n),T #);
A1: Support p is Element of Fin the carrier of RelStr(# (Bags n),T #) by Lm11;
( Support (0_ (n,L)) = {} & Support (0_ (n,L)) is Element of Fin the carrier of RelStr(# (Bags n),T #) ) by Lm11, POLYNOM7:1;
then [(Support (0_ (n,L))),(Support p)] in { [x,y] where x, y is Element of Fin the carrier of RelStr(# (Bags n),T #) : ( x = {} or ( x <> {} & y <> {} & PosetMax x <> PosetMax y & [(PosetMax x),(PosetMax y)] in the InternalRel of RelStr(# (Bags n),T #) ) ) } by A1;
then A2: [(Support (0_ (n,L))),(Support p)] in (FinOrd-Approx RelStr(# (Bags n),T #)) . 0 by BAGORDER:def 14;
dom (FinOrd-Approx RelStr(# (Bags n),T #)) = NAT by BAGORDER:def 14;
then (FinOrd-Approx RelStr(# (Bags n),T #)) . 0 in rng (FinOrd-Approx RelStr(# (Bags n),T #)) by FUNCT_1:3;
then [(Support (0_ (n,L))),(Support p)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A2, TARSKI:def 4;
then [(Support (0_ (n,L))),(Support p)] in FinOrd RelStr(# (Bags n),T #) by BAGORDER:def 15;
hence 0_ (n,L) <= p,T ; :: thesis: verum