theorem :: GLENUM00:201

for G being _Graph holds the_Vertices_of (G .allComponents()) = G .componentSet() by Lm3;