set v = (the_Source_of G) . e;
set w = (the_Target_of G) . e;
reconsider V = {((the_Source_of G) . e),((the_Target_of G) . e)} as non empty Subset of (the_Vertices_of G) ;
set S = e .--> ((the_Source_of G) . e);
set T = e .--> ((the_Target_of G) . e);
( dom (e .--> ((the_Source_of G) . e)) = dom {[e,((the_Source_of G) . e)]} & dom (e .--> ((the_Target_of G) . e)) = dom {[e,((the_Target_of G) . e)]} ) by FUNCT_4:82;
then A1: ( dom (e .--> ((the_Source_of G) . e)) = {e} & dom (e .--> ((the_Target_of G) . e)) = {e} ) by RELAT_1:9;
( rng (e .--> ((the_Source_of G) . e)) = {((the_Source_of G) . e)} & rng (e .--> ((the_Target_of G) . e)) = {((the_Target_of G) . e)} ) by FUNCOP_1:88;
then reconsider S = e .--> ((the_Source_of G) . e), T = e .--> ((the_Target_of G) . e) as Function of {e},V by A1, ZFMISC_1:7, FUNCT_2:2;
set H = createGraph (V,{e},S,T);

now :: thesis:

thus ( the_Vertices_of (createGraph (V,{e},S,T)) c= the_Vertices_of G & the_Edges_of (createGraph (V,{e},S,T)) c= the_Edges_of G ) ; :: thesis:
let e0 be set ; :: thesis:
assume e0 in the_Edges_of (createGraph (V,{e},S,T)) ; :: thesis:
then A2: e0 = e by TARSKI:def 1;
thus (the_Source_of (createGraph (V,{e},S,T))) . e0 = (the_Source_of G) . e0 by A2, FUNCOP_1:72; :: thesis:
thus (the_Target_of (createGraph (V,{e},S,T))) . e0 = (the_Target_of G) . e0 by A2, FUNCOP_1:72; :: thesis:

end;

then reconsider H = createGraph (V,{e},S,T) as plain Subgraph of G by GLIB_000:def 32;
take H ; :: thesis:
take V ; :: thesis:
take S ; :: thesis:
take T ; :: thesis:
thus ( H = createGraph (V,{e},S,T) & {((the_Source_of G) . e),((the_Target_of G) . e)} = V & S = e .--> ((the_Source_of G) . e) & T = e .--> ((the_Target_of G) . e) ) ; :: thesis: