let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 well-unital distributive add-associative right_zeroed associative commutative 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 well-unital distributive add-associative right_zeroed associative commutative 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₁[ 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: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for f, g being Polynomial of n,L st Support f c= Support g & card (Support f) = k + 1 holds
f <= g,T

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

now :: thesis: ( ( HT (f,T) = HT (g,T) & f <= g,T ) or ( HT (f,T) <> HT (g,T) & f <= g,T ) )

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

case A10: HT (f,T) = HT (g,T) ; :: thesis: f <= g,T

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

now :: thesis: for u being object st u in Support (Red (f,T)) holds
u in Support (Red (g,T))

let u be object ; :: 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 A11, XBOOLE_0:def 5;
hence u in Support (Red (g,T)) by A4, A10, A12, XBOOLE_0:def 5; :: thesis: verum

end;

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

end;

case A24: HT (f,T) <> HT (g,T) ; :: thesis: f <= g,T

now :: thesis: not HT (g,T) < HT (f,T),T

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 A4, A7, 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 A24, 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;

A25: ex k being Element of NAT st card (Support q) = k ;
A26: 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 that
Support f c= Support g and
A27: card (Support f) = 0 ; :: thesis: f <= g,T
Support f = {} by A27;
then f = 0_ (n,L) by POLYNOM7:1;
hence f <= g,T by POLYRED:30; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A26, A2);
hence q <= p,T by A1, A25; :: thesis: verum