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 (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 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 (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 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 (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 )
assume A2: for f being Polynomial of n,L st f in I holds
PolyRedRel G,T reduces f, 0_ n,L ; :: thesis: G -Ideal = I

A3: now

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

end;

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 (Polynom-Ring n,L) ;
reconsider u' = u' as Polynomial of n,L by POLYNOM1:def 27;
PolyRedRel G,T reduces u', 0_ n,L by A2, A5;
hence u in G -Ideal by POLYRED:60; :: thesis: verum

end;

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