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()

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

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

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()

then A2:
G1 .loops() c= G2 .loops()
by TARSKI:def 3;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;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

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

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