theorem :: GLIB_011:24

for G1, G2 being _Graph
for F being semi-continuous PGraphMapping of G1,G2 st F is total & F is onto holds
F _V is continuous PVertexMapping of G1,G2