let G be _Graph; :: thesis: ( G is loopless iff G .loops() = {} )
now :: thesis: ( G .loops() <> {} implies not 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;
hence ( G is loopless implies G .loops() = {} ) ; :: thesis: ( G .loops() = {} implies G is loopless )
now :: thesis: ( not G is loopless implies G .loops() <> {} )
assume 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;
hence ( G .loops() = {} implies G is loopless ) ; :: thesis: verum