theorem :: GLIBPRE1:78

for G1 being _Graph
for G2 being DSimpleGraph of G1
for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff v2,w2 are_adjacent )