:: deftheorem defines Disomorphism GLIB_010:def 22 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is Disomorphism iff ( F is directed & F is total & F is one-to-one & F is onto ) );