let G be _Graph; :: thesis: for X being set holds G == G .set (OrderingSelector,X)
let X be set ; :: thesis: G == G .set (OrderingSelector,X)
set G2 = G .set (OrderingSelector,X);
( the_Vertices_of G = the_Vertices_of (G .set (OrderingSelector,X)) & the_Edges_of G = the_Edges_of (G .set (OrderingSelector,X)) & the_Source_of G = the_Source_of (G .set (OrderingSelector,X)) & the_Target_of G = the_Target_of (G .set (OrderingSelector,X)) ) by Lm1, GLIB_000:10;
hence G == G .set (OrderingSelector,X) by GLIB_000:def 34; :: thesis: verum