G,H:Graph. G H H G

Unfold `graph-isomorphic` 0
THEN
ExRepD
THEN
AllHyps (h. FwdThru Thm* f:(AB). Bij(A; B; f) (g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g)) [h])
THEN
ExRepD
THEN
InstConcl [g;g1]

1

1. G: Graph 2. H: Graph 3. vmap: Vertices(G)Vertices(H) 4. emap: Edges(G)Edges(H) 5. Bij(Vertices(G); Vertices(H); vmap) 6. Bij(Edges(G); Edges(H); emap) 7. (vmap,vmap) o Incidence(G) = Incidence(H) o emap 8. g1: Edges(H)Edges(G) 9. Bij(Edges(H); Edges(G); g1) 10. InvFuns(Edges(G); Edges(H); emap; g1) 11. g: Vertices(H)Vertices(G) 12. Bij(Vertices(H); Vertices(G); g) 13. InvFuns(Vertices(G); Vertices(H); vmap; g) (g,g) o Incidence(H) = Incidence(G) o g1

2 steps

About: