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

thus ( G is loopless implies for v, e being object holds not e SJoins {v},{v},G ) by Th12, GLIB_000:18; :: thesis: ( ( for v, e being object holds not e SJoins {v},{v},G ) implies G is loopless )

assume A1: for v, e being object holds not e SJoins {v},{v},G ; :: thesis: G is loopless

for v, e being object holds not e Joins v,v,G

thus ( G is loopless implies for v, e being object holds not e SJoins {v},{v},G ) by Th12, GLIB_000:18; :: thesis: ( ( for v, e being object holds not e SJoins {v},{v},G ) implies G is loopless )

assume A1: for v, e being object holds not e SJoins {v},{v},G ; :: thesis: G is loopless

for v, e being object holds not e Joins v,v,G

proof

hence
G is loopless
by GLIB_000:18; :: thesis: verum
let v be object ; :: thesis: for e being object holds not e Joins v,v,G

given e being object such that A2: e Joins v,v,G ; :: thesis: contradiction

v in {v} by TARSKI:def 1;

then e SJoins {v},{v},G by A2, GLIB_000:17;

hence contradiction by A1; :: thesis: verum

end;given e being object such that A2: e Joins v,v,G ; :: thesis: contradiction

v in {v} by TARSKI:def 1;

then e SJoins {v},{v},G by A2, GLIB_000:17;

hence contradiction by A1; :: thesis: verum