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

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