let S be GraphUnionSet; :: thesis: for G being GraphUnion of S holds
( ( S is loopless implies G is loopless ) & ( G is loopless implies S is loopless ) & ( S is edgeless implies G is edgeless ) & ( G is edgeless implies S is edgeless ) & ( S is loopfull implies G is loopfull ) )
let G be GraphUnion of S; :: thesis: ( ( S is loopless implies G is loopless ) & ( G is loopless implies S is loopless ) & ( S is edgeless implies G is edgeless ) & ( G is edgeless implies S is edgeless ) & ( S is loopfull implies G is loopfull ) )

hereby :: thesis: ( ( G is loopless implies S is loopless ) & ( S is edgeless implies G is edgeless ) & ( G is edgeless implies S is edgeless ) & ( S is loopfull implies G is loopfull ) )

assume A1: S is loopless ; :: thesis: G is loopless
assume not G is loopless ; :: thesis: contradiction
then consider v being object such that
A2: ex e being object st e DJoins v,v,G by GLIB_000:136;
reconsider v = v as set by TARSKI:1;
consider e being object such that
A3: e DJoins v,v,G by A2;
reconsider e = e as set by TARSKI:1;
e in the_Edges_of G by A3, GLIB_000:def 14;
then e in union (the_Edges_of S) by Def25;
then consider E being set such that
A4: ( e in E & E in the_Edges_of S ) by TARSKI:def 4;
consider H being _Graph such that
A5: ( H in S & E = the_Edges_of H ) by A4, Def15;
H is Subgraph of G by A5, Th21;
then e DJoins v,v,H by A3, A4, A5, GLIB_000:73;
hence contradiction by A1, A5, GLIB_000:136; :: thesis: verum

end;

hereby :: thesis: ( ( S is edgeless implies G is edgeless ) & ( G is edgeless implies S is edgeless ) & ( S is loopfull implies G is loopfull ) )

assume A6: G is loopless ; :: thesis: S is loopless

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

let H be _Graph; :: thesis: ( H in S implies H is loopless )
assume H in S ; :: thesis: H is loopless
then H is Subgraph of G by Th21;
hence H is loopless by A6; :: thesis: verum

end;

hence S is loopless ; :: thesis: verum

end;

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

assume A8: S is edgeless ; :: thesis: G is edgeless
the_Edges_of G = union (the_Edges_of S) by Def25;
hence G is edgeless by A8; :: thesis: verum

end;

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

assume A9: G is edgeless ; :: thesis: S is edgeless

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

let H be _Graph; :: thesis: ( H in S implies H is edgeless )
assume H in S ; :: thesis: H is edgeless
then H is Subgraph of G by Th21;
hence H is edgeless by A9; :: thesis: verum

end;

hence S is edgeless ; :: thesis: verum

end;

hereby :: thesis: verum

assume A11: S is loopfull ; :: thesis: G is loopfull

now :: thesis: for v being Vertex of G ex e being object st e DJoins v,v,G

let v be Vertex of G; :: thesis: ex e being object st e DJoins v,v,G
v in the_Vertices_of G ;
then v in union (the_Vertices_of S) by Def25;
then consider V being set such that
A12: ( v in V & V in the_Vertices_of S ) by TARSKI:def 4;
consider H being _Graph such that
A13: ( H in S & V = the_Vertices_of H ) by A12, Def14;
consider e being object such that
A14: e DJoins v,v,H by A11, A12, A13, GLIB_012:1;
take e = e; :: thesis: e DJoins v,v,G
H is Subgraph of G by A13, Th21;
hence e DJoins v,v,G by A14, GLIB_000:72; :: thesis: verum

end;

hence G is loopfull by GLIB_012:1; :: thesis: verum

end;