for G being _Graph
for v being Vertex of G holds
( v in Endvertices G iff v is endvertex )