set X = { W where W is DPath of G : W is_Walk_from x,y } ;

let e be object ; :: thesis:
assume e in { W where W is DPath of G : W is_Walk_from x,y } ; :: thesis:
then ex W being DPath of G st
( e = W & W is_Walk_from x,y ) ;
then e in { w where w is DPath of G : verum } ;
hence e in G .allDPaths() by GLIB_001:def 38; :: thesis:

end;

then reconsider X = { W where W is DPath of G : W is_Walk_from x,y } as finite Subset of (G .allDPaths()) by TARSKI:def 3;

assume ex W being DWalk of G st W is_Walk_from x,y ; :: thesis:
then consider W being DWalk of G such that
A1: W is_Walk_from x,y ;
set P = the DPath of W;
the DPath of W is_Walk_from x,y by A1, GLIB_001:160;
then the DPath of W in X ;
then reconsider X = X as non empty finite Subset of (G .allDPaths()) ;
deffunc H₁( Element of X) -> object = $1 .cost() ;
consider W1 being Element of X such that
A2: for W2 being Element of X holds H₁(W1) <= H₁(W2) from PRE_CIRC:sch 5();
W1 in X ;
then consider WA being DPath of G such that
A3: WA = W1 and
A4: WA is_Walk_from x,y ;

let WB be DPath of G; :: thesis:
assume WB is_Walk_from x,y ; :: thesis:
then WB in X ;
then reconsider WB9 = WB as Element of X ;
H₁(W1) <= H₁(WB9) by A2;
hence WA .cost() <= WB .cost() by A3; :: thesis:

end;

reconsider WA = WA as DPath of G ;
set IT = WA .cost() ;
take IT = WA .cost() ; :: thesis:
take WA = WA; :: thesis:
thus WA is_mincost_DPath_from x,y by A4, A5; :: thesis:
thus IT = WA .cost() ; :: thesis:

end;

thus ( ( for W being DWalk of G holds not W is_Walk_from x,y ) implies ex b₁ being Real st b₁ = 0 ) ; :: thesis: