let S be Graph-membered set ; :: thesis: ( S is Dsimple implies ( S is loopless & S is non-Dmulti ) )
assume A5: S is Dsimple ; :: thesis: ( S is loopless & S is non-Dmulti )

now :: thesis: for G being _Graph st G in S holds
( G is loopless & G is non-Dmulti )

let G be _Graph; :: thesis: ( G in S implies ( G is loopless & G is non-Dmulti ) )
assume G in S ; :: thesis: ( G is loopless & G is non-Dmulti )
then G is Dsimple by A5;
hence ( G is loopless & G is non-Dmulti ) ; :: thesis: verum

end;

hence ( S is loopless & S is non-Dmulti ) ; :: thesis: verum