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