theorem Th48: :: GLIB_009:48

for G1 being _Graph
for G2 being Subgraph of G1 holds G2 .loops() c= G1 .loops()