let G2 be _Graph; :: thesis: for v being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,v st not e in the_Edges_of G2 holds
G1 .loops() = (G2 .loops()) \/ {e}
let v be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v,e,v st not e in the_Edges_of G2 holds
G1 .loops() = (G2 .loops()) \/ {e}
let e be object ; :: thesis: for G1 being addEdge of G2,v,e,v st not e in the_Edges_of G2 holds
G1 .loops() = (G2 .loops()) \/ {e}
let G1 be addEdge of G2,v,e,v; :: thesis: ( not e in the_Edges_of G2 implies G1 .loops() = (G2 .loops()) \/ {e} )
assume A1: not e in the_Edges_of G2 ; :: thesis: G1 .loops() = (G2 .loops()) \/ {e}
then e in G1 .loops() by Th45, GLIB_006:105;
then A2: {e} c= G1 .loops() by ZFMISC_1:31;
G2 .loops() c= G1 .loops() by Th49;
then A3: (G2 .loops()) \/ {e} c= G1 .loops() by A2, XBOOLE_1:8;

now :: thesis: for e0 being object st e0 in G1 .loops() holds
e0 in (G2 .loops()) \/ {e}

let e0 be object ; :: thesis: ( e0 in G1 .loops() implies b₁ in (G2 .loops()) \/ {e} )
assume e0 in G1 .loops() ; :: thesis: b₁ in (G2 .loops()) \/ {e}
then consider w being object such that
A4: e0 Joins w,w,G1 by Def2;

per cases ( e0 in the_Edges_of G2 or not e0 in the_Edges_of G2 ) ;

suppose e0 in the_Edges_of G2 ; :: thesis: b₁ in (G2 .loops()) \/ {e}

then e0 Joins w,w,G2 by A4, GLIB_006:72;
then e0 in G2 .loops() by Def2;
hence e0 in (G2 .loops()) \/ {e} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose not e0 in the_Edges_of G2 ; :: thesis: b₁ in (G2 .loops()) \/ {e}

then e = e0 by A1, A4, GLIB_006:106;
then e0 in {e} by TARSKI:def 1;
hence e0 in (G2 .loops()) \/ {e} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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