theorem :: GLIB_002:34

for G being _Graph
for C1, C2 being Component of G
for v being set st v in the_Vertices_of C1 & v in the_Vertices_of C2 holds
C1 == C2 by Lm17;