let G be non-Dmulti _Graph; :: thesis: createGraph ((the_Vertices_of G),(VertexDomRel G)) is G -Disomorphic
set G9 = createGraph ((the_Vertices_of G),(VertexDomRel G));
consider F being PGraphMapping of G, createGraph ((the_Vertices_of G),(VertexDomRel G)) such that
A1: F is Disomorphism and
( F _V = id (the_Vertices_of G) & ( for e being object st e in the_Edges_of G holds
(F _E) . e = [((the_Source_of G) . e),((the_Target_of G) . e)] ) ) by Th86;
thus createGraph ((the_Vertices_of G),(VertexDomRel G)) is G -Disomorphic by A1, GLIB_010:def 24; :: thesis: verum