let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for v being Valuation of K st K is having_valuation holds
for I being non empty Subset of K
for x being Element of (ValuatRing v) st I is Ideal of (ValuatRing v) & x in min (I,v) holds
I = {x} -Ideal
let v be Valuation of K; :: thesis: ( K is having_valuation implies for I being non empty Subset of K
for x being Element of (ValuatRing v) st I is Ideal of (ValuatRing v) & x in min (I,v) holds
I = {x} -Ideal )
assume A1: K is having_valuation ; :: thesis: for I being non empty Subset of K
for x being Element of (ValuatRing v) st I is Ideal of (ValuatRing v) & x in min (I,v) holds
I = {x} -Ideal
let I be non empty Subset of K; :: thesis: for x being Element of (ValuatRing v) st I is Ideal of (ValuatRing v) & x in min (I,v) holds
I = {x} -Ideal
let x be Element of (ValuatRing v); :: thesis: ( I is Ideal of (ValuatRing v) & x in min (I,v) implies I = {x} -Ideal )
assume A2: I is Ideal of (ValuatRing v) ; :: thesis: ( not x in min (I,v) or I = {x} -Ideal )
assume A3: x in min (I,v) ; :: thesis: I = {x} -Ideal
A4: min (I,v) c= I by A1, A2, Th64;
thus I c= {x} -Ideal :: according to XBOOLE_0:def 10 :: thesis: {x} -Ideal c= I

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in I or a in {x} -Ideal )
assume A5: a in I ; :: thesis: a in {x} -Ideal
then reconsider y = a as Element of (ValuatRing v) by A2;
reconsider x1 = x, y1 = y as Element of K by A1, Th51;

per cases ( x <> 0. K or x = 0. (ValuatRing v) ) by A1, Def12;

suppose A6: x <> 0. K ; :: thesis: a in {x} -Ideal

set r1 = y1 / x1;
v . x1 <= v . y1 by A1, A2, A3, A5, Th65;
then 0 <= (v . y1) - (v . x1) by Lm4;
then 0 <= v . (y1 / x1) by A6, A1, Th22;
then reconsider r0 = y1 / x1 as Element of (ValuatRing v) by A1, Th52;
x1 * (y1 / x1) = y1 * ((x1 ") * x1) by GROUP_1:def 3
.= y1 * (1_ K) by A6, VECTSP_2:9
.= y1 ;
then A7: y = x * r0 by A1, Th55;
{x} -Ideal = { (x * r) where r is Element of (ValuatRing v) : verum } by IDEAL_1:64;
hence a in {x} -Ideal by A7; :: thesis: verum

end;

suppose A8: x = 0. (ValuatRing v) ; :: thesis: a in {x} -Ideal

then A9: {x} -Ideal = {(0. (ValuatRing v))} by IDEAL_1:47;
A10: 0. (ValuatRing v) = 0. K by A1, Def12;
then A11: v . x1 = +infty by A1, A8, Def8;
v . x1 <= v . y1 by A1, A5, A2, A3, Th65;
then y = 0. (ValuatRing v) by A1, A10, Th18, A11, XXREAL_0:4;
hence a in {x} -Ideal by A9, TARSKI:def 1; :: thesis: verum

end;

end;

end;

{x} c= I by A4, A3, ZFMISC_1:31;
hence {x} -Ideal c= I by A2, IDEAL_1:def 14; :: thesis: verum