let G be _finite real-weighted WGraph; :: thesis: for EL being FF:ELabeling of G
for source being Vertex of G holds source in dom (AP:FindAugPath (EL,source))
let EL be FF:ELabeling of G; :: thesis: for source being Vertex of G holds source in dom (AP:FindAugPath (EL,source))
let source be Vertex of G; :: thesis: source in dom (AP:FindAugPath (EL,source))
set CS = AP:CompSeq (EL,source);
dom ((AP:CompSeq (EL,source)) . 0) = {source} by Th4;
then A1: source in dom ((AP:CompSeq (EL,source)) . 0) by TARSKI:def 1;
dom ((AP:CompSeq (EL,source)) . 0) c= dom (AP:FindAugPath (EL,source)) by Th5;
hence source in dom (AP:FindAugPath (EL,source)) by A1; :: thesis: verum