let G2 be _Graph; :: thesis: for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 holds G1 .loops() = G2 .loops()
let v1, e, v2 be object ; :: thesis: for G1 being addAdjVertex of G2,v1,e,v2 holds G1 .loops() = G2 .loops()
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis: G1 .loops() = G2 .loops()
A1: G2 .loops() c= G1 .loops() by Th49;

per cases ( ( v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) or ( not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) or ( ( not v1 in the_Vertices_of G2 or v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) & ( v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) ) ) ;

suppose A2: ( v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: G1 .loops() = G2 .loops()

now :: thesis: for e0 being object st e0 in G1 .loops() holds
e0 in G2 .loops()

let e0 be object ; :: thesis: ( e0 in G1 .loops() implies e0 in G2 .loops() )
assume e0 in G1 .loops() ; :: thesis: e0 in G2 .loops()
then consider w being object such that
A3: e0 Joins w,w,G1 by Def2;
e0 in the_Edges_of G2

proof

assume A4: not e0 in the_Edges_of G2 ; :: thesis: contradiction
A5: e0 in the_Edges_of G1 by A3, GLIB_000:def 13;
the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A2, GLIB_006:def 12;
then e0 in {e} by A4, A5, XBOOLE_0:def 3;
then e = e0 by TARSKI:def 1;
then e0 Joins v1,v2,G1 by A2, GLIB_006:131;
then ( v1 = w & v2 = w ) by A3, GLIB_000:15;
hence contradiction by A2; :: thesis: verum

end;

then e0 Joins w,w,G2 by A3, GLIB_006:72;
hence e0 in G2 .loops() by Def2; :: thesis: verum

end;

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

end;

suppose A6: ( not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: G1 .loops() = G2 .loops()

now :: thesis: for e0 being object st e0 in G1 .loops() holds
e0 in G2 .loops()

let e0 be object ; :: thesis: ( e0 in G1 .loops() implies e0 in G2 .loops() )
assume e0 in G1 .loops() ; :: thesis: e0 in G2 .loops()
then consider w being object such that
A7: e0 Joins w,w,G1 by Def2;
e0 in the_Edges_of G2

proof

assume A8: not e0 in the_Edges_of G2 ; :: thesis: contradiction
A9: e0 in the_Edges_of G1 by A7, GLIB_000:def 13;
the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A6, GLIB_006:def 12;
then e0 in {e} by A8, A9, XBOOLE_0:def 3;
then e = e0 by TARSKI:def 1;
then e0 Joins v1,v2,G1 by A6, GLIB_006:132;
then ( v1 = w & v2 = w ) by A7, GLIB_000:15;
hence contradiction by A6; :: thesis: verum

end;

then e0 Joins w,w,G2 by A7, GLIB_006:72;
hence e0 in G2 .loops() by Def2; :: thesis: verum

end;

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

end;

suppose ( ( not v1 in the_Vertices_of G2 or v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) & ( v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) ) ; :: thesis: G1 .loops() = G2 .loops()

then G1 == G2 by GLIB_006:def 12;
hence G1 .loops() = G2 .loops() by Th50; :: thesis: verum

end;

end;