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