let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies G1 .loops() = G2 .loops() )
assume G1 == G2 ; :: thesis: G1 .loops() = G2 .loops()
then ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) by GLIB_000:87;
then ( G1 .loops() c= G2 .loops() & G2 .loops() c= G1 .loops() ) by Th48;
hence G1 .loops() = G2 .loops() by XBOOLE_0:def 10; :: thesis: verum