let G be _Graph; :: thesis: id (the_Vertices_of G) is isomorphism Disomorphism PVertexMapping of G,G
reconsider f = id (the_Vertices_of G) as PVertexMapping of G,G by Th5;
f is Disomorphism ;
hence id (the_Vertices_of G) is isomorphism Disomorphism PVertexMapping of G,G ; :: thesis: verum