let n be Element of NAT ; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q being Element of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) )
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q being Element of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) )
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p, q being Element of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) )
let p, q be Element of (Polynom-Ring (n,L)); :: thesis: for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_wrt T holds
( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) )
let G be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( G is_Groebner_basis_wrt T implies ( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) ) )
set R = PolyRedRel (G,T);
assume G is_Groebner_basis_wrt T ; :: thesis: ( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) )
then A1: PolyRedRel (G,T) is locally-confluent by Def3;

now

nf (q,(PolyRedRel (G,T))) is_a_normal_form_of q, PolyRedRel (G,T) by A1, REWRITE1:54;
then PolyRedRel (G,T) reduces q, nf (q,(PolyRedRel (G,T))) by REWRITE1:def 6;
then A2: nf (q,(PolyRedRel (G,T))),q are_convertible_wrt PolyRedRel (G,T) by REWRITE1:25;
nf (p,(PolyRedRel (G,T))) is_a_normal_form_of p, PolyRedRel (G,T) by A1, REWRITE1:54;
then PolyRedRel (G,T) reduces p, nf (p,(PolyRedRel (G,T))) by REWRITE1:def 6;
then A3: p, nf (p,(PolyRedRel (G,T))) are_convertible_wrt PolyRedRel (G,T) by REWRITE1:25;
assume nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) ; :: thesis: p,q are_congruent_mod G -Ideal
hence p,q are_congruent_mod G -Ideal by A3, A2, POLYRED:57, REWRITE1:30; :: thesis: verum

end;

hence ( p,q are_congruent_mod G -Ideal iff nf (p,(PolyRedRel (G,T))) = nf (q,(PolyRedRel (G,T))) ) by A1, POLYRED:58, REWRITE1:55; :: thesis: verum