let S be Graph-membered set ; :: thesis: ( S is loopless & S is non-Dmulti implies S is Dsimple )
assume A3: ( S is loopless & S is non-Dmulti ) ; :: thesis: S is Dsimple
let G be _Graph; :: according to GLIB_014:def 7 :: thesis: ( G in S implies G is Dsimple )
assume G in S ; :: thesis: G is Dsimple
then ( G is loopless & G is non-Dmulti ) by A3;
hence G is Dsimple ; :: thesis: verum