theorem :: GLIB_013:22

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for c being Cardinal st F is isomorphism holds
( ( G1 is c -vertex implies G2 is c -vertex ) & ( G2 is c -vertex implies G1 is c -vertex ) & ( G1 is c -edge implies G2 is c -edge ) & ( G2 is c -edge implies G1 is c -edge ) ) by GLIB_010:84;