let S be vertex-disjoint GraphUnionSet; :: thesis: for G being GraphUnion of S holds
( ( S is chordal implies G is chordal ) & ( G is chordal implies S is chordal ) & ( S is loopfull implies G is loopfull ) & ( G is loopfull implies S is loopfull ) )
let G be GraphUnion of S; :: thesis: ( ( S is chordal implies G is chordal ) & ( G is chordal implies S is chordal ) & ( S is loopfull implies G is loopfull ) & ( G is loopfull implies S is loopfull ) )
hereby :: thesis: ( ( G is chordal implies S is chordal ) & ( S is loopfull implies G is loopfull ) & ( G is loopfull implies S is loopfull ) )
assume A1: S is chordal ; :: thesis: G is chordal
now :: thesis: for W being Walk of G st W .length() > 3 & W is Cycle-like holds
W is chordal
let W be Walk of G; :: thesis: ( W .length() > 3 & W is Cycle-like implies W is chordal )
assume A2: ( W .length() > 3 & W is Cycle-like ) ; :: thesis: W is chordal
now :: thesis: ex m, n being odd Nat st
( m + 2 < n & n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( for f being object st f in W .edges() holds
not f Joins W . m,W . n,G ) )
consider H being Element of S such that
A3: W is Walk of H by Th58;
reconsider W9 = W as Walk of H by A3;
( W9 .length() > 3 & W9 is Cycle-like ) by A2, GLIB_001:114, GLIB_006:24;
then W9 is chordal by A1, CHORD:def 11;
then consider m, n being odd Nat such that
A4: ( m + 2 < n & n <= len W9 & W9 . m <> W9 . n ) and
A5: ex e being object st e Joins W9 . m,W9 . n,H and
A6: for f being object st f in W9 .edges() holds
not f Joins W9 . m,W9 . n,H by CHORD:def 10;
take m = m; :: thesis: ex n being odd Nat st
( m + 2 < n & n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( for f being object st f in W .edges() holds
not f Joins W . m,W . n,G ) )
take n = n; :: thesis: ( m + 2 < n & n <= len W & W . m <> W . n & ex e being object st e Joins W . m,W . n,G & ( for f being object st f in W .edges() holds
not f Joins W . m,W . n,G ) )
thus ( m + 2 < n & n <= len W & W . m <> W . n ) by A4; :: thesis: ( ex e being object st e Joins W . m,W . n,G & ( for f being object st f in W .edges() holds
not f Joins W . m,W . n,G ) )
hereby :: thesis: for f being object st f in W .edges() holds
not f Joins W . m,W . n,G
consider e being object such that
A7: e Joins W9 . m,W9 . n,H by A5;
take e = e; :: thesis: e Joins W . m,W . n,G
H is Subgraph of G by GLIB_014:21;
hence e Joins W . m,W . n,G by A7, GLIB_000:72; :: thesis: verum
end;
let f be object ; :: thesis: ( f in W .edges() implies not f Joins W . m,W . n,G )
assume A8: f in W .edges() ; :: thesis: not f Joins W . m,W . n,G
W .edges() = rng (W .edgeSeq()) by GLIB_001:def 17
.= rng (W9 .edgeSeq()) by GLIB_001:86
.= W9 .edges() by GLIB_001:def 17 ;
then A9: not f Joins W9 . m,W9 . n,H by A6, A8;
assume f Joins W . m,W . n,G ; :: thesis: contradiction
then consider H9 being Element of S such that
A10: f Joins W . m,W . n,H9 by GLIBPRE1:117;
A11: W . n in the_Vertices_of H9 by A10, GLIB_000:13;
n is odd Element of NAT by ORDINAL1:def 12;
then W9 . n in the_Vertices_of H by A4, GLIB_001:7;
then H = H9 by A11, Def18, XBOOLE_0:3;
hence contradiction by A9, A10; :: thesis: verum
end;
hence W is chordal by CHORD:def 10; :: thesis: verum
end;
hence G is chordal by CHORD:def 11; :: thesis: verum
end;
hereby :: thesis: ( S is loopfull iff G is loopfull )
assume A12: G is chordal ; :: thesis: S is chordal
now :: thesis: for H being _Graph st H in S holds
H is chordal
let H be _Graph; :: thesis: ( H in S implies H is chordal )
assume H in S ; :: thesis: H is chordal
then H is inducedSubgraph of G,(the_Vertices_of H) by Th62;
hence H is chordal by A12; :: thesis: verum
end;
hence S is chordal by GLIB_014:def 11; :: thesis: verum
end;
thus ( S is loopfull implies G is loopfull ) ; :: thesis: ( G is loopfull implies S is loopfull )
hereby :: thesis: verum
assume A13: G is loopfull ; :: thesis: S is loopfull
now :: thesis: for H being _Graph st H in S holds
H is loopfull
let H be _Graph; :: thesis: ( H in S implies H is loopfull )
assume A14: H in S ; :: thesis: H is loopfull
now :: thesis: for v being Vertex of H ex e being object st e Joins v,v,H
let v be Vertex of H; :: thesis: ex e being object st e Joins v,v,H
H is Subgraph of G by A14, GLIB_014:21;
then the_Vertices_of H c= the_Vertices_of G by GLIB_000:def 32;
then reconsider w = v as Vertex of G by TARSKI:def 3;
consider e being object such that
A15: e Joins w,w,G by A13, GLIB_012:def 1;
consider H9 being Element of S such that
A16: e Joins w,w,H9 by A15, GLIBPRE1:117;
take e = e; :: thesis: e Joins v,v,H
w in the_Vertices_of H9 by A16, GLIB_000:13;
then H = H9 by A14, Def18, XBOOLE_0:3;
hence e Joins v,v,H by A16; :: thesis: verum
end;
hence H is loopfull by GLIB_012:def 1; :: thesis: verum
end;
hence S is loopfull by GLIB_014:def 13; :: thesis: verum
end;