let S be Graph-membered set ; :: thesis: ( S is simple implies ( S is loopless & S is non-multi ) )
assume A4: S is simple ; :: thesis: ( S is loopless & S is non-multi )

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

let G be _Graph; :: thesis: ( G in S implies ( G is loopless & G is non-multi ) )
assume G in S ; :: thesis: ( G is loopless & G is non-multi )
then G is simple by A4;
hence ( G is loopless & G is non-multi ) ; :: thesis: verum

end;

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