:: deftheorem defines ordering-preserving GLIB_010:def 28 :
for G1, G2 being [Ordered] _Graph
for F being PGraphMapping of G1,G2 holds
( F is ordering-preserving iff (the_Ordering_of G2) * (F _V) = (the_Ordering_of G1) | (dom (F _V)) );