let G be non edgeless _Graph; :: thesis: for S being GraphUnionSet
for G9 being GraphUnion of S st ( for v being Vertex of G ex H9 being Element of S st v in the_Vertices_of H9 ) & ( for e being Edge of G ex H9 being Element of S st createGraph e is Subgraph of H9 ) holds
G is Subgraph of G9
let S be GraphUnionSet; :: thesis: for G9 being GraphUnion of S st ( for v being Vertex of G ex H9 being Element of S st v in the_Vertices_of H9 ) & ( for e being Edge of G ex H9 being Element of S st createGraph e is Subgraph of H9 ) holds
G is Subgraph of G9
let G9 be GraphUnion of S; :: thesis: ( ( for v being Vertex of G ex H9 being Element of S st v in the_Vertices_of H9 ) & ( for e being Edge of G ex H9 being Element of S st createGraph e is Subgraph of H9 ) implies G is Subgraph of G9 )
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 ex H9 being Element of S st createGraph e is Subgraph of H9 ; :: thesis: G is Subgraph of G9

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

let x be object ; :: thesis: ( x in the_Vertices_of G implies x in the_Vertices_of G9 )
assume x in the_Vertices_of G ; :: thesis: x in the_Vertices_of G9
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: verum

end;

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

now :: thesis: for x being object st x in the_Edges_of G holds
x in the_Edges_of G9

let x be object ; :: thesis: ( x in the_Edges_of G implies x in the_Edges_of G9 )
assume x in the_Edges_of G ; :: thesis: x in the_Edges_of G9
then reconsider e = x as Edge of G ;
consider H9 being Element of S such that
A5: createGraph e is Subgraph of H9 by A2;
H9 is Subgraph of G9 by GLIB_014:21;
then createGraph e is Subgraph of G9 by A5, 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: verum

end;

then A6: the_Edges_of G c= the_Edges_of G9 by TARSKI:def 3;

now :: thesis: for e0 being set st e0 in the_Edges_of G holds
( (the_Source_of G) . e0 = (the_Source_of G9) . e0 & (the_Target_of G) . e0 = (the_Target_of G9) . e0 )

let e0 be set ; :: thesis: ( e0 in the_Edges_of G implies ( (the_Source_of G) . e0 = (the_Source_of G9) . e0 & (the_Target_of G) . e0 = (the_Target_of G9) . e0 ) )
assume e0 in the_Edges_of G ; :: thesis: ( (the_Source_of G) . e0 = (the_Source_of G9) . e0 & (the_Target_of G) . e0 = (the_Target_of G9) . e0 )
then reconsider e = e0 as Edge of G ;
consider H9 being Element of S such that
A7: createGraph e is Subgraph of H9 by A2;
H9 is Subgraph of G9 by GLIB_014:21;
then A8: createGraph e is Subgraph of G9 by A7, GLIB_000:43;
the_Edges_of (createGraph e) = {e} by Th13;
then A9: e0 in the_Edges_of (createGraph e) by TARSKI:def 1;
then ( (the_Source_of (createGraph e)) . e0 = (the_Source_of G9) . e0 & (the_Target_of (createGraph e)) . e0 = (the_Target_of G9) . e0 ) by A8, GLIB_000:def 32;
hence ( (the_Source_of G) . e0 = (the_Source_of G9) . e0 & (the_Target_of G) . e0 = (the_Target_of G9) . e0 ) by A9, GLIB_000:def 32; :: thesis: verum

end;

hence G is Subgraph of G9 by A4, A6, GLIB_000:def 32; :: thesis: verum