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

now

let e be set ; :: thesis: ( e in { W where W is DPath of G : W is_Walk_from x,y } implies e in G .allDPaths() )
assume e in { W where W is DPath of G : W is_Walk_from x,y } ; :: thesis: e in G .allDPaths()
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: verum

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;

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

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

A5: now

let WB be DPath of G; :: thesis: ( WB is_Walk_from x,y implies WA .cost() <= WB .cost() )
assume WB is_Walk_from x,y ; :: thesis: WA .cost() <= WB .cost()
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: verum

end;

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

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: verum