theorem Th17: :: GLIB_005:17

for G being _finite natural-weighted WGraph
for source, sink being Vertex of G st source <> sink holds
FF:CompSeq (G,source,sink) is halting