theorem Th16: :: GLIB_004:16

for G being real-weighted WGraph
for L being DIJK:Labeling of G holds
( dom (L `1) c= dom ((DIJK:Step L) `1) & L `2 c= (DIJK:Step L) `2 )