:: deftheorem Def6 defines .reachableDFrom GLIB_002:def 6 :
for G being _Graph
for v being Vertex of G
for b₃ being non empty Subset of (the_Vertices_of G) holds
( b₃ = G .reachableDFrom v iff for x being object holds
( x in b₃ iff ex W being DWalk of G st W is_Walk_from v,x ) );