theorem Th15: :: GLIB_004:15

for G being _finite real-weighted WGraph
for L being DIJK:Labeling of G holds
( ( card (dom ((DIJK:Step L) `1)) = card (dom (L `1)) implies DIJK:NextBestEdges L = {} ) & ( DIJK:NextBestEdges L = {} implies card (dom ((DIJK:Step L) `1)) = card (dom (L `1)) ) & ( card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 implies DIJK:NextBestEdges L <> {} ) & ( DIJK:NextBestEdges L <> {} implies card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 ) )