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 Abelian add-associative right_zeroed doubleLoopStr
for I being LeftIdeal of Polynom-Ring n,L
for G being non empty Subset of 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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for I being LeftIdeal of Polynom-Ring n,L
for G being non empty Subset of 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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for I being LeftIdeal of Polynom-Ring n,L
for G being non empty Subset of 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 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 ; :: 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

let u be set ; :: 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 15;
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

let u be set ; :: thesis: ( u in I implies u in G -Ideal )
assume A5: u in I ; :: thesis: u in G -Ideal
then reconsider u' = u as Element of ;
reconsider u' = u' as Polynomial of n,L by POLYNOM1:def 27;
PolyRedRel G,T reduces u', 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