let G1, G2 be _Graph; :: thesis: for V being non empty Subset of (the_Vertices_of G1) st V c= the_Vertices_of G2 holds
createGraph V is Subgraph of G2
let V be non empty Subset of (the_Vertices_of G1); :: thesis: ( V c= the_Vertices_of G2 implies createGraph V is Subgraph of G2 )
assume A1: V c= the_Vertices_of G2 ; :: thesis: createGraph V is Subgraph of G2
for e being set st e in the_Edges_of (createGraph V) holds
( (the_Source_of (createGraph V)) . e = (the_Source_of G2) . e & (the_Target_of (createGraph V)) . e = (the_Target_of G2) . e ) ;
hence createGraph V is Subgraph of G2 by A1, XBOOLE_1:2, GLIB_000:def 32; :: thesis: verum