let G be _Graph; :: thesis: G is GraphUnion of G .allInducedSG()
set G9 = the GraphUnion of G .allInducedSG() ;
set G8 = the GraphUnion of {G};
G | _GraphSelectors in G .allInducedSG() by Th47;
then A1: G | _GraphSelectors is Subgraph of the GraphUnion of G .allInducedSG() by GLIB_014:21;
G == G | _GraphSelectors by GLIB_000:128;
then A2: G is Subgraph of the GraphUnion of G .allInducedSG() by A1, GLIB_000:92;

now :: thesis: for H2 being Element of G .allInducedSG() ex H1 being Element of {G} st H2 is Subgraph of H1

let H2 be Element of G .allInducedSG() ; :: thesis: ex H1 being Element of {G} st H2 is Subgraph of H1
reconsider H1 = G as Element of {G} by TARSKI:def 1;
take H1 = H1; :: thesis: H2 is Subgraph of H1
thus H2 is Subgraph of H1 ; :: thesis: verum

end;

then the GraphUnion of G .allInducedSG() is Subgraph of the GraphUnion of {G} by GLIBPRE1:118;
then the GraphUnion of G .allInducedSG() is Subgraph of G by GLIB_000:91, GLIB_014:24;
hence G is GraphUnion of G .allInducedSG() by A2, GLIB_000:87, GLIB_014:22; :: thesis: verum