let G be non edgeless _Graph; :: thesis: for S being GraphUnionSet
for G9 being GraphUnion of S st ( for v being Vertex of G holds createGraph v in S ) & ( for e being Edge of G holds createGraph e in S ) holds
G is Subgraph of G9
let S be GraphUnionSet; :: thesis: for G9 being GraphUnion of S st ( for v being Vertex of G holds createGraph v in S ) & ( for e being Edge of G holds createGraph e in S ) holds
G is Subgraph of G9
let G9 be GraphUnion of S; :: thesis: ( ( for v being Vertex of G holds createGraph v in S ) & ( for e being Edge of G holds createGraph e in S ) implies G is Subgraph of G9 )
assume that
A1: for v being Vertex of G holds createGraph v in S and
A2: for e being Edge of G holds createGraph e in S ; :: thesis: G is Subgraph of G9

A3: now :: thesis: for v being Vertex of G ex H9 being Element of S st v in the_Vertices_of H9

let v be Vertex of G; :: thesis: ex H9 being Element of S st v in the_Vertices_of H9
reconsider H9 = createGraph v as Element of S by A1;
take H9 = H9; :: thesis: v in the_Vertices_of H9
thus v in the_Vertices_of H9 by ZFMISC_1:31; :: thesis: verum

end;

now :: thesis: for e being Edge of G ex H9 being Element of S st createGraph e is Subgraph of H9

let e be Edge of G; :: thesis: ex H9 being Element of S st createGraph e is Subgraph of H9
reconsider H9 = createGraph e as Element of S by A2;
take H9 = H9; :: thesis: createGraph e is Subgraph of H9
thus createGraph e is Subgraph of H9 by GLIB_000:40; :: thesis: verum

end;

hence G is Subgraph of G9 by A3, Th23; :: thesis: verum