for G being _Graph
for v, w being Vertex of G
for e being object
for H being addEdge of G,v,e,w st v,w are_adjacent holds
VertexAdjSymRel H = VertexAdjSymRel G