for G being _finite real-weighted WGraph
for EL being FF:ELabeling of G
for source being Vertex of G holds source in dom (AP:FindAugPath (EL,source))