let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies ( id G1 = id G2 & id G1 is PGraphMapping of G1,G2 ) )
assume A1: G1 == G2 ; :: thesis: ( id G1 = id G2 & id G1 is PGraphMapping of G1,G2 )
thus id G1 = [(id (the_Vertices_of G2)),(id (the_Edges_of G1))] by A1, GLIB_000:def 34
.= id G2 by A1, GLIB_000:def 34 ; :: thesis: id G1 is PGraphMapping of G1,G2
thus id G1 is PGraphMapping of G1,G2 by A1, Th9; :: thesis: verum