is mentioned by

Thm* t:Graph. Incidence(t) Edges(t)Vertices(t)Vertices(t)	[gr_f_wf]
Def G H == vmap:(Vertices(G)Vertices(H)), emap:(Edges(G)Edges(H)). Bij(Vertices(G); Vertices(H); vmap) & Bij(Edges(G); Edges(H); emap) & (vmap,vmap) o Incidence(G) = Incidence(H) o emap	[graph-isomorphic]
Def x-the_graph- > y == e:Edges(the_graph). Incidence(the_graph)(e) = < x,y >	[edge]

Try larger context: Graphs