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