let G be _Graph; :: thesis: ( G is loopless iff 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 Joins v,v,G ) ; :: thesis: ( ( for v, e being object holds not e Joins v,v,G ) implies G is loopless )
assume A1: for v, e being object holds not e Joins v,v,G ; :: thesis: G is loopless

now :: thesis: for e being object holds
( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e )

given e being object such that A2: ( 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 A2;
hence contradiction by A1; :: thesis: verum

end;

hence G is loopless ; :: thesis: verum