:: deftheorem Def8 defines Endvertices GLIB_006:def 8 :
for G being _Graph
for b₂ being Subset of (the_Vertices_of G) holds
( b₂ = Endvertices G iff for v being object holds
( v in b₂ iff ex w being Vertex of G st
( v = w & w is endvertex ) ) );