take id (the_Vertices_of G) ; :: thesis: ( id (the_Vertices_of G) is one-to-one & id (the_Vertices_of G) is proper )
thus ( id (the_Vertices_of G) is one-to-one & id (the_Vertices_of G) is proper ) ; :: thesis: verum