let G be _Graph; :: thesis: for v being Vertex of G holds
( v in Endvertices G iff v is endvertex )
let v be Vertex of G; :: thesis: ( v in Endvertices G iff v is endvertex )

hereby :: thesis: ( v is endvertex implies v in Endvertices G )

assume v in Endvertices G ; :: thesis: v is endvertex
then consider w being Vertex of G such that
A1: ( v = w & w is endvertex ) by Def8;
thus v is endvertex by A1; :: thesis: verum

end;

thus ( v is endvertex implies v in Endvertices G ) by Def8; :: thesis: verum