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

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

A2: for v being Vertex of G holds createGraph v in G .allConnectedSG() by Th127;

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

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

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

end;

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

then reconsider G0 = G as non edgeless _Graph ;
for e being Edge of G0 holds createGraph e in G .allConnectedSG() by Th128;
hence G is Subgraph of the GraphUnion of G .allConnectedSG() by A2, Th25; :: thesis: verum

end;

end;

end;

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