let S be vertex-disjoint GraphUnionSet; :: thesis: for G being GraphUnion of S holds
( ( S is simple implies G is simple ) & ( G is simple implies S is simple ) & ( S is Dsimple implies G is Dsimple ) & ( G is Dsimple implies S is Dsimple ) )
let G be GraphUnion of S; :: thesis: ( ( S is simple implies G is simple ) & ( G is simple implies S is simple ) & ( S is Dsimple implies G is Dsimple ) & ( G is Dsimple implies S is Dsimple ) )
hereby :: thesis: ( ( G is simple implies S is simple ) & ( S is Dsimple implies G is Dsimple ) & ( G is Dsimple implies S is Dsimple ) )
assume S is simple ; :: thesis: G is simple
then ( G is loopless & G is non-multi ) by Th60;
hence G is simple ; :: thesis: verum
end;
hereby :: thesis: ( S is Dsimple iff G is Dsimple )
assume G is simple ; :: thesis: S is simple
then ( G is loopless & G is non-multi ) ;
then ( S is loopless & S is non-multi ) by Th60, GLIB_014:23;
hence S is simple ; :: thesis: verum
end;
hereby :: thesis: ( G is Dsimple implies S is Dsimple )
assume S is Dsimple ; :: thesis: G is Dsimple
then ( G is loopless & G is non-Dmulti ) by Th60;
hence G is Dsimple ; :: thesis: verum
end;
hereby :: thesis: verum
assume G is Dsimple ; :: thesis: S is Dsimple
then ( S is loopless & S is non-Dmulti ) by Th60, GLIB_014:23;
hence S is Dsimple ; :: thesis: verum
end;