let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; :: thesis: for v being Valuation of K st K is having_valuation holds
vp v is maximal
let v be Valuation of K; :: thesis: ( K is having_valuation implies vp v is maximal )
assume A1: K is having_valuation ; :: thesis: vp v is maximal
thus vp v is proper :: according to RING_1:def 4 :: thesis: vp v is V247( ValuatRing v)

proof

1. (ValuatRing v) = 1. K by A1, Def14;
hence vp v <> the carrier of (ValuatRing v) by A1, Th66; :: according to SUBSET_1:def 6 :: thesis: verum

end;

let J be Ideal of (ValuatRing v); :: according to RING_1:def 3 :: thesis: ( not vp v c= J or J = vp v or not J is proper )
assume A2: vp v c= J ; :: thesis: ( J = vp v or not J is proper )
( not J is proper or J = vp v )

proof

assume J is proper ; :: thesis: J = vp v
then J c= vp v by A1, Th82;
hence J = vp v by A2, XBOOLE_0:def 10; :: thesis: verum

end;

hence ( J = vp v or not J is proper ) ; :: thesis: verum