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

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 v being object such that
A1: e Joins v,v,G1 by Def2;
v is set by TARSKI:1;
then e Joins v,v,G2 by A1, Th41;
hence e in G2 .loops() by Def2; :: thesis: verum

end;

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