for G1, G2 being _Graph
for G3 being removeLoops of G1 st G1 == G2 holds
G3 is removeLoops of G2