let n be Element of NAT ; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis:
let P be Subset of (Polynom-Ring n,L); :: thesis:
assume A1: for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T ; :: thesis:
thus for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T :: thesis:

proof

set H = { g where g is non-zero Polynomial of n,L : ( g in P -Ideal & not g is_top_reducible_wrt P,T ) } ;
let f be non-zero Polynomial of n,L; :: thesis:
assume A2: f in P -Ideal ; :: thesis:
assume not f is_top_reducible_wrt P,T ; :: thesis:
then A3: f in { g where g is non-zero Polynomial of n,L : ( g in P -Ideal & not g is_top_reducible_wrt P,T ) } by A2;

now

let u be set ; :: thesis:
assume u in { g where g is non-zero Polynomial of n,L : ( g in P -Ideal & not g is_top_reducible_wrt P,T ) } ; :: thesis:
then ex g9 being non-zero Polynomial of n,L st
( u = g9 & g9 in P -Ideal & not g9 is_top_reducible_wrt P,T ) ;
hence u in the carrier of (Polynom-Ring n,L) ; :: thesis:

end;

then reconsider H = { g where g is non-zero Polynomial of n,L : ( g in P -Ideal & not g is_top_reducible_wrt P,T ) } as non empty Subset of (Polynom-Ring n,L) by A3, TARSKI:def 3;
consider p being Polynomial of n,L such that
A4: p in H and
A5: for q being Polynomial of n,L st q in H holds
p <= q,T by POLYRED:31;
A6: ex p9 being non-zero Polynomial of n,L st
( p9 = p & p9 in P -Ideal & not p9 is_top_reducible_wrt P,T ) by A4;
then reconsider p = p as non-zero Polynomial of n,L ;
p is_reducible_wrt P,T by A1, A6;
then consider q being Polynomial of n,L such that
A7: p reduces_to q,P,T by POLYRED:def 9;
consider u being Polynomial of n,L such that
A8: u in P and
A9: p reduces_to q,u,T by A7, POLYRED:def 7;
ex b being bag of n st p reduces_to q,u,b,T by A9, POLYRED:def 6;
then A10: u <> 0_ n,L by POLYRED:def 5;
then reconsider u = u as non-zero Polynomial of n,L by POLYNOM7:def 2;
consider b being bag of n such that
A11: p reduces_to q,u,b,T by A9, POLYRED:def 6;

A12: now

assume b = HT p,T ; :: thesis:
then p top_reduces_to q,u,T by A11, POLYRED:def 10;
then p is_top_reducible_wrt u,T by POLYRED:def 11;
hence contradiction by A6, A8, POLYRED:def 12; :: thesis:

end;

consider m being Monomial of n,L such that
A13: q = p - (m *' u) by A9, Th1;
reconsider uu = u, pp = p, mm = m as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider uu = uu, pp = pp, mm = mm as Element of (Polynom-Ring n,L) ;
uu in P -Ideal by A8, Lm1;
then mm * uu in P -Ideal by IDEAL_1:def 2;
then - (mm * uu) in P -Ideal by IDEAL_1:13;
then A14: pp + (- (mm * uu)) in P -Ideal by A6, IDEAL_1:def 1;
mm * uu = m *' u by POLYNOM1:def 27;
then p - (m *' u) = pp - (mm * uu) by Lm2;
then A15: q in P -Ideal by A13, A14, RLVECT_1:def 14;
A16: q < p,T by A9, POLYRED:43;
A17: p <> 0_ n,L by POLYNOM7:def 2;
then Support p <> {} by POLYNOM7:1;
then A18: HT p,T in Support p by TERMORD:def 6;
b in Support p by A11, POLYRED:def 5;
then b <= HT p,T,T by TERMORD:def 6;
then b < HT p,T,T by A12, TERMORD:def 3;
then A19: HT p,T in Support q by A18, A11, POLYRED:40;

now

per cases ;

case A20: q <> 0_ n,L ; :: thesis:

then reconsider q = q as non-zero Polynomial of n,L by POLYNOM7:def 2;
Support q <> {} by A20, POLYNOM7:1;
then HT q,T in Support q by TERMORD:def 6;
then A21: HT q,T <= HT p,T,T by A9, POLYRED:42;
HT p,T <= HT q,T,T by A19, TERMORD:def 6;
then A22: HT q,T = HT p,T by A21, TERMORD:7;

now

assume not q is_top_reducible_wrt P,T ; :: thesis:
then q in H by A15;
then p <= q,T by A5;
hence contradiction by A16, POLYRED:29; :: thesis:

end;

then consider u9 being Polynomial of n,L such that
A23: u9 in P and
A24: q is_top_reducible_wrt u9,T by POLYRED:def 12;
consider q9 being Polynomial of n,L such that
A25: q top_reduces_to q9,u9,T by A24, POLYRED:def 11;
A26: p <> 0_ n,L by POLYNOM7:def 2;
then Support p <> {} by POLYNOM7:1;
then A27: HT p,T in Support p by TERMORD:def 6;
A28: q reduces_to q9,u9, HT q,T,T by A25, POLYRED:def 10;
then consider s being bag of n such that
A29: s + (HT u9,T) = HT q,T and
q9 = q - (((q . (HT q,T)) / (HC u9,T)) * (s *' u9)) by POLYRED:def 5;
set qq = p - (((p . (HT p,T)) / (HC u9,T)) * (s *' u9));
u9 <> 0_ n,L by A28, POLYRED:def 5;
then p reduces_to p - (((p . (HT p,T)) / (HC u9,T)) * (s *' u9)),u9, HT p,T,T by A22, A29, A26, A27, POLYRED:def 5;
then p top_reduces_to p - (((p . (HT p,T)) / (HC u9,T)) * (s *' u9)),u9,T by POLYRED:def 10;
then p is_top_reducible_wrt u9,T by POLYRED:def 11;
hence contradiction by A6, A23, POLYRED:def 12; :: thesis:

end;

case q = 0_ n,L ; :: thesis:

then A30: m *' u = (p - (m *' u)) + (m *' u) by A13, POLYRED:2
.= (p + (- (m *' u))) + (m *' u) by POLYNOM1:def 23
.= p + ((- (m *' u)) + (m *' u)) by POLYNOM1:80
.= p + (0_ n,L) by POLYRED:3
.= p by POLYNOM1:82 ;

now

A31: p <> 0_ n,L by POLYNOM7:def 2;
assume m = 0_ n,L ; :: thesis:
hence contradiction by A30, A31, POLYRED:5; :: thesis:

end;

then reconsider m = m as non-zero Polynomial of n,L by POLYNOM7:def 2;
set pp = p - (((p . (HT p,T)) / (HC u,T)) * ((HT m,T) *' u));
HT p,T = (HT m,T) + (HT u,T) by A30, TERMORD:31;
then p reduces_to p - (((p . (HT p,T)) / (HC u,T)) * ((HT m,T) *' u)),u, HT p,T,T by A10, A17, A18, POLYRED:def 5;
then p top_reduces_to p - (((p . (HT p,T)) / (HC u,T)) * ((HT m,T) *' u)),u,T by POLYRED:def 10;
then p is_top_reducible_wrt u,T by POLYRED:def 11;
hence contradiction by A6, A8, POLYRED:def 12; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;