let G2 be removeLoops of G; G2 is complete
A1:
( the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 = (the_Edges_of G) \ (G .loops()) )
by GLIB_000:53;
now for v2, w2 being Vertex of G2 st v2 <> w2 holds
v2,w2 are_adjacent let v2,
w2 be
Vertex of
G2;
( v2 <> w2 implies v2,w2 are_adjacent )assume A2:
v2 <> w2
;
v2,w2 are_adjacent reconsider v1 =
v2,
w1 =
w2 as
Vertex of
G by GLIB_000:53;
consider e being
object such that A3:
e Joins v1,
w1,
G
by A2, CHORD:def 6, CHORD:def 3;
A4:
not
e in G .loops()
by A2, A3, Th46;
e in the_Edges_of G
by A3, GLIB_000:def 13;
then
e in the_Edges_of G2
by A1, A4, XBOOLE_0:def 5;
then
e Joins v2,
w2,
G2
by A3, GLIB_000:73;
hence
v2,
w2 are_adjacent
by CHORD:def 3;
verum end;
hence
G2 is complete
by CHORD:def 6; verum