let G be _Graph; :: thesis: ( G is edgeless implies ( G is non-multi & G is non-Dmulti & G is loopless & G is simple & G is Dsimple ) )
assume A1: G is edgeless ; :: thesis: ( G is non-multi & G is non-Dmulti & G is loopless & G is simple & G is Dsimple )
then for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2 by GLIB_000:def 13;
hence A2: G is non-multi by GLIB_000:def 20; :: thesis: ( G is non-Dmulti & G is loopless & G is simple & G is Dsimple )
for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds
e1 = e2 by A1, GLIB_000:def 14;
hence G is non-Dmulti by GLIB_000:def 21; :: thesis: ( G is loopless & G is simple & G is Dsimple )
for e being object holds
( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e ) by A1;
hence G is loopless by GLIB_000:def 18; :: thesis: ( G is simple & G is Dsimple )
hence ( G is simple & G is Dsimple ) by A2; :: thesis: verum