theorem :: GLIB_010:176

for G1, G2 being loopless _trivial _Graph
for F being non empty PGraphMapping of G1,G2 holds
( F is Disomorphism & F = [( the Vertex of G1 .--> the Vertex of G2),{}] )