let F be non empty Graph-yielding Function; :: thesis: 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 ) )
let S be GraphSum of F; :: thesis: ( ( 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 ) )
consider G9 being GraphUnion of rng (canGFDistinction F) such that
A1: S is G9 -Disomorphic by Def27;
consider H being PGraphMapping of G9,S such that
A2: H is Disomorphism by A1, GLIB_010:def 24;
F, canGFDistinction F are_Disomorphic by Th87;
then A3: F, canGFDistinction F are_isomorphic by Th42;
thus ( F is acyclic implies S is acyclic ) by A2, GLIB_010:140; :: thesis: ( ( S is acyclic implies F is acyclic ) & ( F is chordal implies S is chordal ) & ( S is chordal implies F is chordal ) )

hereby :: thesis: ( F is chordal iff S is chordal )

assume S is acyclic ; :: thesis: F is acyclic
then G9 is acyclic by A2, GLIB_010:140;
then rng (canGFDistinction F) is acyclic by Th60;
hence F is acyclic by GLIB_014:3; :: thesis: verum

end;

hereby :: thesis: ( S is chordal implies F is chordal )

assume F is chordal ; :: thesis: S is chordal
then canGFDistinction F is chordal by A3, Th48;
then G9 is chordal by Th63;
hence S is chordal by A2, GLIB_010:140; :: thesis: verum

end;

hereby :: thesis: verum

assume S is chordal ; :: thesis: F is chordal
then G9 is chordal by A2, GLIB_010:140;
then rng (canGFDistinction F) is chordal by Th63;
then canGFDistinction F is chordal by GLIB_014:3;
hence F is chordal by A3, Th48; :: thesis: verum

end;