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

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 (ValuatRing v) 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 (ValuatRing v) 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 (ValuatRing v) 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 (ValuatRing v) ; :: 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 A1, A2, Def14;

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 ) ) )

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

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: verum

for S being non empty Subset of K st K is having_valuation & S is Subset of (ValuatRing v) 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 (ValuatRing v) 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 (ValuatRing v) 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 (ValuatRing v) 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 (ValuatRing v) ; :: 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 A1, A2, Def14;

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 that 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 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: 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 A6, A4, FUNCT_2:35, XXREAL_2:def 2; :: thesis: verum

end;v . x <= v . y ) )

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: 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 A6, A4, FUNCT_2:35, XXREAL_2:def 2; :: thesis: verum

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

for y being LowerBound of v .: S holds y <= v . x
by A7, FUNCT_2:35, XXREAL_2:def 2;
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;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

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: verum