:: deftheorem Def4 defines the_Vertices_of GLIB_015:def 4 :
for F being Graph-yielding Function
for b₂ being Function holds
( b₂ = the_Vertices_of F iff ( dom b₂ = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b₂ . x = the_Vertices_of G ) ) ) );