theorem :: GLIB_002:32
for G being _Graph
for C1, C2 being Component of G holds
( the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 ) by Lm15;