let G be _Graph; :: thesis: ( G is loopless iff for v, e being object holds not e DSJoins {v},{v},G )

hereby :: thesis: ( ( for v, e being object holds not e DSJoins {v},{v},G ) implies G is loopless )

assume A1: G is loopless ; :: thesis: for v, e being object holds not e DSJoins {v},{v},G
let v be object ; :: thesis: for e being object holds not e DSJoins {v},{v},G
given e being object such that A2: e DSJoins {v},{v},G ; :: thesis: contradiction
e SJoins {v},{v},G by A2;
hence contradiction by A1, Th137; :: thesis: verum

end;

assume A3: for v, e being object holds not e DSJoins {v},{v},G ; :: 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 DSJoins {v},{v},G by A4;
hence contradiction by A3; :: thesis: verum

end;

hence G is loopless by Th137; :: thesis: verum