theorem Th34: :: GRAPHSP:34

for n being Nat
for f being Element of REAL * st OuterVx (f,n) <> {} holds
ex j being Nat st
( j in OuterVx (f,n) & 1 <= j & j <= n & ((findmin n) . f) . j = - 1 )