let G be _Graph; :: thesis: for x being set st G is_DTree_rooted_at x holds

x is Vertex of G

let x be set ; :: thesis: ( G is_DTree_rooted_at x implies x is Vertex of G )

set v = the Vertex of G;

assume G is_DTree_rooted_at x ; :: thesis: x is Vertex of G

then ex W being DWalk of G st W is_Walk_from x, the Vertex of G ;

hence x is Vertex of G by GLIB_001:18; :: thesis: verum

x is Vertex of G

let x be set ; :: thesis: ( G is_DTree_rooted_at x implies x is Vertex of G )

set v = the Vertex of G;

assume G is_DTree_rooted_at x ; :: thesis: x is Vertex of G

then ex W being DWalk of G st W is_Walk_from x, the Vertex of G ;

hence x is Vertex of G by GLIB_001:18; :: thesis: verum