theorem :: GLIB_012:32

for G3, G4 being _Graph
for V being set
for G1 being addLoops of G3,V
for G2 being addLoops of G4,V st G3 == G4 holds
G2 is G1 -Disomorphic