theorem Th30: :: GRAPHSP:30

for n being Nat
for f being Element of REAL * holds Argmin ((OuterVx (f,n)),f,n) <= n