theorem Th86: :: GLUNIR00:86

for G being non-Dmulti _Graph ex F being PGraphMapping of G, createGraph ((the_Vertices_of G),(VertexDomRel G)) st
( F is Disomorphism & 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)] ) )