let S be vertex-disjoint GraphUnionSet; :: thesis: for G being GraphUnion of S holds
( ( S is non-multi implies G is non-multi ) & ( G is non-multi implies S is non-multi ) & ( S is non-Dmulti implies G is non-Dmulti ) & ( G is non-Dmulti implies S is non-Dmulti ) & ( S is acyclic implies G is acyclic ) & ( G is acyclic implies S is acyclic ) )
let G be GraphUnion of S; :: thesis: ( ( S is non-multi implies G is non-multi ) & ( G is non-multi implies S is non-multi ) & ( S is non-Dmulti implies G is non-Dmulti ) & ( G is non-Dmulti implies S is non-Dmulti ) & ( S is acyclic implies G is acyclic ) & ( G is acyclic implies S is acyclic ) )

hereby :: thesis: ( ( G is non-multi implies S is non-multi ) & ( S is non-Dmulti implies G is non-Dmulti ) & ( G is non-Dmulti implies S is non-Dmulti ) & ( S is acyclic implies G is acyclic ) & ( G is acyclic implies S is acyclic ) )

assume A1: S is non-multi ; :: thesis: G is non-multi

now :: thesis: for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2

let e1, e2, v1, v2 be object ; :: thesis: ( e1 Joins v1,v2,G & e2 Joins v1,v2,G implies e1 = e2 )
assume A2: ( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ; :: thesis: e1 = e2
then consider H1 being Element of S such that
A3: e1 Joins v1,v2,H1 by GLIBPRE1:117;
consider H2 being Element of S such that
A4: e2 Joins v1,v2,H2 by A2, GLIBPRE1:117;
( v1 in the_Vertices_of H1 & v1 in the_Vertices_of H2 ) by A3, A4, GLIB_000:13;
then e2 Joins v1,v2,H1 by A4, Def18, XBOOLE_0:3;
hence e1 = e2 by A1, A3, GLIB_000:def 20; :: thesis: verum

end;

hence G is non-multi by GLIB_000:def 20; :: thesis: verum

end;

hereby :: thesis: ( ( S is non-Dmulti implies G is non-Dmulti ) & ( G is non-Dmulti implies S is non-Dmulti ) & ( S is acyclic implies G is acyclic ) & ( G is acyclic implies S is acyclic ) )

assume A5: G is non-multi ; :: thesis: S is non-multi

now :: thesis: for H being _Graph st H in S holds
H is non-multi

let H be _Graph; :: thesis: ( H in S implies H is non-multi )
assume H in S ; :: thesis: H is non-multi
then H is Subgraph of G by GLIB_014:21;
hence H is non-multi by A5; :: thesis: verum

end;

hence S is non-multi by GLIB_014:def 4; :: thesis: verum

end;

hereby :: thesis: ( ( G is non-Dmulti implies S is non-Dmulti ) & ( S is acyclic implies G is acyclic ) & ( G is acyclic implies S is acyclic ) )

assume A6: S is non-Dmulti ; :: thesis: G is non-Dmulti

now :: thesis: for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds
e1 = e2

let e1, e2, v1, v2 be object ; :: thesis: ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G implies e1 = e2 )
assume A7: ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ; :: thesis: e1 = e2
then consider H1 being Element of S such that
A8: e1 DJoins v1,v2,H1 by GLIBPRE1:116;
consider H2 being Element of S such that
A9: e2 DJoins v1,v2,H2 by A7, GLIBPRE1:116;
( e1 Joins v1,v2,H1 & e2 Joins v1,v2,H2 ) by A8, A9, GLIB_000:16;
then ( v1 in the_Vertices_of H1 & v1 in the_Vertices_of H2 ) by GLIB_000:13;
then e2 DJoins v1,v2,H1 by A9, Def18, XBOOLE_0:3;
hence e1 = e2 by A6, A8, GLIB_000:def 21; :: thesis: verum

end;

hence G is non-Dmulti by GLIB_000:def 21; :: thesis: verum

end;

hereby :: thesis: ( S is acyclic iff G is acyclic )

assume A10: G is non-Dmulti ; :: thesis: S is non-Dmulti

now :: thesis: for H being _Graph st H in S holds
H is non-Dmulti

let H be _Graph; :: thesis: ( H in S implies H is non-Dmulti )
assume H in S ; :: thesis: H is non-Dmulti
then H is Subgraph of G by GLIB_014:21;
hence H is non-Dmulti by A10; :: thesis: verum

end;

hence S is non-Dmulti by GLIB_014:def 5; :: thesis: verum

end;

hereby :: thesis: ( G is acyclic implies S is acyclic )

assume A11: S is acyclic ; :: thesis: G is acyclic
assume not G is acyclic ; :: thesis: contradiction
then consider W being Walk of G such that
A12: W is Cycle-like by GLIB_002:def 2;
consider H being Element of S such that
A13: W is Walk of H by Th58;
reconsider W9 = W as Walk of H by A13;
W9 is Cycle-like by A12, GLIB_006:24;
hence contradiction by A11, GLIB_002:def 2; :: thesis: verum

end;

hereby :: thesis: verum

assume A14: G is acyclic ; :: thesis: S is acyclic

now :: thesis: for H being _Graph st H in S holds
H is acyclic

let H be _Graph; :: thesis: ( H in S implies H is acyclic )
assume H in S ; :: thesis: H is acyclic
then H is Subgraph of G by GLIB_014:21;
hence H is acyclic by A14; :: thesis: verum

end;

hence S is acyclic by GLIB_014:def 8; :: thesis: verum

end;