theorem :: GLIB_006:93

for G2 being _Graph
for v being object
for G1 being addVertex of G2,v holds
( G1 == G2 iff v in the_Vertices_of G2 ) by Th82, ZFMISC_1:31;