let G be _Graph; :: thesis: (id G) " = id G
thus (id G) " = [(id (the_Vertices_of G)),((id (the_Edges_of G)) ")] by FUNCT_1:45
.= id G by FUNCT_1:45 ; :: thesis: verum