theorem Th24: :: GLIB_008:24

for G being _Graph
for C being a_partition of the_Vertices_of G
for v being Vertex of G st C = G .componentSet() holds
EqClass (v,C) = G .reachableFrom v