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 V268( ValuatRing v)

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

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 V268( ValuatRing v)

proof

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 )
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;hence vp v <> the carrier of (ValuatRing v) by A1, Th63; :: according to SUBSET_1:def 6 :: thesis: verum

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