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

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