let U, V be set ; :: thesis:
let G be oriented finite Graph; :: thesis:
let P be oriented Chain of G; :: thesis:
let W be Function of the carrier' of G,Real>=0; :: thesis:
let v1, v2 be Vertex of G; :: thesis:
assume A1: ( the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) ) ; :: thesis:

hereby :: thesis:

assume A2: P is_shortestpath_of v1,v2,U,W ; :: thesis:

A3: now :: thesis:

let Q be oriented Chain of G; :: thesis:
assume Q is_orientedpath_of v1,v2 ; :: thesis:
then Q is_orientedpath_of v1,v2,U by A1, Th12;
hence cost (P,W) <= cost (Q,W) by A2, GRAPH_5:def 18; :: thesis:

end;

P is_orientedpath_of v1,v2,U by A2, GRAPH_5:def 18;
then P is_orientedpath_of v1,v2 by GRAPH_5:def 4;
hence P is_shortestpath_of v1,v2,W by A3, GRAPH_5:def 17; :: thesis:

end;

hereby :: thesis:

assume A4: P is_shortestpath_of v1,v2,W ; :: thesis:

A5: now :: thesis:

let Q be oriented Chain of G; :: thesis:
assume Q is_orientedpath_of v1,v2,U ; :: thesis:
then Q is_orientedpath_of v1,v2 by GRAPH_5:def 4;
hence cost (P,W) <= cost (Q,W) by A4, GRAPH_5:def 17; :: thesis:

end;

P is_orientedpath_of v1,v2 by A4, GRAPH_5:def 17;
then P is_orientedpath_of v1,v2,U by A1, Th12;
hence P is_shortestpath_of v1,v2,U,W by A5, GRAPH_5:def 18; :: thesis:

end;