theorem Th23: :: GLIB_008:23

for G being _Graph holds G .componentSet() is a_partition of the_Vertices_of G