:: deftheorem defines is_DTree_rooted_at GLIB_002:def 4 :
for G being _Graph
for v being set holds
( G is_DTree_rooted_at v iff ( G is Tree-like & ( for x being Vertex of G ex W being DWalk of G st W is_Walk_from v,x ) ) );