let G be _Graph; :: thesis: ( G is loopless iff for v, e being set holds not e Joins v,v,G )

hereby :: thesis: ( ( for v, e being set holds not e Joins v,v,G ) implies G is loopless )

assume A1: G is loopless ; :: thesis: for v, e being set holds not e Joins v,v,G
let v be set ; :: thesis: for e being set holds not e Joins v,v,G

now

given e being set such that A2: e Joins v,v,G ; :: thesis: contradiction
A3: (the_Target_of G) . e = v by A2, Def15;
( e in the_Edges_of G & (the_Source_of G) . e = v ) by A2, Def15;
hence contradiction by A1, A3, Def20; :: thesis: verum

end;

hence for e being set holds not e Joins v,v,G ; :: thesis: verum

end;

assume A4: for v, e being set holds not e Joins v,v,G ; :: thesis: G is loopless

now

given e being set such that A5: ( e in the_Edges_of G & (the_Source_of G) . e = (the_Target_of G) . e ) ; :: thesis: contradiction
set v = (the_Source_of G) . e;
e Joins (the_Source_of G) . e,(the_Source_of G) . e,G by A5, Def15;
hence contradiction by A4; :: thesis: verum

end;

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