defpred S₁[ set ] means ex W being 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₁[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 Walk of G st W is_Walk_from v,x )
let x be object ; :: thesis: ( x in IT iff ex W being Walk of G st W is_Walk_from v,x )
thus ( x in IT implies ex W being Walk of G st W is_Walk_from v,x ) by A1; :: thesis: ( ex W being Walk of G st W is_Walk_from v,x implies x in IT )
assume A2: ex W being Walk of G st W is_Walk_from v,x ; :: thesis: x in IT
then x is Vertex of G by GLIB_001:18;
hence x in IT by A1, A2; :: thesis: verum