let G2 be removeLoops of G; :: thesis: G2 is loopless

assume not G2 is loopless ; :: thesis: contradiction

then consider v being object such that

A1: ex e being object st e Joins v,v,G2 by GLIB_000:18;

consider e being object such that

A2: e Joins v,v,G2 by A1;

v is set by TARSKI:1;

then e Joins v,v,G by A2, GLIB_000:72;

then e in G .loops() by Def2;

then not e in (the_Edges_of G) \ (G .loops()) by XBOOLE_0:def 5;

then not e in the_Edges_of G2 by GLIB_000:53;

hence contradiction by A2, GLIB_000:def 13; :: thesis: verum

assume not G2 is loopless ; :: thesis: contradiction

then consider v being object such that

A1: ex e being object st e Joins v,v,G2 by GLIB_000:18;

consider e being object such that

A2: e Joins v,v,G2 by A1;

v is set by TARSKI:1;

then e Joins v,v,G by A2, GLIB_000:72;

then e in G .loops() by Def2;

then not e in (the_Edges_of G) \ (G .loops()) by XBOOLE_0:def 5;

then not e in the_Edges_of G2 by GLIB_000:53;

hence contradiction by A2, GLIB_000:def 13; :: thesis: verum