let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L st Support q c= Support p holds
q <= p,T
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L st Support q c= Support p holds
q <= p,T
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p, q being Polynomial of n,L st Support q c= Support p holds
q <= p,T
let p, q be Polynomial of n,L; :: thesis: ( Support q c= Support p implies q <= p,T )
assume A1: Support q c= Support p ; :: thesis: q <= p,T
defpred S₁[ Element of NAT ] means for f, g being Polynomial of n,L st Support f c= Support g & card (Support f) = $1 holds
f <= g,T;
A2: S₁[ 0 ]

proof

let f, g be Polynomial of n,L; :: thesis: ( Support f c= Support g & card (Support f) = 0 implies f <= g,T )
assume ( Support f c= Support g & card (Support f) = 0 ) ; :: thesis: f <= g,T
then Support f, {} are_equipotent by CARD_1:def 5;
then Support f = {} by CARD_1:46;
then f = 0_ n,L by POLYNOM7:1;
hence f <= g,T by POLYRED:30; :: thesis: verum

end;

A3: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]

now

let f, g be Polynomial of n,L; :: thesis: ( Support f c= Support g & card (Support f) = k + 1 implies f <= g,T )
assume A5: ( Support f c= Support g & card (Support f) = k + 1 ) ; :: thesis: f <= g,T
set rf = Red f,T;
set rg = Red g,T;
set R = RelStr(# (Bags n),T #);
Support f <> {} by A5;
then A6: HT f,T in Support f by TERMORD:def 6;
then ( g <> 0_ n,L & f <> 0_ n,L ) by A5, POLYNOM7:1;
then A7: ( g is non-zero & f is non-zero ) by POLYNOM7:def 2;

now

per cases ( HT f,T = HT g,T or HT f,T <> HT g,T ) ;

case A8: HT f,T = HT g,T ; :: thesis: f <= g,T

A9: ( Support (Red f,T) = (Support f) \ {(HT f,T)} & Support (Red g,T) = (Support g) \ {(HT g,T)} ) by TERMORD:36;

now

let u be set ; :: thesis: ( u in Support (Red f,T) implies u in Support (Red g,T) )
assume u in Support (Red f,T) ; :: thesis: u in Support (Red g,T)
then ( u in Support f & not u in {(HT f,T)} ) by A9, XBOOLE_0:def 5;
hence u in Support (Red g,T) by A5, A8, A9, XBOOLE_0:def 5; :: thesis: verum

end;

then A10: Support (Red f,T) c= Support (Red g,T) by TARSKI:def 3;
A11: ( Support (Red f,T),T = Support (Red f,T) & Support (Red g,T),T = Support (Red g,T) & Support f,T = Support f & Support g,T = Support g ) by POLYRED:def 4;
for u being set st u in {(HT f,T)} holds
u in Support f by A6, TARSKI:def 1;
then A12: {(HT f,T)} c= Support f by TARSKI:def 3;
A13: (Support (Red f,T)) \/ {(HT f,T)} = (Support f) \/ {(HT f,T)} by A9, XBOOLE_1:39
.= Support f by A12, XBOOLE_1:12 ;
HT f,T in {(HT f,T)} by TARSKI:def 1;
then not HT f,T in Support (Red f,T) by A9, XBOOLE_0:def 5;
then (card (Support (Red f,T))) + 1 = k + 1 by A5, A13, CARD_2:54;
then Red f,T <= Red g,T,T by A4, A10;
then [(Support (Red f,T)),(Support (Red g,T))] in FinOrd RelStr(# (Bags n),T #) by POLYRED:def 2;
then A14: [(Support (Red f,T),T),(Support (Red g,T),T)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A11, BAGORDER:def 17;
A15: ( Support f,T <> {} & Support g,T <> {} ) by A5, A6, POLYRED:def 4;
A16: PosetMax (Support f,T) = HT g,T by A7, A8, POLYRED:24
.= PosetMax (Support g,T) by A7, POLYRED:24 ;
A17: (Support f,T) \ {(PosetMax (Support f,T))} = Support (Red f,T),T by A7, A9, A11, POLYRED:24;
(Support g,T) \ {(PosetMax (Support g,T))} = Support (Red g,T),T by A7, A9, A11, POLYRED:24;
then [(Support f,T),(Support g,T)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A14, A15, A16, A17, BAGORDER:36;
then [(Support f),(Support g)] in FinOrd RelStr(# (Bags n),T #) by A11, BAGORDER:def 17;
hence f <= g,T by POLYRED:def 2; :: thesis: verum

end;

case A18: HT f,T <> HT g,T ; :: thesis: f <= g,T

now

assume HT g,T < HT f,T,T ; :: thesis: contradiction
then not HT f,T <= HT g,T,T by TERMORD:5;
hence contradiction by A5, A6, TERMORD:def 6; :: thesis: verum

end;

then HT f,T <= HT g,T,T by TERMORD:5;
then HT f,T < HT g,T,T by A18, TERMORD:def 3;
then f < g,T by POLYRED:32;
hence f <= g,T by POLYRED:def 3; :: thesis: verum

end;

end;

end;

hence f <= g,T ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A19: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3);
consider k being Element of NAT such that
A20: card (Support q) = k ;
thus q <= p,T by A1, A19, A20; :: thesis: verum