for G being _Graph
for v being Vertex of G holds v in G .reachableDFrom v