let S be Graph-membered set ; :: thesis: ( S is non-multi implies S is non-Dmulti )
assume A1: S is non-multi ; :: thesis: S is non-Dmulti
let G be _Graph; :: according to GLIB_014:def 5 :: thesis: ( G in S implies G is non-Dmulti )
assume G in S ; :: thesis: G is non-Dmulti
then G is non-multi by A1;
hence G is non-Dmulti ; :: thesis: verum