let G be non edgeless _Graph; :: thesis: for e being Edge of G holds
( the_Edges_of (createGraph e) = {e} & the_Vertices_of (createGraph e) = {((the_Source_of G) . e),((the_Target_of G) . e)} )
let e be Edge of G; :: thesis: ( the_Edges_of (createGraph e) = {e} & the_Vertices_of (createGraph e) = {((the_Source_of G) . e),((the_Target_of G) . e)} )
consider V being non empty Subset of (the_Vertices_of G), S, T being Function of {e},V such that
A1: ( createGraph e = 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) ) by Def4;
thus ( the_Edges_of (createGraph e) = {e} & the_Vertices_of (createGraph e) = {((the_Source_of G) . e),((the_Target_of G) . e)} ) by A1; :: thesis: verum