:: deftheorem defines DijkstraAlgorithm GRAPHSP:def 21 :
for n being Nat holds DijkstraAlgorithm n = while_do (((Relax n) * (findmin n)),n);