let F be 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 ) )
let S be GraphSum of F; ( ( 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 ) )
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; ( ( 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 ) )
thus A5:
( 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 ) )
thus A6:
( F is non-multi implies S is non-multi )
by A2, GLIB_010:89; ( ( 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 ) )
thus A7:
( 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 ) )
thus A8:
( F is non-Dmulti implies S is non-Dmulti )
by A2, GLIB_010:90; ( ( 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 ) )
thus A9:
( 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 ) )
thus
( F is simple implies S is simple )
by A4, A6; ( ( 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 ) )
thus
( S is simple implies F is simple )
by A5, A7; ( ( 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 ) )
thus
( F is Dsimple implies S is Dsimple )
by A4, A8; ( ( 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 ) )
thus
( S is Dsimple implies F is Dsimple )
by A5, A9; ( ( 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 ) )
thus
( F is edgeless implies S is edgeless )
by A2, GLIB_010:89; ( ( S is edgeless implies F is edgeless ) & ( F is loopfull implies S is loopfull ) & ( S is loopfull implies F is loopfull ) )