theorem :: GLIBPRE0:51

for G2 being _Graph
for v being object
for G1 being addVertex of G2,v holds G1 is addAdjVertexAll of G2,v, {}