let S be Graph-membered set ; :: thesis: ( S is loopless & S is non-multi implies S is simple )
assume A2: ( S is loopless & S is non-multi ) ; :: thesis: S is simple
let G be _Graph; :: according to GLIB_014:def 6 :: thesis: ( G in S implies G is simple )
assume G in S ; :: thesis: G is simple
then ( G is loopless & G is non-multi ) by A2;
hence G is simple ; :: thesis: verum