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

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