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 )
consider v being 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,v by Def4;
hence x is Vertex of G by GLIB_001:19; :: thesis: verum