let G1 be connected _Graph; :: thesis: for G2 being Component of G1 holds G1 == G2
let G2 be Component of G1; :: thesis: G1 == G2
reconsider G3 = G1 as Component of G1 by GLIB_002:30;
set v = the Vertex of G2;
reconsider w = the Vertex of G2 as Vertex of G1 by GLIB_000:42;
the_Vertices_of G2 = G1 .reachableFrom w by GLIB_002:33
.= the_Vertices_of G3 by GLIB_002:16 ;
hence G1 == G2 by GLIB_002:32; :: thesis: verum