set W = G .walkOf v;

defpred S_{1}[ set ] means ex W being directed Walk of G st W is_Walk_from v,$1;

consider IT being Subset of (the_Vertices_of G) such that

A1: for x being set holds

( x in IT iff ( x in the_Vertices_of G & S_{1}[x] ) )
from SUBSET_1:sch 1();

G .walkOf v is_Walk_from v,v by GLIB_001:13;

then reconsider IT = IT as non empty Subset of (the_Vertices_of G) by A1;

take IT ; :: thesis: for x being object holds

( x in IT iff ex W being DWalk of G st W is_Walk_from v,x )

let x be object ; :: thesis: ( x in IT iff ex W being DWalk of G st W is_Walk_from v,x )

thus ( x in IT implies ex W being directed Walk of G st W is_Walk_from v,x ) by A1; :: thesis: ( ex W being DWalk of G st W is_Walk_from v,x implies x in IT )

given W being directed Walk of G such that A2: W is_Walk_from v,x ; :: thesis: x in IT

x is Vertex of G by A2, GLIB_001:18;

hence x in IT by A1, A2; :: thesis: verum

defpred S

consider IT being Subset of (the_Vertices_of G) such that

A1: for x being set holds

( x in IT iff ( x in the_Vertices_of G & S

G .walkOf v is_Walk_from v,v by GLIB_001:13;

then reconsider IT = IT as non empty Subset of (the_Vertices_of G) by A1;

take IT ; :: thesis: for x being object holds

( x in IT iff ex W being DWalk of G st W is_Walk_from v,x )

let x be object ; :: thesis: ( x in IT iff ex W being DWalk of G st W is_Walk_from v,x )

thus ( x in IT implies ex W being directed Walk of G st W is_Walk_from v,x ) by A1; :: thesis: ( ex W being DWalk of G st W is_Walk_from v,x implies x in IT )

given W being directed Walk of G such that A2: W is_Walk_from v,x ; :: thesis: x in IT

x is Vertex of G by A2, GLIB_001:18;

hence x in IT by A1, A2; :: thesis: verum