let G be Graph; :: thesis: for p, q being oriented Chain of G
for W being Function
for V being set
for v1, v2 being Vertex of G st p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W holds
cost p,W = cost q,W
let p, q be oriented Chain of G; :: thesis: for W being Function
for V being set
for v1, v2 being Vertex of G st p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W holds
cost p,W = cost q,W
let W be Function; :: thesis: for V being set
for v1, v2 being Vertex of G st p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W holds
cost p,W = cost q,W
let V be set ; :: thesis: for v1, v2 being Vertex of G st p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W holds
cost p,W = cost q,W
let v1, v2 be Vertex of G; :: thesis: ( p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W implies cost p,W = cost q,W )
assume A1: ( p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W ) ; :: thesis: cost p,W = cost q,W
then A2: ( p is_orientedpath_of v1,v2,V & ( for r being oriented Chain of G st r is_orientedpath_of v1,v2,V holds
cost p,W <= cost r,W ) ) by GRAPH_5:def 18;
( q is_orientedpath_of v1,v2,V & ( for r being oriented Chain of G st r is_orientedpath_of v1,v2,V holds
cost q,W <= cost r,W ) ) by A1, GRAPH_5:def 18;
then A3: cost p,W <= cost q,W by A1, GRAPH_5:def 18;
cost q,W <= cost p,W by A1, A2, GRAPH_5:def 18;
hence cost p,W = cost q,W by A3, XXREAL_0:1; :: thesis: verum