consider f being ManySortedSet of the_Vertices_of G such that

A1: G . VLabelSelector = f by Def2;

thus the_VLabel_of G is ManySortedSet of the_Vertices_of G by A1, GLIB_003:def 9; :: thesis: verum

A1: G . VLabelSelector = f by Def2;

thus the_VLabel_of G is ManySortedSet of the_Vertices_of G by A1, GLIB_003:def 9; :: thesis: verum