let G be _Graph; :: thesis: ( G is connected implies for v being Vertex of G holds G .reachableFrom v = the_Vertices_of G )

assume A1: G is connected ; :: thesis: for v being Vertex of G holds G .reachableFrom v = the_Vertices_of G

let v be Vertex of G; :: thesis: G .reachableFrom v = the_Vertices_of G

assume A1: G is connected ; :: thesis: for v being Vertex of G holds G .reachableFrom v = the_Vertices_of G

let v be Vertex of G; :: thesis: G .reachableFrom v = the_Vertices_of G

now :: thesis: for x being object holds

( ( x in G .reachableFrom v implies x in the_Vertices_of G ) & ( x in the_Vertices_of G implies x in G .reachableFrom v ) )

hence
G .reachableFrom v = the_Vertices_of G
by TARSKI:2; :: thesis: verum( ( x in G .reachableFrom v implies x in the_Vertices_of G ) & ( x in the_Vertices_of G implies x in G .reachableFrom v ) )

let x be object ; :: thesis: ( ( x in G .reachableFrom v implies x in the_Vertices_of G ) & ( x in the_Vertices_of G implies x in G .reachableFrom v ) )

thus ( x in G .reachableFrom v implies x in the_Vertices_of G ) ; :: thesis: ( x in the_Vertices_of G implies x in G .reachableFrom v )

assume x in the_Vertices_of G ; :: thesis: x in G .reachableFrom v

then ex W being Walk of G st W is_Walk_from v,x by A1;

hence x in G .reachableFrom v by Def5; :: thesis: verum

end;thus ( x in G .reachableFrom v implies x in the_Vertices_of G ) ; :: thesis: ( x in the_Vertices_of G implies x in G .reachableFrom v )

assume x in the_Vertices_of G ; :: thesis: x in G .reachableFrom v

then ex W being Walk of G st W is_Walk_from v,x by A1;

hence x in G .reachableFrom v by Def5; :: thesis: verum