theorem Th18: :: GLIB_004:18

for G being real-weighted WGraph
for src being Vertex of G
for i, j being Nat st i <= j holds
( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . j) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . j) `2 )