(v " {(inf (v .: S))}) /\ S c= NonNegElements v

proof

hence
(v " {(inf (v .: S))}) /\ S is Subset of (ValuatRing v)
by A1, Def12; :: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (v " {(inf (v .: S))}) /\ S or a in NonNegElements v )

assume A3: a in (v " {(inf (v .: S))}) /\ S ; :: thesis: a in NonNegElements v

then A4: a in v " {(inf (v .: S))} by XBOOLE_0:def 4;

reconsider a = a as Element of K by A3;

reconsider vS = v .: S as non empty Subset of ExtREAL ;

v . a in {(inf (v .: S))} by A4, FUNCT_2:38;

then A5: v . a = inf vS by TARSKI:def 1;

0 is LowerBound of vS by A1, A2, Th53;

then 0 <= inf vS by XXREAL_2:def 4;

hence a in NonNegElements v by A5; :: thesis: verum

end;assume A3: a in (v " {(inf (v .: S))}) /\ S ; :: thesis: a in NonNegElements v

then A4: a in v " {(inf (v .: S))} by XBOOLE_0:def 4;

reconsider a = a as Element of K by A3;

reconsider vS = v .: S as non empty Subset of ExtREAL ;

v . a in {(inf (v .: S))} by A4, FUNCT_2:38;

then A5: v . a = inf vS by TARSKI:def 1;

0 is LowerBound of vS by A1, A2, Th53;

then 0 <= inf vS by XXREAL_2:def 4;

hence a in NonNegElements v by A5; :: thesis: verum