Изменения

|proof= Не теряя общности, будем считать, что граф связен. Тогда в конце работы алгоритма все вершины должны оказаться в <tex>M_0.</tex> Заметим, что на На каждом шаге мы гарантированно либо уменьшаем расстояние до какой-то вершины(возможно, она перейдет из <tex>M_0</tex> в <tex>M_1^{''}</tex>), либо перемещаем текущую вершину в <tex>M_0</tex>. Так как в графе нет отрицательных циклов, то уменьшить расстояние можно только конечное число раз. Количество вершин тоже конечно. Следовательно, будет произведено конечное число шагов.