let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; for v being Valuation of K st K is having_valuation holds
vp v is prime
let v be Valuation of K; ( K is having_valuation implies vp v is prime )
assume A1:
K is having_valuation
; vp v is prime
hence
vp v is proper
by Th76; RING_1:def 2 vp v is quasi-prime
let a, b be Element of (ValuatRing v); RING_1:def 1 ( not a * b in vp v or a in vp v or b in vp v )
assume A2:
a * b in vp v
; ( a in vp v or b in vp v )
assume
not a in vp v
; b in vp v
then A3:
v . a = 0
by A1, Th77;
assume A4:
not b in vp v
; contradiction
reconsider x = a, y = b as Element of K by A1, Th51;
A5:
a * b = x * y
by A1, Th55;
A6:
v . y = 0
by A1, A4, Th77;
v . (x * y) =
(v . x) + (v . y)
by A1, Def8
.=
0
by A3, A6
;
hence
contradiction
by A1, A2, A5, Th61; verum