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 x being Element of (ValuatRing v) holds x is Element of K
let v be Valuation of K; :: thesis: ( K is having_valuation implies for x being Element of (ValuatRing v) holds x is Element of K )
assume A1: K is having_valuation ; :: thesis: for x being Element of (ValuatRing v) holds x is Element of K
let x be Element of (ValuatRing v); :: thesis: x is Element of K
the carrier of (ValuatRing v) = NonNegElements v by A1, Def12;
then ( x in NonNegElements v & NonNegElements v c= the carrier of K ) by Th48;
hence x is Element of K ; :: thesis: verum