let G be _Graph; :: thesis: ( G is loopless iff for v being object holds G .edgesBetween ({v},{v}) = {} )

for v, e being object holds not e SJoins {v},{v},G

hereby :: thesis: ( ( for v being object holds G .edgesBetween ({v},{v}) = {} ) implies G is loopless )

assume A3:
for v being object holds G .edgesBetween ({v},{v}) = {}
; :: thesis: 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})

end;let v be object ; :: thesis: G .edgesBetween ({v},{v}) = {}

for e being object holds not e in G .edgesBetween ({v},{v})

proof

hence
G .edgesBetween ({v},{v}) = {}
by XBOOLE_0:def 1; :: thesis: verum
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;e SJoins {v},{v},G by A2, GLIB_000:def 30;

hence contradiction by A1, Th18; :: thesis: verum

for v, e being object holds not e SJoins {v},{v},G

proof

hence
G is loopless
by Th18; :: thesis: verum
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;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