let G be _Graph; :: thesis: ( G is elabel-full implies G is [ELabeled] )
assume A1: G is elabel-full ; :: thesis: G is [ELabeled]
then consider f being ManySortedSet of the_Edges_of G such that
A2: G . ELabelSelector = f ;
dom f = the_Edges_of G by PARTFUN1:def 2;
hence G is [ELabeled] by A1, A2, GLIB_003:def 5; :: thesis: verum