:: deftheorem defines the_Ordering_of GLIB_010:def 7 :
for G being [Ordered] _Graph holds the_Ordering_of G = G . OrderingSelector;