consider f being ManySortedSet of the_Edges_of G such that
A1: G . ELabelSelector = f by Def1;
thus the_ELabel_of G is ManySortedSet of the_Edges_of G by A1, GLIB_003:def 8; :: thesis: verum