let G be _Graph; :: thesis: ( G is vlabel-full implies G is [VLabeled] )

assume A3: G is vlabel-full ; :: thesis: G is [VLabeled]

then consider f being ManySortedSet of the_Vertices_of G such that

A4: G . VLabelSelector = f ;

dom f = the_Vertices_of G by PARTFUN1:def 2;

hence G is [VLabeled] by A3, A4, GLIB_003:def 6; :: thesis: verum

assume A3: G is vlabel-full ; :: thesis: G is [VLabeled]

then consider f being ManySortedSet of the_Vertices_of G such that

A4: G . VLabelSelector = f ;

dom f = the_Vertices_of G by PARTFUN1:def 2;

hence G is [VLabeled] by A3, A4, GLIB_003:def 6; :: thesis: verum