for G being _Graph
for C being Component of G
for v being Vertex of G holds
( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v ) by Lm16;