let G be non edgeless _Graph; :: thesis: for e being Edge of G
for V being Subset of (the_Vertices_of G)
for H being addVertices of createGraph e,V holds H is Subgraph of G
let e be Edge of G; :: thesis: for V being Subset of (the_Vertices_of G)
for H being addVertices of createGraph e,V holds H is Subgraph of G
let V be Subset of (the_Vertices_of G); :: thesis: for H being addVertices of createGraph e,V holds H is Subgraph of G
let H be addVertices of createGraph e,V; :: thesis: H is Subgraph of G
the_Vertices_of H = (the_Vertices_of (createGraph e)) \/ V by GLIB_006:def 10;
then A1: the_Vertices_of H c= the_Vertices_of G ;
the_Edges_of H = the_Edges_of (createGraph e) by GLIB_006:def 10;
then A2: the_Edges_of H c= the_Edges_of G ;

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

let e0 be set ; :: thesis: ( e0 in the_Edges_of H implies ( (the_Source_of H) . e0 = (the_Source_of G) . e0 & (the_Target_of H) . e0 = (the_Target_of G) . e0 ) )
assume e0 in the_Edges_of H ; :: thesis: ( (the_Source_of H) . e0 = (the_Source_of G) . e0 & (the_Target_of H) . e0 = (the_Target_of G) . e0 )
then A3: e0 in the_Edges_of (createGraph e) by GLIB_006:def 10;
thus (the_Source_of H) . e0 = (the_Source_of (createGraph e)) . e0 by GLIB_006:def 10
.= (the_Source_of G) . e0 by A3, GLIB_000:def 32 ; :: thesis: (the_Target_of H) . e0 = (the_Target_of G) . e0
thus (the_Target_of H) . e0 = (the_Target_of (createGraph e)) . e0 by GLIB_006:def 10
.= (the_Target_of G) . e0 by A3, GLIB_000:def 32 ; :: thesis: verum

end;

hence H is Subgraph of G by A1, A2, GLIB_000:def 32; :: thesis: verum