let G be _Graph; :: thesis: ( G is loopless iff for v being object holds G .edgesBetween ({v},{v}) = {} )
hereby :: thesis: ( ( for v being object holds G .edgesBetween ({v},{v}) = {} ) implies G is loopless )
assume A1: G is loopless ; :: thesis: for v being object holds G .edgesBetween ({v},{v}) = {}
let v be object ; :: thesis: G .edgesBetween ({v},{v}) = {}
for e being object holds not e in G .edgesBetween ({v},{v})
proof
given e being object such that A2: e in G .edgesBetween ({v},{v}) ; :: thesis: contradiction
e SJoins {v},{v},G by A2, GLIB_000:def 30;
hence contradiction by A1, Th18; :: thesis: verum
end;
hence G .edgesBetween ({v},{v}) = {} by XBOOLE_0:def 1; :: thesis: verum
end;
assume A3: for v being object holds G .edgesBetween ({v},{v}) = {} ; :: thesis: G is loopless
for v, e being object holds not e SJoins {v},{v},G
proof
let v be object ; :: thesis: for e being object holds not e SJoins {v},{v},G
given e being object such that A4: e SJoins {v},{v},G ; :: thesis: contradiction
e in G .edgesBetween ({v},{v}) by A4, GLIB_000:def 30;
hence contradiction by A3; :: thesis: verum
end;
hence G is loopless by Th18; :: thesis: verum