theorem :: GLIB_002:31

for G being _Graph
for C being Component of G holds the_Edges_of C = G .edgesBetween (the_Vertices_of C) by Lm14;