theorem Th6: :: GLIB_005:6

for G being finite real-weighted WGraph
for EL being FF:ELabeling of G
for source being Vertex of G holds AP:CompSeq (EL,source) is halting