let G be _Graph; :: thesis: for x being set st G is_DTree_rooted_at x holds
x is Vertex of
let x be set ; :: thesis: ( G is_DTree_rooted_at x implies x is Vertex of )
consider v being Vertex of ;
assume G is_DTree_rooted_at x ; :: thesis: x is Vertex of
then ex W being DWalk of st W is_Walk_from x,v by Def4;
hence x is Vertex of by GLIB_001:19; :: thesis: verum