theorem Th84: :: GLIB_010:84

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 .order() = G2 .order() & G1 .size() = G2 .size() )