let S be vertex-disjoint GraphUnionSet; :: thesis: for G being GraphUnion of S st G is connected holds
ex H being _Graph st S = {H}
let G be GraphUnion of S; :: thesis: ( G is connected implies ex H being _Graph st S = {H} )
assume A1: G is connected ; :: thesis: ex H being _Graph st S = {H}
set v = the Vertex of G;
the_Vertices_of G = union (the_Vertices_of S) by GLIB_014:def 25;
then consider X being set such that
A2: ( the Vertex of G in X & X in the_Vertices_of S ) by TARSKI:def 4;
consider H being _Graph such that
A3: ( H in S & X = the_Vertices_of H ) by A2, GLIB_014:def 14;
take H ; :: thesis: S = {H}

now :: thesis: for x being object st x in the_Vertices_of G holds
x in the_Vertices_of H

let x be object ; :: thesis: ( x in the_Vertices_of G implies x in the_Vertices_of H )
assume x in the_Vertices_of G ; :: thesis: x in the_Vertices_of H
then reconsider w = x as Vertex of G ;
consider W being Walk of G such that
A4: W is_Walk_from the Vertex of G,w by A1, GLIB_002:def 1;
consider H9 being Element of S such that
A5: W is Walk of H9 by Th58;
reconsider W9 = W as Walk of H9 by A5;
W9 is_Walk_from the Vertex of G,w by A4, GLIB_001:19;
then A6: ( the Vertex of G is Vertex of H9 & w is Vertex of H9 ) by GLIB_001:18;
then the_Vertices_of H meets the_Vertices_of H9 by A2, A3, XBOOLE_0:3;
then H = H9 by A3, Def18;
hence x in the_Vertices_of H by A6; :: thesis: verum

end;

then A7: the_Vertices_of G c= the_Vertices_of H by TARSKI:def 3;

now :: thesis: for Y being object st Y in S holds
Y in {H}

let Y be object ; :: thesis: ( Y in S implies Y in {H} )
assume Y in S ; :: thesis: Y in {H}
then reconsider H9 = Y as Element of S ;
set w = the Vertex of H9;
H9 is Subgraph of G by GLIB_014:21;
then the_Vertices_of H9 c= the_Vertices_of G by GLIB_000:def 32;
then the Vertex of H9 in the_Vertices_of G by TARSKI:def 3;
then the_Vertices_of H meets the_Vertices_of H9 by A7, XBOOLE_0:3;
then Y = H by A3, Def18;
hence Y in {H} by TARSKI:def 1; :: thesis: verum

end;

hence S = {H} by TARSKI:def 3, ZFMISC_1:33; :: thesis: verum