let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis:
let v be Valuation of K; :: thesis:
let S be non empty Subset of K; :: thesis:
assume A1: K is having_valuation ; :: thesis:
assume A2: S is Subset of (ValuatRing v) ; :: thesis:
A3: min (S,v) = (v " {(inf (v .: S))}) /\ S by A1, A2, Def14;
A4: inf (v .: S) is LowerBound of v .: S by XXREAL_2:def 4;
let x be Element of K; :: thesis:

hereby :: thesis:

assume A5: x in min (S,v) ; :: thesis:
then x in v " {(inf (v .: S))} by A3, XBOOLE_0:def 4;
then v . x in {(inf (v .: S))} by FUNCT_2:38;
then A6: v . x = inf (v .: S) by TARSKI:def 1;
min (S,v) c= S by A1, A2, Th64;
hence x in S by A5; :: thesis:
let y be Element of K; :: thesis:
assume y in S ; :: thesis:
hence v . x <= v . y by A6, A4, FUNCT_2:35, XXREAL_2:def 2; :: thesis:

end;

assume that
A7: x in S and
A8: for y being Element of K st y in S holds
v . x <= v . y ; :: thesis:
A9: v . x is LowerBound of v .: S

let a be ExtReal; :: according to XXREAL_2:def 2 :: thesis:
assume a in v .: S ; :: thesis:
then ex y being Element of K st
( y in S & a = v . y ) by FUNCT_2:65;
hence v . x <= a by A8; :: thesis:

end;

for y being LowerBound of v .: S holds y <= v . x by A7, FUNCT_2:35, XXREAL_2:def 2;
then v . x = inf (v .: S) by A9, XXREAL_2:def 4;
then v . x in {(inf (v .: S))} by TARSKI:def 1;
then x in v " {(inf (v .: S))} by FUNCT_2:38;
hence x in min (S,v) by A7, A3; :: thesis: