let G2 be removeParallelEdges of G; G2 is loopfull
consider E being RepEdgeSelection of G such that
A1:
G2 is inducedSubgraph of G, the_Vertices_of G,E
by GLIB_009:def 7;
now for v being Vertex of G2 ex e being object st e Joins v,v,G2let v be
Vertex of
G2;
ex e being object st e Joins v,v,G2
v is
Vertex of
G
by GLIB_000:def 33;
then consider e0 being
object such that A2:
e0 Joins v,
v,
G
by Def1;
consider e being
object such that A3:
(
e Joins v,
v,
G &
e in E )
and
for
e9 being
object st
e9 Joins v,
v,
G &
e9 in E holds
e9 = e
by A2, GLIB_009:def 5;
take e =
e;
e Joins v,v,G2
E c= the_Edges_of G
;
then A4:
E c= G .edgesBetween (the_Vertices_of G)
by GLIB_000:34;
the_Vertices_of G c= the_Vertices_of G
;
then
the_Edges_of G2 = E
by A1, A4, GLIB_000:def 37;
hence
e Joins v,
v,
G2
by A3, GLIB_000:73;
verum end;
hence
G2 is loopfull
; verum