let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A3: a in (v " {(inf (v .: S))}) /\ S ; :: thesis:
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:

end;