theorem Th25: :: GLIB_004:25

for G being _finite real-weighted WGraph
for s being Vertex of G holds ((DIJK:CompSeq s) .Lifespan()) + 1 = card (G .reachableDFrom s)