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 b1 in (G2 .loops()) \/ {e} )
assume e0 in G1 .loops() ; :: thesis: b1 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 ) ;
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