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
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 quasi-maximal

proof

1. (ValuatRing v) = 1. K by A1, Def12;
hence vp v <> the carrier of (ValuatRing v) by A1, Th63; :: 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 ) by A1, Th79, A2;
hence ( J = vp v or not J is proper ) ; :: thesis: verum