for F being non empty Graph-yielding Function
for S being GraphSum of F holds
( ( F is loopless implies S is loopless ) & ( S is loopless implies F is loopless ) & ( F is non-multi implies S is non-multi ) & ( S is non-multi implies F is non-multi ) & ( F is non-Dmulti implies S is non-Dmulti ) & ( S is non-Dmulti implies F is non-Dmulti ) & ( F is simple implies S is simple ) & ( S is simple implies F is simple ) & ( F is Dsimple implies S is Dsimple ) & ( S is Dsimple implies F is Dsimple ) & ( F is chordal implies S is chordal ) & ( S is chordal implies F is chordal ) & ( F is edgeless implies S is edgeless ) & ( S is edgeless implies F is edgeless ) & ( F is loopfull implies S is loopfull ) & ( S is loopfull implies F is loopfull ) )