let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being LeftIdeal of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds
G -Ideal = I
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being LeftIdeal of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds
G -Ideal = I
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for I being LeftIdeal of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds
G -Ideal = I
let I be LeftIdeal of (Polynom-Ring (n,L)); :: thesis: for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds
G -Ideal = I
let G be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( G c= I & ( for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) ) implies G -Ideal = I )
assume A1: G c= I ; :: thesis: ( ex f being Polynomial of n,L st
( f in I & not PolyRedRel (G,T) reduces f, 0_ (n,L) ) or G -Ideal = I )

A2: now :: thesis: for u being object st u in G -Ideal holds
u in I

let u be object ; :: thesis: ( u in G -Ideal implies u in I )
assume A3: u in G -Ideal ; :: thesis: u in I
G -Ideal c= I by A1, IDEAL_1:def 14;
hence u in I by A3; :: thesis: verum

end;

assume A4: for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) ; :: thesis: G -Ideal = I

now :: thesis: for u being object st u in I holds
u in G -Ideal

let u be object ; :: thesis: ( u in I implies u in G -Ideal )
assume A5: u in I ; :: thesis: u in G -Ideal
then reconsider u9 = u as Element of (Polynom-Ring (n,L)) ;
reconsider u9 = u9 as Polynomial of n,L by POLYNOM1:def 11;
PolyRedRel (G,T) reduces u9, 0_ (n,L) by A4, A5;
hence u in G -Ideal by POLYRED:60; :: thesis: verum

end;

hence G -Ideal = I by A2, TARSKI:2; :: thesis: verum