theorem :: GLIB_012:30

for G3 being _Graph
for G4 being b₁ -isomorphic _Graph
for G1 being addLoops of G3
for G2 being addLoops of G4 holds G2 is G1 -isomorphic