:: deftheorem Def6 defines [Ordered] GLIB_010:def 6 :
for G being GraphStruct holds
( G is [Ordered] iff ( OrderingSelector in dom G & G . OrderingSelector is Enumeration of (the_Vertices_of G) ) );