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 () holds
for x being Element of K holds
( x in min (S,v) iff ( x in S & ( for y being Element of K st y in S holds
v . x <= v . y ) ) )

let v be Valuation of K; :: thesis: for S being non empty Subset of K st K is having_valuation & S is Subset of () holds
for x being Element of K holds
( x in min (S,v) iff ( x in S & ( for y being Element of K st y in S holds
v . x <= v . y ) ) )

let S be non empty Subset of K; :: thesis: ( K is having_valuation & S is Subset of () implies for x being Element of K holds
( x in min (S,v) iff ( x in S & ( for y being Element of K st y in S holds
v . x <= v . y ) ) ) )

assume A1: K is having_valuation ; :: thesis: ( not S is Subset of () or for x being Element of K holds
( x in min (S,v) iff ( x in S & ( for y being Element of K st y in S holds
v . x <= v . y ) ) ) )

assume A2: S is Subset of () ; :: thesis: for x being Element of K holds
( x in min (S,v) iff ( x in S & ( for y being Element of K st y in S holds
v . x <= v . y ) ) )

A3: min (S,v) = (v " {(inf (v .: S))}) /\ S by ;
A4: inf (v .: S) is LowerBound of v .: S by XXREAL_2:def 4;
let x be Element of K; :: thesis: ( x in min (S,v) iff ( x in S & ( for y being Element of K st y in S holds
v . x <= v . y ) ) )

hereby :: thesis: ( x in S & ( for y being Element of K st y in S holds
v . x <= v . y ) implies x in min (S,v) )
assume A5: x in min (S,v) ; :: thesis: ( x in S & ( for y being Element of K st y in S holds
v . x <= v . y ) )

then x in v " {(inf (v .: S))} by ;
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: for y being Element of K st y in S holds
v . x <= v . y

let y be Element of K; :: thesis: ( y in S implies v . x <= v . y )
assume y in S ; :: thesis: v . x <= v . y
hence v . x <= v . y by ; :: thesis: verum
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: x in min (S,v)
A9: v . x is LowerBound of v .: S
proof
let a be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not a in v .: S or v . x <= a )
assume a in v .: S ; :: thesis: v . x <= a
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: verum
end;
for y being LowerBound of v .: S holds y <= v . x by ;
then v . x = inf (v .: S) by ;
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: verum