let G be non edgeless _Graph; :: thesis:
let H be removeLoops of G; :: thesis:
let S be GraphUnionSet; :: thesis:
let G9 be GraphUnion of S; :: thesis:
assume that
A1: for v being Vertex of G ex H9 being Element of S st v in the_Vertices_of H9 and
A2: for e being Edge of G st not e in G .loops() holds
ex H9 being Element of S st createGraph e is Subgraph of H9 ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in the_Vertices_of H ; :: thesis:
then consider H9 being Element of S such that
A3: x in the_Vertices_of H9 by A1;
H9 is Subgraph of G9 by GLIB_014:21;
then the_Vertices_of H9 c= the_Vertices_of G9 by GLIB_000:def 32;
hence x in the_Vertices_of G9 by A3; :: thesis:

end;

then A4: the_Vertices_of H c= the_Vertices_of G9 by TARSKI:def 3;

now :: thesis:

let x be object ; :: thesis:
assume x in the_Edges_of H ; :: thesis:
then x in (the_Edges_of G) \ (G .loops()) by GLIB_000:53;
then A5: ( x in the_Edges_of G & not x in G .loops() ) by XBOOLE_0:def 5;
then reconsider e = x as Edge of G ;
consider H9 being Element of S such that
A6: createGraph e is Subgraph of H9 by A2, A5;
H9 is Subgraph of G9 by GLIB_014:21;
then createGraph e is Subgraph of G9 by A6, GLIB_000:43;
then the_Edges_of (createGraph e) c= the_Edges_of G9 by GLIB_000:def 32;
then {e} c= the_Edges_of G9 by Th13;
hence x in the_Edges_of G9 by ZFMISC_1:31; :: thesis:

end;

then A7: the_Edges_of H c= the_Edges_of G9 by TARSKI:def 3;

now :: thesis:

let e0 be set ; :: thesis:
assume e0 in the_Edges_of H ; :: thesis:
then e0 in (the_Edges_of G) \ (G .loops()) by GLIB_000:53;
then A8: ( e0 in the_Edges_of G & not e0 in G .loops() ) by XBOOLE_0:def 5;
then reconsider e = e0 as Edge of G ;
consider H9 being Element of S such that
A9: createGraph e is Subgraph of H9 by A2, A8;
H9 is Subgraph of G9 by GLIB_014:21;
then A10: createGraph e is Subgraph of G9 by A9, GLIB_000:43;
the_Edges_of (createGraph e) = {e} by Th13;
then A11: e0 in the_Edges_of (createGraph e) by TARSKI:def 1;
then A12: ( (the_Source_of (createGraph e)) . e0 = (the_Source_of G9) . e0 & (the_Target_of (createGraph e)) . e0 = (the_Target_of G9) . e0 ) by A10, GLIB_000:def 32;
createGraph e is Subgraph of H by A8, Th26;
hence ( (the_Source_of H) . e0 = (the_Source_of G9) . e0 & (the_Target_of H) . e0 = (the_Target_of G9) . e0 ) by A11, A12, GLIB_000:def 32; :: thesis:

end;

hence H is Subgraph of G9 by A4, A7, GLIB_000:def 32; :: thesis: