let G2 be _Graph; :: thesis: for v1, e, v2 being object
for G1 being addEdge of G2,v1,e,v2 st v1 <> v2 holds
G1 .loops() = G2 .loops()
let v1, e, v2 be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2 st v1 <> v2 holds
G1 .loops() = G2 .loops()
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( v1 <> v2 implies G1 .loops() = G2 .loops() )
assume A1: v1 <> v2 ; :: thesis: G1 .loops() = G2 .loops()

per cases ( not v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 or ( v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ) ;

suppose ( not v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) ; :: thesis: G1 .loops() = G2 .loops()

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

end;

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

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

now :: thesis: for e0 being object st e0 in G1 .loops() holds
e0 in G2 .loops()

let e0 be object ; :: thesis: ( e0 in G1 .loops() implies e0 in G2 .loops() )
assume e0 in G1 .loops() ; :: thesis: e0 in G2 .loops()
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: contradiction
then ( v1 = w & v2 = w ) by A2, A4, GLIB_006:107;
hence contradiction by A1; :: thesis: verum

end;

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

end;

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

end;

end;