theorem Th39: :: GRAPHSP:39

for i, k, n being Nat
for f, g, h being Element of REAL * st g = ((repeat ((Relax n) * (findmin n))) . i) . f & h = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f & k = Argmin ((OuterVx (g,n)),g,n) & OuterVx (g,n) <> {} holds
( UsedVx (h,n) = (UsedVx (g,n)) \/ {k} & not k in UsedVx (g,n) )