let G be 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 ) 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 ) 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 ) implies G is Subgraph of G9 )
assume A1: for v being Vertex of G ex H9 being Element of S st v in the_Vertices_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
A2: 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 A2; :: thesis: verum

end;

hence G is Subgraph of G9 by TARSKI:def 3, GLIBPRE1:68; :: thesis: verum