theorem :: GLIB_002:27

for G being _Graph
for x being set st x in G .componentSet() holds
x is non empty Subset of (the_Vertices_of G) by Lm13;