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