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 proper

let v be Valuation of K; :: thesis: ( K is having_valuation implies vp v is proper )

assume A1: K is having_valuation ; :: thesis: vp v is proper

then 1. K is Element of (ValuatRing v) by Def12;

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

vp v is proper

let v be Valuation of K; :: thesis: ( K is having_valuation implies vp v is proper )

assume A1: K is having_valuation ; :: thesis: vp v is proper

then 1. K is Element of (ValuatRing v) by Def12;

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