let G be _Graph; :: thesis: ( the_Edges_of G = {} implies G is simple )
assume A1: the_Edges_of G = {} ; :: thesis: G is simple
then for e being set holds
( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e ) ;
then A2: G is loopless by Def20;
for e1, e2, v1, v2 being set st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2 by A1, Def15;
then G is non-multi by Def22;
hence G is simple by A2; :: thesis: verum