:: deftheorem defines invertible GLIB_011:def 9 :
for G1, G2 being _Graph
for f being PVertexMapping of G1,G2 holds
( f is invertible iff ( f is one-to-one & f is continuous ) );