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 maximal Ideal of (ValuatRing v) holds I = vp v

let v be Valuation of K; :: thesis: ( K is having_valuation implies for I being maximal Ideal of (ValuatRing v) holds I = vp v )

assume A1: K is having_valuation ; :: thesis: for I being maximal Ideal of (ValuatRing v) holds I = vp v

let I be maximal Ideal of (ValuatRing v); :: thesis: I = vp v

assume A2: not I = vp v ; :: thesis: contradiction

for I being maximal Ideal of (ValuatRing v) holds I = vp v

let v be Valuation of K; :: thesis: ( K is having_valuation implies for I being maximal Ideal of (ValuatRing v) holds I = vp v )

assume A1: K is having_valuation ; :: thesis: for I being maximal Ideal of (ValuatRing v) holds I = vp v

let I be maximal Ideal of (ValuatRing v); :: thesis: I = vp v

assume A2: not I = vp v ; :: thesis: contradiction

per cases
( not I c= vp v or I c= vp v )
;

end;

suppose
I c= vp v
; :: thesis: contradiction

then
( not vp v is proper or I = vp v )
by RING_1:def 3;

then A3: ( vp v = the carrier of (ValuatRing v) or I = vp v ) ;

1. (ValuatRing v) = 1. K by A1, Def12;

hence contradiction by A3, A1, A2, Th63; :: thesis: verum

end;then A3: ( vp v = the carrier of (ValuatRing v) or I = vp v ) ;

1. (ValuatRing v) = 1. K by A1, Def12;

hence contradiction by A3, A1, A2, Th63; :: thesis: verum