reconsider f = id (the_Vertices_of G) as PVertexMapping of G,G by Th5;
take f ; :: thesis: ( f is Disomorphism & f is isomorphism )
thus f is Disomorphism ; :: thesis: f is isomorphism
thus f is isomorphism ; :: thesis: verum