let n be Ordinal; :: thesis: for T being connected 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 being Subset of (Polynom-Ring n,L) st ( for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T
let T be connected 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 being Subset of (Polynom-Ring n,L) st ( for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt 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 being Subset of (Polynom-Ring n,L) st ( for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T
let P be Subset of (Polynom-Ring n,L); :: thesis: ( ( for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L ) implies for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T )
assume A1: for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel P,T reduces f, 0_ n,L ; :: thesis: for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T

now

let f be non-zero Polynomial of n,L; :: thesis: ( f in P -Ideal implies f is_reducible_wrt P,T )
assume f in P -Ideal ; :: thesis: f is_reducible_wrt P,T
then A2: PolyRedRel P,T reduces f, 0_ n,L by A1;
f <> 0_ n,L by POLYNOM7:def 2;
then ex g being Polynomial of n,L st
( f reduces_to g,P,T & PolyRedRel P,T reduces g, 0_ n,L ) by A2, Lm5;
hence f is_reducible_wrt P,T by POLYRED:def 9; :: thesis: verum

end;

hence for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T ; :: thesis: verum