let G be non edgeless _Graph; :: thesis: for e being Edge of G
for H being inducedSubgraph of G,{((the_Source_of G) . e),((the_Target_of G) . e)},{e} holds H == createGraph e
let e be Edge of G; :: thesis: for H being inducedSubgraph of G,{((the_Source_of G) . e),((the_Target_of G) . e)},{e} holds H == createGraph e
set V = {((the_Source_of G) . e),((the_Target_of G) . e)};
let H be inducedSubgraph of G,{((the_Source_of G) . e),((the_Target_of G) . e)},{e}; :: thesis: H == createGraph e
( (the_Source_of G) . e in {((the_Source_of G) . e),((the_Target_of G) . e)} & (the_Target_of G) . e in {((the_Source_of G) . e),((the_Target_of G) . e)} ) by TARSKI:def 2;
then A1: {e} c= G .edgesBetween {((the_Source_of G) . e),((the_Target_of G) . e)} by ZFMISC_1:31, GLIB_000:31;
( the_Vertices_of H = {((the_Source_of G) . e),((the_Target_of G) . e)} & the_Edges_of H = {e} ) by A1, GLIB_000:def 37;
then ( the_Vertices_of H = the_Vertices_of (createGraph e) & the_Edges_of H = the_Edges_of (createGraph e) ) by Th13;
hence H == createGraph e by GLIB_000:86; :: thesis: verum