let G be Graph; :: thesis: for p being oriented Chain of G
for W being Function
for V being set
for v1, v2 being Vertex of G holds
( p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/ {v2},W )
let p be oriented Chain of G; :: thesis: for W being Function
for V being set
for v1, v2 being Vertex of G holds
( p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/ {v2},W )
let W be Function; :: thesis: for V being set
for v1, v2 being Vertex of G holds
( p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/ {v2},W )
let V be set ; :: thesis: for v1, v2 being Vertex of G holds
( p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/ {v2},W )
let v1, v2 be Vertex of G; :: thesis: ( p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/ {v2},W )
set V9 = V \/ {v2};

hereby :: thesis: ( p is_shortestpath_of v1,v2,V \/ {v2},W implies p is_shortestpath_of v1,v2,V,W )

assume A1: p is_shortestpath_of v1,v2,V,W ; :: thesis: p is_shortestpath_of v1,v2,V \/ {v2},W

A2: now :: thesis: for q being oriented Chain of G st q is_orientedpath_of v1,v2,V \/ {v2} holds
cost (p,W) <= cost (q,W)

let q be oriented Chain of G; :: thesis: ( q is_orientedpath_of v1,v2,V \/ {v2} implies cost (p,W) <= cost (q,W) )
assume q is_orientedpath_of v1,v2,V \/ {v2} ; :: thesis: cost (p,W) <= cost (q,W)
then q is_orientedpath_of v1,v2,V by Th7;
hence cost (p,W) <= cost (q,W) by A1, GRAPH_5:def 18; :: thesis: verum

end;

p is_orientedpath_of v1,v2,V by A1, GRAPH_5:def 18;
then p is_orientedpath_of v1,v2,V \/ {v2} by Th7;
hence p is_shortestpath_of v1,v2,V \/ {v2},W by A2, GRAPH_5:def 18; :: thesis: verum

end;

assume A3: p is_shortestpath_of v1,v2,V \/ {v2},W ; :: thesis: p is_shortestpath_of v1,v2,V,W

A4: now :: thesis: for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds
cost (p,W) <= cost (q,W)

let q be oriented Chain of G; :: thesis: ( q is_orientedpath_of v1,v2,V implies cost (p,W) <= cost (q,W) )
assume q is_orientedpath_of v1,v2,V ; :: thesis: cost (p,W) <= cost (q,W)
then q is_orientedpath_of v1,v2,V \/ {v2} by Th7;
hence cost (p,W) <= cost (q,W) by A3, GRAPH_5:def 18; :: thesis: verum

end;

p is_orientedpath_of v1,v2,V \/ {v2} by A3, GRAPH_5:def 18;
then p is_orientedpath_of v1,v2,V by Th7;
hence p is_shortestpath_of v1,v2,V,W by A4, GRAPH_5:def 18; :: thesis: verum