let G be _Graph; :: thesis: ( the_Edges_of G = {} implies G is simple )
assume A1: the_Edges_of G = {} ; :: thesis: G is simple
then A2: G is loopless ;
for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2 by A1;
then G is non-multi ;
hence G is simple by A2; :: thesis: verum