theorem :: GLIB_012:19
for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds G1 .order() = G2 .order() by Th15;