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;

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

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}

then
G1 .loops() c= (G2 .loops()) \/ {e}
by TARSKI:def 3;e0 in (G2 .loops()) \/ {e}

let e0 be object ; :: thesis: ( e0 in G1 .loops() implies b_{1} in (G2 .loops()) \/ {e} )

assume e0 in G1 .loops() ; :: thesis: b_{1} in (G2 .loops()) \/ {e}

then consider w being object such that

A4: e0 Joins w,w,G1 by Def2;

end;assume e0 in G1 .loops() ; :: thesis: b

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

end;

suppose
e0 in the_Edges_of G2
; :: thesis: b_{1} 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;then e0 in G2 .loops() by Def2;

hence e0 in (G2 .loops()) \/ {e} by XBOOLE_0:def 3; :: thesis: verum

suppose
not e0 in the_Edges_of G2
; :: thesis: b_{1} 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;then e0 in {e} by TARSKI:def 1;

hence e0 in (G2 .loops()) \/ {e} by XBOOLE_0:def 3; :: thesis: verum

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