for G1, G2 being _Graph
for S being GraphSum of G1,G2 holds
( ( G1 is loopless & G2 is loopless implies S is loopless ) & ( S is loopless implies ( G1 is loopless & G2 is loopless ) ) & ( G1 is non-multi & G2 is non-multi implies S is non-multi ) & ( S is non-multi implies ( G1 is non-multi & G2 is non-multi ) ) & ( G1 is non-Dmulti & G2 is non-Dmulti implies S is non-Dmulti ) & ( S is non-Dmulti implies ( G1 is non-Dmulti & G2 is non-Dmulti ) ) & ( G1 is simple & G2 is simple implies S is simple ) & ( S is simple implies ( G1 is simple & G2 is simple ) ) & ( G1 is Dsimple & G2 is Dsimple implies S is Dsimple ) & ( S is Dsimple implies ( G1 is Dsimple & G2 is Dsimple ) ) & ( G1 is acyclic & G2 is acyclic implies S is acyclic ) & ( S is acyclic implies ( G1 is acyclic & G2 is acyclic ) ) & ( G1 is chordal & G2 is chordal implies S is chordal ) & ( S is chordal implies ( G1 is chordal & G2 is chordal ) ) & ( G1 is edgeless & G2 is edgeless implies S is edgeless ) & ( S is edgeless implies ( G1 is edgeless & G2 is edgeless ) ) & ( G1 is loopfull & G2 is loopfull implies S is loopfull ) & ( S is loopfull implies ( G1 is loopfull & G2 is loopfull ) ) )