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

proof

let a be set ; :: 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, Th56;
then 0 <= inf vS by XXREAL_2:def 4;
hence a in NonNegElements v by A5; :: thesis: verum

end;

hence (v " {(inf (v .: S))}) /\ S is Subset of (ValuatRing v) by A1, Def14; :: thesis: verum