the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:def 33;
hence G2 .set (OrderingSelector,(the_Ordering_of G1)) is [Ordered] ; :: thesis: verum