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

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