let G2 be _Graph; :: thesis:
let v1, e, v2 be object ; :: thesis:
let G1 be addEdge of G2,v1,e,v2; :: thesis:
assume A1: v1 <> v2 ; :: thesis:

per cases ;

suppose ( not v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) ; :: thesis:

then G1 == G2 by GLIB_006:def 11;
hence G1 .loops() = G2 .loops() by Th50; :: thesis:

end;

suppose A2: ( v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis:

A3: G2 .loops() c= G1 .loops() by Th49;

now :: thesis:

let e0 be object ; :: thesis:
assume e0 in G1 .loops() ; :: thesis:
then consider w being object such that
A4: e0 Joins w,w,G1 by Def2;
e0 in the_Edges_of G2

proof

assume not e0 in the_Edges_of G2 ; :: thesis:
then ( v1 = w & v2 = w ) by A2, A4, GLIB_006:107;
hence contradiction by A1; :: thesis:

end;

then e0 Joins w,w,G2 by A4, GLIB_006:72;
hence e0 in G2 .loops() by Def2; :: thesis:

end;

then G1 .loops() c= G2 .loops() by TARSKI:def 3;
hence G1 .loops() = G2 .loops() by A3, XBOOLE_0:def 10; :: thesis:

end;

end;