theorem Th37: :: GLIB_004:37

for G being _finite real-weighted WGraph holds
( PRIM:CompSeq G is halting & ((PRIM:CompSeq G) .Lifespan()) + 1 = card (G .reachableFrom the Element of the_Vertices_of G) )