let S be vertex-disjoint GraphUnionSet; :: thesis:
let G be GraphUnion of S; :: thesis:

hereby :: thesis:

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

now :: thesis:

let e1, e2, v1, v2 be object ; :: thesis:
assume A2: ( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ; :: thesis:
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:

end;

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

end;

hereby :: thesis:

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

now :: thesis:

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

end;

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

end;

hereby :: thesis:

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

now :: thesis:

let e1, e2, v1, v2 be object ; :: thesis:
assume A7: ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ; :: thesis:
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:

end;

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

end;

hereby :: thesis:

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

now :: thesis:

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

end;

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

end;

hereby :: thesis:

assume A11: S is acyclic ; :: thesis:
assume not G is acyclic ; :: thesis:
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:

end;

hereby :: thesis:

assume A14: G is acyclic ; :: thesis:

now :: thesis:

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

end;

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

end;