theorem Th5: :: GLIB_012:5

for G2 being loopfull _Graph
for G1 being Supergraph of G2 st the_Vertices_of G1 = the_Vertices_of G2 holds
G1 is loopfull