set G0 = G .set (OrderingSelector,X);

VLabelSelector in dom G by Def2;

then VLabelSelector in (dom G) \/ {OrderingSelector} by XBOOLE_0:def 3;

hence VLabelSelector in dom (G .set (OrderingSelector,X)) by GLIB_000:7; :: according to GLIB_010:def 2 :: thesis: ex f being ManySortedSet of the_Vertices_of (G .set (OrderingSelector,X)) st (G .set (OrderingSelector,X)) . VLabelSelector = f

consider f being ManySortedSet of the_Vertices_of G such that

A1: G . VLabelSelector = f by Def2;

G == G .set (OrderingSelector,X) by Th3;

then the_Vertices_of G = the_Vertices_of (G .set (OrderingSelector,X)) by GLIB_000:def 34;

then reconsider f = f as ManySortedSet of the_Vertices_of (G .set (OrderingSelector,X)) ;

take f ; :: thesis: (G .set (OrderingSelector,X)) . VLabelSelector = f

OrderingSelector <> VLabelSelector by GLIB_003:def 3;

hence (G .set (OrderingSelector,X)) . VLabelSelector = f by A1, GLIB_000:9; :: thesis: verum

VLabelSelector in dom G by Def2;

then VLabelSelector in (dom G) \/ {OrderingSelector} by XBOOLE_0:def 3;

hence VLabelSelector in dom (G .set (OrderingSelector,X)) by GLIB_000:7; :: according to GLIB_010:def 2 :: thesis: ex f being ManySortedSet of the_Vertices_of (G .set (OrderingSelector,X)) st (G .set (OrderingSelector,X)) . VLabelSelector = f

consider f being ManySortedSet of the_Vertices_of G such that

A1: G . VLabelSelector = f by Def2;

G == G .set (OrderingSelector,X) by Th3;

then the_Vertices_of G = the_Vertices_of (G .set (OrderingSelector,X)) by GLIB_000:def 34;

then reconsider f = f as ManySortedSet of the_Vertices_of (G .set (OrderingSelector,X)) ;

take f ; :: thesis: (G .set (OrderingSelector,X)) . VLabelSelector = f

OrderingSelector <> VLabelSelector by GLIB_003:def 3;

hence (G .set (OrderingSelector,X)) . VLabelSelector = f by A1, GLIB_000:9; :: thesis: verum