:: deftheorem Def5 defines AP:VLabeling GLIB_005:def 5 :
for G being _Graph
for EL being FF:ELabeling of G
for b₃ being PartFunc of (the_Vertices_of G),({1} \/ (the_Edges_of G)) holds
( b₃ is AP:VLabeling of EL iff verum );