:: deftheorem Def23 defines -isomorphic GLIB_010:def 23 :
for G1, G2 being _Graph holds
( G2 is G1 -isomorphic iff ex F being PGraphMapping of G1,G2 st F is isomorphism );