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
for S being non empty Subset of K st K is having_valuation & S is Subset of (ValuatRing v) holds
min (S,v) c= S
let v be Valuation of K; :: thesis: for S being non empty Subset of K st K is having_valuation & S is Subset of (ValuatRing v) holds
min (S,v) c= S
let S be non empty Subset of K; :: thesis: ( K is having_valuation & S is Subset of (ValuatRing v) implies min (S,v) c= S )
assume ( K is having_valuation & S is Subset of (ValuatRing v) ) ; :: thesis: min (S,v) c= S
then min (S,v) = (v " {(inf (v .: S))}) /\ S by Def14;
hence min (S,v) c= S by XBOOLE_1:17; :: thesis: verum