let G be _Graph; :: thesis: ( G is loopless iff G .loops() = {} )

now :: thesis: ( G .loops() <> {} implies not G is loopless )

hence
( G is loopless implies G .loops() = {} )
; :: thesis: ( G .loops() = {} implies G is loopless )assume
G .loops() <> {}
; :: thesis: not G is loopless

then consider e being object such that

A1: e in G .loops() by XBOOLE_0:def 1;

consider v being object such that

A2: e Joins v,v,G by A1, Def2;

thus not G is loopless by A2, GLIB_000:18; :: thesis: verum

end;then consider e being object such that

A1: e in G .loops() by XBOOLE_0:def 1;

consider v being object such that

A2: e Joins v,v,G by A1, Def2;

thus not G is loopless by A2, GLIB_000:18; :: thesis: verum

now :: thesis: ( not G is loopless implies G .loops() <> {} )

hence
( G .loops() = {} implies G is loopless )
; :: thesis: verumassume
not G is loopless
; :: thesis: G .loops() <> {}

then consider v being object such that

A3: ex e being object st e Joins v,v,G by GLIB_000:18;

consider e being object such that

A4: e Joins v,v,G by A3;

thus G .loops() <> {} by A4, Def2; :: thesis: verum

end;then consider v being object such that

A3: ex e being object st e Joins v,v,G by GLIB_000:18;

consider e being object such that

A4: e Joins v,v,G by A3;

thus G .loops() <> {} by A4, Def2; :: thesis: verum