:: deftheorem Def14 defines the_Vertices_of GLIB_014:def 14 :
for S being Graph-membered set
for b₂ being set holds
( b₂ = the_Vertices_of S iff for V being object holds
( V in b₂ iff ex G being _Graph st
( G in S & V = the_Vertices_of G ) ) );