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:55;
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:26;
nf p,(PolyRedRel G,T) is_a_normal_form_of p, PolyRedRel G,T by A1, REWRITE1:55;
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:26;
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:31; :: 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:56; :: thesis: verum