let G be _Graph; :: thesis: for V being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,V, {} holds H == createGraph V
let V be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,V, {} holds H == createGraph V
let H be inducedSubgraph of G,V, {} ; :: thesis: H == createGraph V
{} c= G .edgesBetween V by XBOOLE_1:2;
then ( the_Vertices_of H = the_Vertices_of (createGraph V) & the_Edges_of H = the_Edges_of (createGraph V) ) by GLIB_000:def 37;
hence H == createGraph V by GLIB_000:86; :: thesis: verum