theorem Th40: :: GRAPHSP:40

for n being Nat
for f being Element of REAL * ex i being Nat st
( i <= n & OuterVx ((((repeat ((Relax n) * (findmin n))) . i) . f),n) = {} )