let G be non edgeless _Graph; :: thesis: for e being Edge of G holds
( createGraph e is loopless iff not e in G .loops() )
let e be Edge of G; :: thesis: ( createGraph e is loopless iff not e in G .loops() )

hereby :: thesis: ( not e in G .loops() implies createGraph e is loopless )

assume A1: createGraph e is loopless ; :: thesis: not e in G .loops()
assume e in G .loops() ; :: thesis: contradiction
then consider v being object such that
A2: e Joins v,v,G by GLIB_009:def 2;
( (the_Source_of G) . e = v & (the_Target_of G) . e = v ) by A2, GLIB_000:def 13;
hence contradiction by A1, Th14, GLIB_000:136; :: thesis: verum

end;

assume A3: not e in G .loops() ; :: thesis: createGraph e is loopless
assume not createGraph e is loopless ; :: thesis: contradiction
then consider v, e0 being object such that
A4: e0 DJoins v,v, createGraph e by GLIB_000:136;
( e0 = e & v is set ) by A4, Th15, TARSKI:1;
hence contradiction by A3, A4, GLIB_000:72, GLIB_009:45; :: thesis: verum