theorem Th125: :: GLIB_015:125

for F being non empty Graph-yielding Function
for S being GraphSum of F holds
( ( F is acyclic implies S is acyclic ) & ( S is acyclic implies F is acyclic ) & ( F is chordal implies S is chordal ) & ( S is chordal implies F is chordal ) )