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 Polynomial of n,L holds 0_ (n,L) is_irreducible_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 Polynomial of n,L holds 0_ (n,L) is_irreducible_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 Polynomial of n,L holds 0_ (n,L) is_irreducible_wrt p,T
let p be Polynomial of n,L; :: thesis: 0_ (n,L) is_irreducible_wrt p,T
assume 0_ (n,L) is_reducible_wrt p,T ; :: thesis: contradiction
then consider g being Polynomial of n,L such that
A1: 0_ (n,L) reduces_to g,p,T by Def8;
ex b being bag of n st 0_ (n,L) reduces_to g,p,b,T by A1, Def6;
hence contradiction by Def5; :: thesis: verum