let G be _Graph; :: thesis: ( not G is _trivial & G is Dcomplete implies ( not G is non-multi & not G is edgeless ) )
assume A3: ( not G is _trivial & G is Dcomplete ) ; :: thesis: ( not G is non-multi & not G is edgeless )
then consider v, w being Vertex of G such that
A4: v <> w by GLIB_000:21;
consider e1 being object such that
A5: e1 DJoins v,w,G by A3, A4;
consider e2 being object such that
A6: e2 DJoins w,v,G by A3, A4;
A7: e1 <> e2

proof

assume e1 = e2 ; :: thesis: contradiction
then ( (the_Source_of G) . e2 = v & (the_Source_of G) . e2 = w ) by A5, A6, GLIB_000:def 14;
hence contradiction by A4; :: thesis: verum

end;

( e1 Joins v,w,G & e2 Joins v,w,G ) by A5, A6, GLIB_000:16;
hence ( not G is non-multi & not G is edgeless ) by A7, GLIB_000:def 20; :: thesis: verum