let G be _Graph; :: thesis: G == createGraph ((the_Vertices_of G),(the_Edges_of G),(the_Source_of G),(the_Target_of G))
set H = createGraph ((the_Vertices_of G),(the_Edges_of G),(the_Source_of G),(the_Target_of G));
( the_Vertices_of G = the_Vertices_of (createGraph ((the_Vertices_of G),(the_Edges_of G),(the_Source_of G),(the_Target_of G))) & the_Edges_of G = the_Edges_of (createGraph ((the_Vertices_of G),(the_Edges_of G),(the_Source_of G),(the_Target_of G))) & the_Source_of G = the_Source_of (createGraph ((the_Vertices_of G),(the_Edges_of G),(the_Source_of G),(the_Target_of G))) & the_Target_of G = the_Target_of (createGraph ((the_Vertices_of G),(the_Edges_of G),(the_Source_of G),(the_Target_of G))) ) ;
hence G == createGraph ((the_Vertices_of G),(the_Edges_of G),(the_Source_of G),(the_Target_of G)) by GLIB_000:def 34; :: thesis: verum