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 () st I is Ideal of () & 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 () st I is Ideal of () & 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 () st I is Ideal of () & x in min (I,v) holds
I = {x} -Ideal

let I be non empty Subset of K; :: thesis: for x being Element of () st I is Ideal of () & x in min (I,v) holds
I = {x} -Ideal

let x be Element of (); :: thesis: ( I is Ideal of () & x in min (I,v) implies I = {x} -Ideal )
assume A2: I is Ideal of () ; :: thesis: ( not x in min (I,v) or I = {x} -Ideal )
assume A3: x in min (I,v) ; :: thesis:
A4: min (I,v) c= I by A1, A2, Th64;
thus I c= {x} -Ideal :: according to XBOOLE_0:def 10 :: thesis:
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:
then reconsider y = a as Element of () by A2;
reconsider x1 = x, y1 = y as Element of K by ;
per cases ( x <> 0. K or x = 0. () ) by ;
suppose A6: x <> 0. K ; :: thesis:
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 () by ;
x1 * (y1 / x1) = y1 * ((x1 ") * x1) by GROUP_1:def 3
.= y1 * (1_ K) by
.= y1 ;
then A7: y = x * r0 by ;
{x} -Ideal = { (x * r) where r is Element of () : verum } by IDEAL_1:64;
hence a in {x} -Ideal by A7; :: thesis: verum
end;
suppose A8: x = 0. () ; :: thesis:
then A9: {x} -Ideal = {(0. ())} by IDEAL_1:47;
A10: 0. () = 0. K by ;
then A11: v . x1 = +infty by A1, A8, Def8;
v . x1 <= v . y1 by A1, A5, A2, A3, Th65;
then y = 0. () by ;
hence a in {x} -Ideal by ; :: thesis: verum
end;
end;
end;
{x} c= I by ;
hence {x} -Ideal c= I by ; :: thesis: verum