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