let G be 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 ) 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 ) holds
G is Subgraph of G9
let G9 be GraphUnion of S; :: thesis: ( ( for v being Vertex of G holds createGraph v in S ) implies G is Subgraph of G9 )
assume A1: for v being Vertex of G holds createGraph v in S ; :: thesis: G is Subgraph of G9

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 TARSKI:def 1; :: thesis: verum

end;

hence G is Subgraph of G9 by Th22; :: thesis: verum