let G1, G2 be _Graph; :: thesis:
let S be GraphSum of G1,G2; :: thesis:
( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def 2;
then A1: ( 1 in dom <*G1,G2*> & 2 in dom <*G1,G2*> ) by FINSEQ_1:92;
A2: ( <*G1,G2*> . 1 = G1 & <*G1,G2*> . 2 = G2 ) ;
A3: S is GraphSum of <*G1,G2*> by Def28;
thus ( G1 is loopless & G2 is loopless implies S is loopless ) by A3; :: thesis:

hereby :: thesis:

assume S is loopless ; :: thesis:
then <*G1,G2*> is loopless by A3;
hence ( G1 is loopless & G2 is loopless ) by A1, A2; :: thesis:

end;

thus ( G1 is non-multi & G2 is non-multi implies S is non-multi ) by A3; :: thesis:

hereby :: thesis:

assume S is non-multi ; :: thesis:
then <*G1,G2*> is non-multi by A3;
hence ( G1 is non-multi & G2 is non-multi ) by A1, A2; :: thesis:

end;

thus ( G1 is non-Dmulti & G2 is non-Dmulti implies S is non-Dmulti ) by A3; :: thesis:

hereby :: thesis:

assume S is non-Dmulti ; :: thesis:
then <*G1,G2*> is non-Dmulti by A3;
hence ( G1 is non-Dmulti & G2 is non-Dmulti ) by A1, A2; :: thesis:

end;

thus ( G1 is simple & G2 is simple implies S is simple ) by A3; :: thesis:

hereby :: thesis:

assume S is simple ; :: thesis:
then <*G1,G2*> is simple by A3, Th124;
hence ( G1 is simple & G2 is simple ) by A1, A2; :: thesis:

end;

thus ( G1 is Dsimple & G2 is Dsimple implies S is Dsimple ) by A3; :: thesis:

hereby :: thesis:

assume S is Dsimple ; :: thesis:
then <*G1,G2*> is Dsimple by A3, Th124;
hence ( G1 is Dsimple & G2 is Dsimple ) by A1, A2; :: thesis:

end;

thus ( G1 is acyclic & G2 is acyclic implies S is acyclic ) by A3; :: thesis:

hereby :: thesis:

assume S is acyclic ; :: thesis:
then <*G1,G2*> is acyclic by A3;
hence ( G1 is acyclic & G2 is acyclic ) by A1, A2; :: thesis:

end;

thus ( G1 is chordal & G2 is chordal implies S is chordal ) by A3, Th124; :: thesis:

hereby :: thesis:

assume S is chordal ; :: thesis:
then <*G1,G2*> is chordal by A3, Th124;
hence ( G1 is chordal & G2 is chordal ) by A1, A2; :: thesis:

end;

thus ( G1 is edgeless & G2 is edgeless implies S is edgeless ) by A3; :: thesis:

hereby :: thesis:

assume S is edgeless ; :: thesis:
then <*G1,G2*> is edgeless by A3;
hence ( G1 is edgeless & G2 is edgeless ) by A1, A2; :: thesis:

end;

thus ( G1 is loopfull & G2 is loopfull implies S is loopfull ) by A3; :: thesis:

hereby :: thesis:

assume S is loopfull ; :: thesis:
then <*G1,G2*> is loopfull by A3;
hence ( G1 is loopfull & G2 is loopfull ) by A1, A2; :: thesis:

end;