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

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