:: deftheorem defines " GLIB_010:def 33 :
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 holds F " = [((F _V) "),((F _E) ")];