let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K
for v being Valuation of K st K is having_valuation & v . a = 0 holds
for I being Ideal of () holds
( a in I iff I = the carrier of () )

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & v . a = 0 holds
for I being Ideal of () holds
( a in I iff I = the carrier of () )

let v be Valuation of K; :: thesis: ( K is having_valuation & v . a = 0 implies for I being Ideal of () holds
( a in I iff I = the carrier of () ) )

assume A1: K is having_valuation ; :: thesis: ( not v . a = 0 or for I being Ideal of () holds
( a in I iff I = the carrier of () ) )

assume A2: v . a = 0 ; :: thesis: for I being Ideal of () holds
( a in I iff I = the carrier of () )

let I be Ideal of (); :: thesis: ( a in I iff I = the carrier of () )
thus ( a in I implies I = the carrier of () ) :: thesis: ( I = the carrier of () implies a in I )
proof
assume A3: a in I ; :: thesis: I = the carrier of ()
thus I c= the carrier of () ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of () c= I
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of () or x in I )
assume x in the carrier of () ; :: thesis: x in I
then reconsider x = x as Element of () ;
reconsider b = x as Element of K by ;
A4: a <> 0. K by A1, A2, Def8;
reconsider y = a, z = a " as Element of () by A1, A2, Th72;
A5: y * (z * x) in I by ;
reconsider za = z * x as Element of K by ;
z * x = (a ") * b by ;
then y * (z * x) = a * ((a ") * b) by ;
hence x in I by A5, A4, Lm8; :: thesis: verum
end;
the carrier of () = NonNegElements v by ;
hence ( I = the carrier of () implies a in I ) by A2; :: thesis: verum