:: deftheorem Def8 defines the_Vertices_of GLIB_015:def 8 :
for F being non empty Graph-yielding Function
for b₂ being Function holds
( b₂ = the_Vertices_of F iff ( dom b₂ = dom F & ( for x being Element of dom F holds b₂ . x = the_Vertices_of (F . x) ) ) );