let G2 be _Graph; :: thesis: for G1 being Supergraph of G2 holds G2 .loops() c= G1 .loops()
let G1 be Supergraph of G2; :: thesis: G2 .loops() c= G1 .loops()
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 .loops() c= G1 .loops() by Th48; :: thesis: verum