let F be non empty Graph-yielding Function; :: thesis:
let S be GraphSum of F; :: thesis:
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 A4: ( F is loopless implies S is loopless ) by A2, GLIB_010:89; :: thesis:
thus A5: ( S is loopless implies F is loopless ) :: thesis:

proof

assume S is loopless ; :: thesis:
then G9 is loopless by A2, GLIB_010:89;
then rng (canGFDistinction F) is loopless by GLIB_014:23;
hence F is loopless by GLIB_014:3; :: thesis:

end;

thus A6: ( F is non-multi implies S is non-multi ) by A2, GLIB_010:89; :: thesis:
thus A7: ( S is non-multi implies F is non-multi ) :: thesis:

proof

assume S is non-multi ; :: thesis:
then G9 is non-multi by A2, GLIB_010:89;
then rng (canGFDistinction F) is non-multi by Th60;
hence F is non-multi by GLIB_014:3; :: thesis:

end;

thus A8: ( F is non-Dmulti implies S is non-Dmulti ) by A2, GLIB_010:90; :: thesis:
thus A9: ( S is non-Dmulti implies F is non-Dmulti ) :: thesis:

proof

assume S is non-Dmulti ; :: thesis:
then G9 is non-Dmulti by A2, GLIB_010:90;
then rng (canGFDistinction F) is non-Dmulti by Th60;
hence F is non-Dmulti by GLIB_014:3; :: thesis:

end;

thus ( F is simple implies S is simple ) by A4, A6; :: thesis:
thus ( S is simple implies F is simple ) by A5, A7; :: thesis:
thus ( F is Dsimple implies S is Dsimple ) by A4, A8; :: thesis:
thus ( S is Dsimple implies F is Dsimple ) by A5, A9; :: thesis:

hereby :: thesis:

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

end;

hereby :: thesis:

assume S is chordal ; :: thesis:
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:

end;

thus ( F is edgeless implies S is edgeless ) by A2, GLIB_010:89; :: thesis:

hereby :: thesis:

assume S is edgeless ; :: thesis:
then G9 is edgeless by A2, GLIB_010:89;
then rng (canGFDistinction F) is edgeless by GLIB_014:23;
hence F is edgeless by GLIB_014:3; :: thesis:

end;

hereby :: thesis:

assume F is loopfull ; :: thesis:
then canGFDistinction F is loopfull by A3, Th48;
then rng (canGFDistinction F) is loopfull ;
hence S is loopfull by A2, GLIB_012:10; :: thesis:

end;

hereby :: thesis:

assume S is loopfull ; :: thesis:
then G9 is loopfull by A2, GLIB_012:10;
then rng (canGFDistinction F) is loopfull by Th63;
then canGFDistinction F is loopfull by GLIB_014:3;
hence F is loopfull by A3, Th48; :: thesis:

end;