let G2 be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V holds G1 .loops() = G2 .loops()
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexAll of G2,v,V holds G1 .loops() = G2 .loops()
let V be set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V holds G1 .loops() = G2 .loops()
let G1 be addAdjVertexAll of G2,v,V; :: thesis: G1 .loops() = G2 .loops()

per cases ( ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) or not V c= the_Vertices_of G2 or v in the_Vertices_of G2 ) ;

suppose A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: G1 .loops() = G2 .loops()

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

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

let e be object ; :: thesis: ( e in G1 .loops() implies e in G2 .loops() )
assume e in G1 .loops() ; :: thesis: e in G2 .loops()
then consider w being object such that
A3: e Joins w,w,G1 by Def2;
v <> w by A1, A3, GLIB_007:def 4;
then e Joins w,w,G2 by A1, A3, GLIB_007:49;
hence e in G2 .loops() by Def2; :: thesis: verum

end;

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

end;

suppose ( not V c= the_Vertices_of G2 or v in the_Vertices_of G2 ) ; :: thesis: G1 .loops() = G2 .loops()

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

end;

end;