let G be _Graph; :: thesis: G is GraphUnion of G .allComponents()
set G9 = the GraphUnion of G .allComponents() ;
G is GraphUnion of G .allSG() by Th35;
then A1: the GraphUnion of G .allComponents() is Subgraph of G by GLIBPRE1:119;

A2: now :: thesis: for v being Vertex of G ex H9 being Element of G .allComponents() st v in the_Vertices_of H9

let v be Vertex of G; :: thesis: ex H9 being Element of G .allComponents() st v in the_Vertices_of H9
set H9 = the plain inducedSubgraph of G,(G .reachableFrom v);
reconsider H9 = the plain inducedSubgraph of G,(G .reachableFrom v) as Element of G .allComponents() by Th189;
take H9 = H9; :: thesis: v in the_Vertices_of H9
the_Vertices_of H9 = G .reachableFrom v by GLIB_000:def 37;
hence v in the_Vertices_of H9 by GLIB_002:9; :: thesis: verum

end;

now :: thesis: G is Subgraph of the GraphUnion of G .allComponents()

per cases ( G is edgeless or not G is edgeless ) ;

suppose G is edgeless ; :: thesis: G is Subgraph of the GraphUnion of G .allComponents()

hence G is Subgraph of the GraphUnion of G .allComponents() by A2, Th22; :: thesis: verum

end;

suppose not G is edgeless ; :: thesis: G is Subgraph of the GraphUnion of G .allComponents()

then reconsider G0 = G as non edgeless _Graph ;

now :: thesis: for e being Edge of G0 ex H9 being Element of G .allComponents() st createGraph e is Subgraph of H9

let e be Edge of G0; :: thesis: ex H9 being Element of G .allComponents() st createGraph e is Subgraph of H9
set v = (the_Source_of G) . e;
set w = (the_Target_of G) . e;
e DJoins (the_Source_of G) . e,(the_Target_of G) . e, createGraph e by Th14;
then e Joins (the_Source_of G) . e,(the_Target_of G) . e, createGraph e by GLIB_000:16;
then A3: e Joins (the_Source_of G) . e,(the_Target_of G) . e,G by GLIB_000:72;
then reconsider v = (the_Source_of G) . e, w = (the_Target_of G) . e as Vertex of G by GLIB_000:13;
set H9 = the plain inducedSubgraph of G,(G .reachableFrom v);
reconsider H9 = the plain inducedSubgraph of G,(G .reachableFrom v) as Element of G .allComponents() by Th189;
take H9 = H9; :: thesis: createGraph e is Subgraph of H9
A4: the_Vertices_of H9 = G .reachableFrom v by GLIB_000:def 37;
then A5: v in the_Vertices_of H9 by GLIB_002:9;
then A6: w in the_Vertices_of H9 by A3, A4, GLIB_002:10;
then e in G .edgesBetween (the_Vertices_of H9) by A3, A5, GLIB_000:32;
then e in the_Edges_of H9 by A4, GLIB_000:def 37;
then {e} c= the_Edges_of H9 by ZFMISC_1:31;
then A7: the_Edges_of (createGraph e) c= the_Edges_of H9 by Th13;
{v,w} c= the_Vertices_of H9 by A5, A6, ZFMISC_1:32;
then the_Vertices_of (createGraph e) c= the_Vertices_of H9 by Th13;
hence createGraph e is Subgraph of H9 by A7, GLIB_000:44; :: thesis: verum

end;

hence G is Subgraph of the GraphUnion of G .allComponents() by A2, Th23; :: thesis: verum

end;

end;

end;

hence G is GraphUnion of G .allComponents() by A1, GLIB_000:87, GLIB_014:22; :: thesis: verum