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_009:17;
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_009:17; :: 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 A7: 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 A10: 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;