theorem :: GLIB_011:3

for G1, G2 being _Graph
for f being PVertexMapping of G1,G2 holds
( f is continuous iff for v, w being Vertex of G1 st v in dom f & w in dom f holds
( v,w are_adjacent iff f /. v,f /. w are_adjacent ) ) by Def1;