:: HELLY semantic presentation begin theorem :: HELLY:1 for p being non empty FinSequence holds <*(p . 1)*> ^' p = p proof let p be non empty FinSequence; ::_thesis: <*(p . 1)*> ^' p = p set o = <*(p . 1)*> ^' p; A1: (len (<*(p . 1)*> ^' p)) + 1 = (len <*(p . 1)*>) + (len p) by GRAPH_2:13; A2: len <*(p . 1)*> = 1 by FINSEQ_1:39; A3: now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_(<*(p_._1)*>_^'_p)_holds_ (<*(p_._1)*>_^'_p)_._k_=_p_._k let k be Nat; ::_thesis: ( 1 <= k & k <= len (<*(p . 1)*> ^' p) implies (<*(p . 1)*> ^' p) . b1 = p . b1 ) assume that A4: 1 <= k and A5: k <= len (<*(p . 1)*> ^' p) ; ::_thesis: (<*(p . 1)*> ^' p) . b1 = p . b1 percases ( k <= len <*(p . 1)*> or k > len <*(p . 1)*> ) ; supposeA6: k <= len <*(p . 1)*> ; ::_thesis: (<*(p . 1)*> ^' p) . b1 = p . b1 then k <= 1 by FINSEQ_1:39; then A7: k = 1 by A4, XXREAL_0:1; hence (<*(p . 1)*> ^' p) . k = <*(p . 1)*> . 1 by A6, GRAPH_2:14 .= p . k by A7, FINSEQ_1:40 ; ::_thesis: verum end; suppose k > len <*(p . 1)*> ; ::_thesis: (<*(p . 1)*> ^' p) . b1 = p . b1 then consider i being Element of NAT such that A8: k = (len <*(p . 1)*>) + i and A9: 1 <= i by FINSEQ_4:84; i < len p by A1, A2, A5, A8, NAT_1:13; hence (<*(p . 1)*> ^' p) . k = p . k by A2, A8, A9, GRAPH_2:15; ::_thesis: verum end; end; end; (len (<*(p . 1)*> ^' p)) + 1 = 1 + (len p) by A1, FINSEQ_1:39; hence <*(p . 1)*> ^' p = p by A3, FINSEQ_1:14; ::_thesis: verum end; definition let p, q be FinSequence; func maxPrefix (p,q) -> FinSequence means :Def1: :: HELLY:def 1 ( it is_a_prefix_of p & it is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds r is_a_prefix_of it ) ); existence ex b1 being FinSequence st ( b1 is_a_prefix_of p & b1 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds r is_a_prefix_of b1 ) ) proof deffunc H1( set ) -> set = $1; defpred S1[ set ] means ex r being FinSequence st ( r c= p & r c= q & len r = $1 ); set S = { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } ; A1: for x being set st x in { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } holds x is natural proof let x be set ; ::_thesis: ( x in { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } implies x is natural ) assume x in { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } ; ::_thesis: x is natural then ex n being Element of NAT st ( x = n & 0 <= n & n <= len p & S1[n] ) ; hence x is natural ; ::_thesis: verum end; A2: { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } is finite from FINSEQ_1:sch_6(); ( {} c= p & {} c= q & len {} = 0 ) by XBOOLE_1:2; then 0 in { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } ; then reconsider S = { H1(k) where k is Element of NAT : ( 0 <= k & k <= len p & S1[k] ) } as non empty finite natural-membered set by A1, A2, MEMBERED:def_6; set maxk = max S; max S in S by XXREAL_2:def_8; then consider K being Element of NAT such that A3: K = max S and 0 <= K and K <= len p and A4: S1[K] ; consider R being FinSequence such that A5: R c= p and A6: R c= q and A7: len R = K by A4; take R ; ::_thesis: ( R is_a_prefix_of p & R is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds r is_a_prefix_of R ) ) thus R c= p by A5; ::_thesis: ( R is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds r is_a_prefix_of R ) ) thus R c= q by A6; ::_thesis: for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds r is_a_prefix_of R let r be FinSequence; ::_thesis: ( r is_a_prefix_of p & r is_a_prefix_of q implies r is_a_prefix_of R ) assume that A8: r c= p and A9: r c= q ; ::_thesis: r is_a_prefix_of R dom r c= dom p by A8, GRFUNC_1:2; then len r <= len p by FINSEQ_3:30; then len r in S by A8, A9; then len r <= len R by A3, A7, XXREAL_2:def_8; then A10: dom r c= dom R by FINSEQ_3:30; now__::_thesis:_for_x_being_set_st_x_in_dom_r_holds_ r_._x_=_R_._x let x be set ; ::_thesis: ( x in dom r implies r . x = R . x ) assume A11: x in dom r ; ::_thesis: r . x = R . x hence r . x = p . x by A8, GRFUNC_1:2 .= R . x by A5, A10, A11, GRFUNC_1:2 ; ::_thesis: verum end; hence r is_a_prefix_of R by A10, GRFUNC_1:2; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence st b1 is_a_prefix_of p & b1 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds r is_a_prefix_of b1 ) & b2 is_a_prefix_of p & b2 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds r is_a_prefix_of b2 ) holds b1 = b2 proof let it1, it2 be FinSequence; ::_thesis: ( it1 is_a_prefix_of p & it1 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds r is_a_prefix_of it1 ) & it2 is_a_prefix_of p & it2 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds r is_a_prefix_of it2 ) implies it1 = it2 ) assume ( it1 c= p & it1 c= q & ( for r being FinSequence st r c= p & r c= q holds r c= it1 ) & it2 c= p & it2 c= q & ( for r being FinSequence st r c= p & r c= q holds r c= it2 ) ) ; ::_thesis: it1 = it2 then ( it1 c= it2 & it2 c= it1 ) ; hence it1 = it2 by XBOOLE_0:def_10; ::_thesis: verum end; commutativity for b1, p, q being FinSequence st b1 is_a_prefix_of p & b1 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds r is_a_prefix_of b1 ) holds ( b1 is_a_prefix_of q & b1 is_a_prefix_of p & ( for r being FinSequence st r is_a_prefix_of q & r is_a_prefix_of p holds r is_a_prefix_of b1 ) ) ; end; :: deftheorem Def1 defines maxPrefix HELLY:def_1_:_ for p, q, b3 being FinSequence holds ( b3 = maxPrefix (p,q) iff ( b3 is_a_prefix_of p & b3 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds r is_a_prefix_of b3 ) ) ); theorem :: HELLY:2 for p, q being FinSequence holds ( p is_a_prefix_of q iff maxPrefix (p,q) = p ) proof let p, q be FinSequence; ::_thesis: ( p is_a_prefix_of q iff maxPrefix (p,q) = p ) hereby ::_thesis: ( maxPrefix (p,q) = p implies p is_a_prefix_of q ) assume p c= q ; ::_thesis: maxPrefix (p,q) = p then A1: p c= maxPrefix (p,q) by Def1; maxPrefix (p,q) c= p by Def1; hence maxPrefix (p,q) = p by A1, XBOOLE_0:def_10; ::_thesis: verum end; assume maxPrefix (p,q) = p ; ::_thesis: p is_a_prefix_of q hence p is_a_prefix_of q by Def1; ::_thesis: verum end; theorem Th3: :: HELLY:3 for p, q being FinSequence holds len (maxPrefix (p,q)) <= len p proof let p, q be FinSequence; ::_thesis: len (maxPrefix (p,q)) <= len p maxPrefix (p,q) c= p by Def1; hence len (maxPrefix (p,q)) <= len p by FINSEQ_1:63; ::_thesis: verum end; theorem Th4: :: HELLY:4 for p being non empty FinSequence holds <*(p . 1)*> is_a_prefix_of p proof let p be non empty FinSequence; ::_thesis: <*(p . 1)*> is_a_prefix_of p A1: now__::_thesis:_for_x_being_set_st_x_in_dom_<*(p_._1)*>_holds_ <*(p_._1)*>_._x_=_p_._x let x be set ; ::_thesis: ( x in dom <*(p . 1)*> implies <*(p . 1)*> . x = p . x ) A2: dom <*(p . 1)*> = Seg 1 by FINSEQ_1:def_8; assume x in dom <*(p . 1)*> ; ::_thesis: <*(p . 1)*> . x = p . x then x = 1 by A2, FINSEQ_1:2, TARSKI:def_1; hence <*(p . 1)*> . x = p . x by FINSEQ_1:def_8; ::_thesis: verum end; len p >= 1 by FINSEQ_1:20; then len <*(p . 1)*> <= len p by FINSEQ_1:39; then dom <*(p . 1)*> c= dom p by FINSEQ_3:30; hence <*(p . 1)*> is_a_prefix_of p by A1, GRFUNC_1:2; ::_thesis: verum end; theorem Th5: :: HELLY:5 for p, q being non empty FinSequence st p . 1 = q . 1 holds 1 <= len (maxPrefix (p,q)) proof let p, q be non empty FinSequence; ::_thesis: ( p . 1 = q . 1 implies 1 <= len (maxPrefix (p,q)) ) assume that A1: p . 1 = q . 1 and A2: 1 > len (maxPrefix (p,q)) ; ::_thesis: contradiction A3: <*(p . 1)*> c= p by Th4; <*(p . 1)*> c= q by A1, Th4; then <*(p . 1)*> c= maxPrefix (p,q) by A3, Def1; then len <*(p . 1)*> <= len (maxPrefix (p,q)) by FINSEQ_1:63; hence contradiction by A2, FINSEQ_1:39; ::_thesis: verum end; theorem Th6: :: HELLY:6 for p, q being FinSequence for j being Nat st j <= len (maxPrefix (p,q)) holds (maxPrefix (p,q)) . j = p . j proof let p, q be FinSequence; ::_thesis: for j being Nat st j <= len (maxPrefix (p,q)) holds (maxPrefix (p,q)) . j = p . j let j be Nat; ::_thesis: ( j <= len (maxPrefix (p,q)) implies (maxPrefix (p,q)) . j = p . j ) assume A1: j <= len (maxPrefix (p,q)) ; ::_thesis: (maxPrefix (p,q)) . j = p . j A2: maxPrefix (p,q) c= p by Def1; percases ( j = 0 or j <> 0 ) ; supposeA3: j = 0 ; ::_thesis: (maxPrefix (p,q)) . j = p . j then A4: not j in dom p by FINSEQ_3:24; not j in dom (maxPrefix (p,q)) by A3, FINSEQ_3:24; hence (maxPrefix (p,q)) . j = 0 by FUNCT_1:def_2 .= p . j by A4, FUNCT_1:def_2 ; ::_thesis: verum end; suppose j <> 0 ; ::_thesis: (maxPrefix (p,q)) . j = p . j then 0 + 1 <= j by NAT_1:13; then j in dom (maxPrefix (p,q)) by A1, FINSEQ_3:25; hence (maxPrefix (p,q)) . j = p . j by A2, GRFUNC_1:2; ::_thesis: verum end; end; end; theorem Th7: :: HELLY:7 for p, q being FinSequence for j being Nat st j <= len (maxPrefix (p,q)) holds p . j = q . j proof let p, q be FinSequence; ::_thesis: for j being Nat st j <= len (maxPrefix (p,q)) holds p . j = q . j let j be Nat; ::_thesis: ( j <= len (maxPrefix (p,q)) implies p . j = q . j ) assume A1: j <= len (maxPrefix (p,q)) ; ::_thesis: p . j = q . j thus p . j = (maxPrefix (p,q)) . j by A1, Th6 .= q . j by A1, Th6 ; ::_thesis: verum end; theorem Th8: :: HELLY:8 for p, q being FinSequence holds ( not p is_a_prefix_of q iff len (maxPrefix (p,q)) < len p ) proof let p, q be FinSequence; ::_thesis: ( not p is_a_prefix_of q iff len (maxPrefix (p,q)) < len p ) A1: maxPrefix (p,q) c= p by Def1; hereby ::_thesis: ( len (maxPrefix (p,q)) < len p implies not p is_a_prefix_of q ) assume A2: not p c= q ; ::_thesis: len (maxPrefix (p,q)) < len p A3: now__::_thesis:_not_len_(maxPrefix_(p,q))_=_len_p assume len (maxPrefix (p,q)) = len p ; ::_thesis: contradiction then A4: dom (maxPrefix (p,q)) = dom p by FINSEQ_3:29; maxPrefix (p,q) c= p by Def1; then maxPrefix (p,q) = p by A4, GRFUNC_1:3; hence contradiction by A2, Def1; ::_thesis: verum end; maxPrefix (p,q) c= p by Def1; then len (maxPrefix (p,q)) <= len p by FINSEQ_1:63; hence len (maxPrefix (p,q)) < len p by A3, XXREAL_0:1; ::_thesis: verum end; assume that A5: len (maxPrefix (p,q)) < len p and A6: p c= q ; ::_thesis: contradiction p c= maxPrefix (p,q) by A6, Def1; hence contradiction by A5, A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th9: :: HELLY:9 for p, q being FinSequence st not p is_a_prefix_of q & not q is_a_prefix_of p holds p . ((len (maxPrefix (p,q))) + 1) <> q . ((len (maxPrefix (p,q))) + 1) proof let p, q be FinSequence; ::_thesis: ( not p is_a_prefix_of q & not q is_a_prefix_of p implies p . ((len (maxPrefix (p,q))) + 1) <> q . ((len (maxPrefix (p,q))) + 1) ) assume that A1: not p c= q and A2: not q c= p and A3: p . ((len (maxPrefix (p,q))) + 1) = q . ((len (maxPrefix (p,q))) + 1) ; ::_thesis: contradiction set dI = len (maxPrefix (p,q)); set mP = maxPrefix (p,q); set lmP = (maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>; A4: now__::_thesis:_for_x_being_set_st_x_in_dom_((maxPrefix_(p,q))_^_<*(p_._((len_(maxPrefix_(p,q)))_+_1))*>)_holds_ ((maxPrefix_(p,q))_^_<*(p_._((len_(maxPrefix_(p,q)))_+_1))*>)_._x_=_q_._x let x be set ; ::_thesis: ( x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) implies ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = q . b1 ) assume A5: x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) ; ::_thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = q . b1 reconsider n = x as Nat by A5; A6: 1 <= n by A5, FINSEQ_3:25; n <= len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) by A5, FINSEQ_3:25; then A7: n <= (len (maxPrefix (p,q))) + 1 by FINSEQ_2:16; percases ( n <= len (maxPrefix (p,q)) or n = (len (maxPrefix (p,q))) + 1 ) by A7, NAT_1:8; supposeA8: n <= len (maxPrefix (p,q)) ; ::_thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = q . b1 then n in dom (maxPrefix (p,q)) by A6, FINSEQ_3:25; hence ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = (maxPrefix (p,q)) . x by FINSEQ_1:def_7 .= q . x by A8, Th6 ; ::_thesis: verum end; suppose n = (len (maxPrefix (p,q))) + 1 ; ::_thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = q . b1 hence ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = q . x by A3, FINSEQ_1:42; ::_thesis: verum end; end; end; A9: now__::_thesis:_for_x_being_set_st_x_in_dom_((maxPrefix_(p,q))_^_<*(p_._((len_(maxPrefix_(p,q)))_+_1))*>)_holds_ ((maxPrefix_(p,q))_^_<*(p_._((len_(maxPrefix_(p,q)))_+_1))*>)_._x_=_p_._x let x be set ; ::_thesis: ( x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) implies ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = p . b1 ) assume A10: x in dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) ; ::_thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = p . b1 reconsider n = x as Nat by A10; A11: 1 <= n by A10, FINSEQ_3:25; n <= len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) by A10, FINSEQ_3:25; then A12: n <= (len (maxPrefix (p,q))) + 1 by FINSEQ_2:16; percases ( n <= len (maxPrefix (p,q)) or n = (len (maxPrefix (p,q))) + 1 ) by A12, NAT_1:8; supposeA13: n <= len (maxPrefix (p,q)) ; ::_thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = p . b1 then n in dom (maxPrefix (p,q)) by A11, FINSEQ_3:25; hence ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = (maxPrefix (p,q)) . x by FINSEQ_1:def_7 .= p . x by A13, Th6 ; ::_thesis: verum end; suppose n = (len (maxPrefix (p,q))) + 1 ; ::_thesis: ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . b1 = p . b1 hence ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) . x = p . x by FINSEQ_1:42; ::_thesis: verum end; end; end; A14: len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) = (len (maxPrefix (p,q))) + 1 by FINSEQ_2:16; len (maxPrefix (p,q)) < len q by A2, Th8; then len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) <= len q by A14, NAT_1:13; then dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) c= dom q by FINSEQ_3:30; then A15: (maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*> c= q by A4, GRFUNC_1:2; len (maxPrefix (p,q)) < len p by A1, Th8; then len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) <= len p by A14, NAT_1:13; then dom ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) c= dom p by FINSEQ_3:30; then (maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*> c= p by A9, GRFUNC_1:2; then (maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*> c= maxPrefix (p,q) by A15, Def1; then len ((maxPrefix (p,q)) ^ <*(p . ((len (maxPrefix (p,q))) + 1))*>) <= len (maxPrefix (p,q)) by FINSEQ_1:63; then (len (maxPrefix (p,q))) + 1 <= len (maxPrefix (p,q)) by FINSEQ_2:16; hence contradiction by NAT_1:13; ::_thesis: verum end; begin theorem Th10: :: HELLY:10 for G being _Graph for W being Walk of G for m, n being Nat holds len (W .cut (m,n)) <= len W proof let G be _Graph; ::_thesis: for W being Walk of G for m, n being Nat holds len (W .cut (m,n)) <= len W let W be Walk of G; ::_thesis: for m, n being Nat holds len (W .cut (m,n)) <= len W let m, n be Nat; ::_thesis: len (W .cut (m,n)) <= len W reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def_12; percases ( ( m is odd & n is odd & m <= n & n <= len W ) or not m is odd or not n is odd or not m <= n or not n <= len W ) ; suppose ( m is odd & n is odd & m <= n & n <= len W ) ; ::_thesis: len (W .cut (m,n)) <= len W then W .cut (m,n) = (m,n) -cut W by GLIB_001:def_11; then len (W .cut (m9,n9)) <= len W by MSSCYC_1:8; hence len (W .cut (m,n)) <= len W ; ::_thesis: verum end; suppose ( not m is odd or not n is odd or not m <= n or not n <= len W ) ; ::_thesis: len (W .cut (m,n)) <= len W hence len (W .cut (m,n)) <= len W by GLIB_001:def_11; ::_thesis: verum end; end; end; theorem :: HELLY:11 for G being _Graph for W being Walk of G for m, n being Nat st not W .cut (m,n) is trivial holds not W is trivial proof let G be _Graph; ::_thesis: for W being Walk of G for m, n being Nat st not W .cut (m,n) is trivial holds not W is trivial let W be Walk of G; ::_thesis: for m, n being Nat st not W .cut (m,n) is trivial holds not W is trivial let m, n be Nat; ::_thesis: ( not W .cut (m,n) is trivial implies not W is trivial ) assume that A1: not W .cut (m,n) is trivial and A2: W is trivial ; ::_thesis: contradiction reconsider W = W as trivial Walk of G by A2; reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def_12; W .cut (m9,n9) is trivial ; hence contradiction by A1; ::_thesis: verum end; theorem Th12: :: HELLY:12 for G being _Graph for W being Walk of G for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds ex j being odd Nat st ( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W ) proof let G be _Graph; ::_thesis: for W being Walk of G for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds ex j being odd Nat st ( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W ) let W be Walk of G; ::_thesis: for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds ex j being odd Nat st ( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W ) let m, n, i be odd Nat; ::_thesis: ( m <= n & n <= len W & i <= len (W .cut (m,n)) implies ex j being odd Nat st ( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W ) ) assume that A1: m <= n and A2: n <= len W and A3: i <= len (W .cut (m,n)) ; ::_thesis: ex j being odd Nat st ( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W ) set j = (m + i) - 1; ( m >= 1 & i >= 1 ) by ABIAN:12; then m + i >= 1 + 1 by XREAL_1:7; then (m + i) - 1 >= (1 + 1) - 1 by XREAL_1:9; then (m + i) - 1 is odd Element of NAT by INT_1:3; then reconsider j = (m + i) - 1 as odd Nat ; take j ; ::_thesis: ( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W ) reconsider m9 = m, n9 = n as odd Element of NAT by ORDINAL1:def_12; i >= 1 by ABIAN:12; then i - 1 >= 1 - 1 by XREAL_1:9; then reconsider i1 = i - 1 as Element of NAT by INT_1:3; i < (len (W .cut (m,n))) + 1 by A3, NAT_1:13; then A4: i1 < ((len (W .cut (m,n))) + 1) - 1 by XREAL_1:9; thus (W .cut (m,n)) . i = (W .cut (m9,n9)) . (i1 + 1) .= W . (m + i1) by A1, A2, A4, GLIB_001:36 .= W . j ; ::_thesis: ( j = (m + i) - 1 & j <= len W ) thus j = (m + i) - 1 ; ::_thesis: j <= len W m + i <= (len (W .cut (m,n))) + m by A3, XREAL_1:7; then m9 + i <= n9 + 1 by A1, A2, GLIB_001:36; then (m + i) - 1 <= (n + 1) - 1 by XREAL_1:9; hence j <= len W by A2, XXREAL_0:2; ::_thesis: verum end; registration let G be _Graph; cluster -> non empty for Walk of G; correctness coherence for b1 being Walk of G holds not b1 is empty ; by CARD_1:27; end; theorem Th13: :: HELLY:13 for G being _Graph for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds W1 .vertices() c= W2 .vertices() proof let G be _Graph; ::_thesis: for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds W1 .vertices() c= W2 .vertices() let W1, W2 be Walk of G; ::_thesis: ( W1 is_a_prefix_of W2 implies W1 .vertices() c= W2 .vertices() ) assume A1: W1 c= W2 ; ::_thesis: W1 .vertices() c= W2 .vertices() let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W1 .vertices() or x in W2 .vertices() ) assume x in W1 .vertices() ; ::_thesis: x in W2 .vertices() then consider n being odd Element of NAT such that A2: n <= len W1 and A3: W1 . n = x by GLIB_001:87; 1 <= n by ABIAN:12; then n in dom W1 by A2, FINSEQ_3:25; then A4: W2 . n = x by A1, A3, GRFUNC_1:2; len W1 <= len W2 by A1, FINSEQ_1:63; then n <= len W2 by A2, XXREAL_0:2; hence x in W2 .vertices() by A4, GLIB_001:87; ::_thesis: verum end; theorem :: HELLY:14 for G being _Graph for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds W1 .edges() c= W2 .edges() proof let G be _Graph; ::_thesis: for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds W1 .edges() c= W2 .edges() let W1, W2 be Walk of G; ::_thesis: ( W1 is_a_prefix_of W2 implies W1 .edges() c= W2 .edges() ) assume A1: W1 c= W2 ; ::_thesis: W1 .edges() c= W2 .edges() let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W1 .edges() or x in W2 .edges() ) assume x in W1 .edges() ; ::_thesis: x in W2 .edges() then consider n being even Element of NAT such that A2: 1 <= n and A3: n <= len W1 and A4: W1 . n = x by GLIB_001:99; n in dom W1 by A2, A3, FINSEQ_3:25; then A5: W2 . n = x by A1, A4, GRFUNC_1:2; len W1 <= len W2 by A1, FINSEQ_1:63; then n <= len W2 by A3, XXREAL_0:2; hence x in W2 .edges() by A2, A5, GLIB_001:99; ::_thesis: verum end; theorem Th15: :: HELLY:15 for G being _Graph for W1, W2 being Walk of G holds W1 is_a_prefix_of W1 .append W2 proof let G be _Graph; ::_thesis: for W1, W2 being Walk of G holds W1 is_a_prefix_of W1 .append W2 let W1, W2 be Walk of G; ::_thesis: W1 is_a_prefix_of W1 .append W2 set W1a = W1 .append W2; percases ( W1 .last() = W2 .first() or W1 .last() <> W2 .first() ) ; suppose W1 .last() = W2 .first() ; ::_thesis: W1 is_a_prefix_of W1 .append W2 then len W1 <= len (W1 .append W2) by GLIB_001:29; then A1: dom W1 c= dom (W1 .append W2) by FINSEQ_3:30; for x being set st x in dom W1 holds W1 . x = (W1 .append W2) . x by GLIB_001:32; hence W1 is_a_prefix_of W1 .append W2 by A1, GRFUNC_1:2; ::_thesis: verum end; suppose W1 .last() <> W2 .first() ; ::_thesis: W1 is_a_prefix_of W1 .append W2 hence W1 is_a_prefix_of W1 .append W2 by GLIB_001:def_10; ::_thesis: verum end; end; end; theorem Th16: :: HELLY:16 for G being _Graph for W1, W2 being Walk of G st W1 is trivial & W1 .last() = W2 .first() holds W1 .append W2 = W2 proof let G be _Graph; ::_thesis: for W1, W2 being Walk of G st W1 is trivial & W1 .last() = W2 .first() holds W1 .append W2 = W2 let W1, W2 be Walk of G; ::_thesis: ( W1 is trivial & W1 .last() = W2 .first() implies W1 .append W2 = W2 ) assume that A1: W1 is trivial and A2: W1 .last() = W2 .first() ; ::_thesis: W1 .append W2 = W2 A3: len W1 = 1 by A1, GLIB_001:126; then A4: (len (W1 .append W2)) + 1 = 1 + (len W2) by A2, GLIB_001:28; now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_(W1_.append_W2)_holds_ (W1_.append_W2)_._k_=_W2_._k let k be Nat; ::_thesis: ( 1 <= k & k <= len (W1 .append W2) implies (W1 .append W2) . k = W2 . k ) assume that A5: 1 <= k and A6: k <= len (W1 .append W2) ; ::_thesis: (W1 .append W2) . k = W2 . k 1 - 1 <= k - 1 by A5, XREAL_1:9; then reconsider k1 = k - 1 as Element of NAT by INT_1:3; k - 1 < k by XREAL_1:44; then k - 1 < len W2 by A4, A6, XXREAL_0:2; then (W1 .append W2) . (1 + k1) = W2 . (k1 + 1) by A2, A3, GLIB_001:33; hence (W1 .append W2) . k = W2 . k ; ::_thesis: verum end; hence W1 .append W2 = W2 by A4, FINSEQ_1:14; ::_thesis: verum end; theorem Th17: :: HELLY:17 for G being _Graph for W1, W2 being Trail of G st W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() holds W1 .append W2 is Trail-like proof let G be _Graph; ::_thesis: for W1, W2 being Trail of G st W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() holds W1 .append W2 is Trail-like let W1, W2 be Trail of G; ::_thesis: ( W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() implies W1 .append W2 is Trail-like ) assume that A1: W1 .last() = W2 .first() and A2: W1 .edges() misses W2 .edges() ; ::_thesis: W1 .append W2 is Trail-like set W = W1 .append W2; now__::_thesis:_for_m,_n_being_even_Element_of_NAT_st_1_<=_m_&_m_<_n_&_n_<=_len_(W1_.append_W2)_holds_ (W1_.append_W2)_._m_<>_(W1_.append_W2)_._n let m, n be even Element of NAT ; ::_thesis: ( 1 <= m & m < n & n <= len (W1 .append W2) implies (W1 .append W2) . b1 <> (W1 .append W2) . b2 ) assume that A3: 1 <= m and A4: m < n and A5: n <= len (W1 .append W2) ; ::_thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2 1 <= n by A3, A4, XXREAL_0:2; then A6: n in dom (W1 .append W2) by A5, FINSEQ_3:25; m <= len (W1 .append W2) by A4, A5, XXREAL_0:2; then A7: m in dom (W1 .append W2) by A3, FINSEQ_3:25; percases ( n in dom W1 or ex k being Element of NAT st ( k < len W2 & n = (len W1) + k ) ) by A6, GLIB_001:34; supposeA8: n in dom W1 ; ::_thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2 then A9: n <= len W1 by FINSEQ_3:25; then m <= len W1 by A4, XXREAL_0:2; then m in dom W1 by A3, FINSEQ_3:25; then A10: W1 . m = (W1 .append W2) . m by GLIB_001:32; W1 . m <> W1 . n by A3, A4, A9, GLIB_001:138; hence (W1 .append W2) . m <> (W1 .append W2) . n by A8, A10, GLIB_001:32; ::_thesis: verum end; suppose ex k being Element of NAT st ( k < len W2 & n = (len W1) + k ) ; ::_thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2 then consider k being Element of NAT such that A11: k < len W2 and A12: n = (len W1) + k ; reconsider k = k as odd Element of NAT by A12; A13: (W1 .append W2) . n = W2 . (k + 1) by A1, A11, A12, GLIB_001:33; A14: k + 1 <= len W2 by A11, NAT_1:13; 1 <= k + 1 by NAT_1:11; then A15: W2 . (k + 1) in W2 .edges() by A14, GLIB_001:99; percases ( m in dom W1 or ex l being Element of NAT st ( l < len W2 & m = (len W1) + l ) ) by A7, GLIB_001:34; supposeA16: m in dom W1 ; ::_thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2 then ( 1 <= m & m <= len W1 ) by FINSEQ_3:25; then A17: W1 . m in W1 .edges() by GLIB_001:99; (W1 .append W2) . m = W1 . m by A16, GLIB_001:32; hence (W1 .append W2) . m <> (W1 .append W2) . n by A2, A13, A15, A17, XBOOLE_0:3; ::_thesis: verum end; suppose ex l being Element of NAT st ( l < len W2 & m = (len W1) + l ) ; ::_thesis: (W1 .append W2) . b1 <> (W1 .append W2) . b2 then consider l being Element of NAT such that A18: l < len W2 and A19: m = (len W1) + l ; reconsider l = l as odd Element of NAT by A19; l < k by A4, A12, A19, XREAL_1:6; then A20: ( 1 <= l + 1 & l + 1 < k + 1 ) by NAT_1:11, XREAL_1:6; (W1 .append W2) . m = W2 . (l + 1) by A1, A18, A19, GLIB_001:33; hence (W1 .append W2) . m <> (W1 .append W2) . n by A13, A14, A20, GLIB_001:138; ::_thesis: verum end; end; end; end; end; hence W1 .append W2 is Trail-like by GLIB_001:138; ::_thesis: verum end; theorem Th18: :: HELLY:18 for G being _Graph for P1, P2 being Path of G st P1 .last() = P2 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & ( P1 .first() in P2 .vertices() implies P1 .first() = P2 .last() ) & (P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} holds P1 .append P2 is Path-like proof let G be _Graph; ::_thesis: for P1, P2 being Path of G st P1 .last() = P2 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & ( P1 .first() in P2 .vertices() implies P1 .first() = P2 .last() ) & (P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} holds P1 .append P2 is Path-like let P1, P2 be Path of G; ::_thesis: ( P1 .last() = P2 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & ( P1 .first() in P2 .vertices() implies P1 .first() = P2 .last() ) & (P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} implies P1 .append P2 is Path-like ) assume that A1: P1 .last() = P2 .first() and A2: P1 is open and A3: P2 is open and A4: P1 .edges() misses P2 .edges() and A5: ( P1 .first() in P2 .vertices() implies P1 .first() = P2 .last() ) and A6: (P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} ; ::_thesis: P1 .append P2 is Path-like thus P1 .append P2 is Trail-like by A1, A4, Th17; :: according to GLIB_001:def_28 ::_thesis: for b1, b2 being Element of NAT holds ( b2 <= b1 or not b2 <= len (P1 .append P2) or not (P1 .append P2) . b1 = (P1 .append P2) . b2 or ( b1 = 1 & b2 = len (P1 .append P2) ) ) set P = P1 .append P2; let m, n be odd Element of NAT ; ::_thesis: ( n <= m or not n <= len (P1 .append P2) or not (P1 .append P2) . m = (P1 .append P2) . n or ( m = 1 & n = len (P1 .append P2) ) ) assume that A7: m < n and A8: n <= len (P1 .append P2) and A9: (P1 .append P2) . m = (P1 .append P2) . n and A10: ( m <> 1 or n <> len (P1 .append P2) ) ; ::_thesis: contradiction A11: 1 <= m by ABIAN:12; 1 <= n by ABIAN:12; then A12: n in dom (P1 .append P2) by A8, FINSEQ_3:25; m <= len (P1 .append P2) by A7, A8, XXREAL_0:2; then A13: m in dom (P1 .append P2) by A11, FINSEQ_3:25; percases ( ex k being Element of NAT st ( k < len P2 & n = (len P1) + k ) or n in dom P1 ) by A12, GLIB_001:34; suppose ex k being Element of NAT st ( k < len P2 & n = (len P1) + k ) ; ::_thesis: contradiction then consider k being Element of NAT such that A14: k < len P2 and A15: n = (len P1) + k ; A16: (P1 .append P2) . n = P2 . (k + 1) by A1, A14, A15, GLIB_001:33; reconsider k = k as even Element of NAT by A15; A17: k + 1 <= len P2 by A14, NAT_1:13; then A18: P2 . (k + 1) in P2 .vertices() by GLIB_001:87; percases ( ex k being Element of NAT st ( k < len P2 & m = (len P1) + k ) or m in dom P1 ) by A13, GLIB_001:34; suppose ex k being Element of NAT st ( k < len P2 & m = (len P1) + k ) ; ::_thesis: contradiction then consider l being Element of NAT such that A19: l < len P2 and A20: m = (len P1) + l ; A21: (P1 .append P2) . m = P2 . (l + 1) by A1, A19, A20, GLIB_001:33; l < k by A7, A15, A20, XREAL_1:6; then A22: l + 1 < k + 1 by XREAL_1:6; reconsider l = l as even Element of NAT by A20; l + 1 is odd ; then A23: P2 .last() = P2 . (k + 1) by A9, A16, A17, A21, A22, GLIB_001:def_28; P2 .first() = P2 . (l + 1) by A9, A16, A17, A21, A22, GLIB_001:def_28; hence contradiction by A3, A9, A16, A21, A23, GLIB_001:def_24; ::_thesis: verum end; supposeA24: m in dom P1 ; ::_thesis: contradiction set x = P1 . m; A25: P1 . m = (P1 .append P2) . m by A24, GLIB_001:32; A26: m <= len P1 by A24, FINSEQ_3:25; then P1 . m in P1 .vertices() by GLIB_001:87; then A27: P1 . m in (P1 .vertices()) /\ (P2 .vertices()) by A9, A16, A18, A25, XBOOLE_0:def_4; percases ( P1 . m = P1 .last() or P1 . m = P1 .first() ) by A6, A27, TARSKI:def_2; supposeA28: P1 . m = P1 .last() ; ::_thesis: contradiction A29: now__::_thesis:_not_m_<_len_P1 assume m < len P1 ; ::_thesis: contradiction then P1 .first() = P1 . m by A28, GLIB_001:def_28; hence contradiction by A2, A28, GLIB_001:def_24; ::_thesis: verum end; A30: now__::_thesis:_not_(2_*_0)_+_1_<_k_+_1 assume (2 * 0) + 1 < k + 1 ; ::_thesis: contradiction then P2 .first() = P2 .last() by A1, A9, A16, A17, A25, A28, GLIB_001:def_28; hence contradiction by A3, GLIB_001:def_24; ::_thesis: verum end; 1 <= k + 1 by NAT_1:11; then 1 = k + 1 by A30, XXREAL_0:1; hence contradiction by A7, A15, A29; ::_thesis: verum end; supposeA31: P1 . m = P1 .first() ; ::_thesis: contradiction then A32: P1 . m = P1 . ((2 * 0) + 1) ; A33: now__::_thesis:_not_m_<>_1 assume m <> 1 ; ::_thesis: contradiction then 1 < m by A11, XXREAL_0:1; then P1 . m = P1 .last() by A26, A32, GLIB_001:def_28; hence contradiction by A2, A31, GLIB_001:def_24; ::_thesis: verum end; now__::_thesis:_not_k_+_1_=_len_P2 assume k + 1 = len P2 ; ::_thesis: contradiction then (len (P1 .append P2)) + 1 = (len P1) + (k + 1) by A1, GLIB_001:28; hence contradiction by A10, A15, A33; ::_thesis: verum end; then A34: k + 1 < len P2 by A17, XXREAL_0:1; P2 . (k + 1) = P2 .last() by A5, A9, A16, A18, A24, A31, GLIB_001:32; then P2 .first() = P2 .last() by A34, GLIB_001:def_28; hence contradiction by A3, GLIB_001:def_24; ::_thesis: verum end; end; end; end; end; supposeA35: n in dom P1 ; ::_thesis: contradiction then A36: n <= len P1 by FINSEQ_3:25; then ( 1 <= m & m <= len P1 ) by A7, ABIAN:12, XXREAL_0:2; then m in dom P1 by FINSEQ_3:25; then A37: P1 . m = (P1 .append P2) . m by GLIB_001:32 .= P1 . n by A9, A35, GLIB_001:32 ; then m = 1 by A7, A36, GLIB_001:def_28; then P1 .first() = P1 .last() by A7, A36, A37, GLIB_001:def_28; hence contradiction by A2, GLIB_001:def_24; ::_thesis: verum end; end; end; theorem Th19: :: HELLY:19 for G being _Graph for P1, P2 being Path of G st P1 .last() = P2 .first() & P1 is open & P2 is open & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} holds ( P1 .append P2 is open & P1 .append P2 is Path-like ) proof let G be _Graph; ::_thesis: for P1, P2 being Path of G st P1 .last() = P2 .first() & P1 is open & P2 is open & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} holds ( P1 .append P2 is open & P1 .append P2 is Path-like ) let P1, P2 be Path of G; ::_thesis: ( P1 .last() = P2 .first() & P1 is open & P2 is open & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} implies ( P1 .append P2 is open & P1 .append P2 is Path-like ) ) assume that A1: P1 .last() = P2 .first() and A2: P1 is open and A3: P2 is open and A4: (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} ; ::_thesis: ( P1 .append P2 is open & P1 .append P2 is Path-like ) set P = P1 .append P2; thus P1 .append P2 is open ::_thesis: P1 .append P2 is Path-like proof assume A5: (P1 .append P2) .first() = (P1 .append P2) .last() ; :: according to GLIB_001:def_24 ::_thesis: contradiction ( (P1 .append P2) .first() = P1 .first() & (P1 .append P2) .last() = P2 .last() ) by A1, GLIB_001:30; then ( P1 .first() in P1 .vertices() & P1 .first() in P2 .vertices() ) by A5, GLIB_001:88; then P1 .first() in {(P1 .last())} by A4, XBOOLE_0:def_4; then P1 .first() = P1 .last() by TARSKI:def_1; hence contradiction by A2, GLIB_001:def_24; ::_thesis: verum end; A6: now__::_thesis:_not_P1_.first()_in_P2_.vertices() A7: P1 .first() in P1 .vertices() by GLIB_001:88; assume P1 .first() in P2 .vertices() ; ::_thesis: contradiction then P1 .first() in {(P1 .last())} by A4, A7, XBOOLE_0:def_4; then P1 .first() = P1 .last() by TARSKI:def_1; hence contradiction by A2, GLIB_001:def_24; ::_thesis: verum end; A8: P1 .edges() misses P2 .edges() proof assume (P1 .edges()) /\ (P2 .edges()) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being set such that A9: x in (P1 .edges()) /\ (P2 .edges()) by XBOOLE_0:def_1; x in P2 .edges() by A9, XBOOLE_0:def_4; then consider u1, u2 being Vertex of G, m being odd Element of NAT such that A10: m + 2 <= len P2 and A11: u1 = P2 . m and x = P2 . (m + 1) and A12: u2 = P2 . (m + 2) and A13: x Joins u1,u2,G by GLIB_001:103; x in P1 .edges() by A9, XBOOLE_0:def_4; then consider v1, v2 being Vertex of G, n being odd Element of NAT such that A14: n + 2 <= len P1 and A15: v1 = P1 . n and x = P1 . (n + 1) and A16: v2 = P1 . (n + 2) and A17: x Joins v1,v2,G by GLIB_001:103; A18: n + 0 < n + 2 by XREAL_1:8; percases ( v1 <> v2 or v1 = v2 ) ; supposeA19: v1 <> v2 ; ::_thesis: contradiction n <= len P1 by A14, A18, XXREAL_0:2; then A20: v1 in P1 .vertices() by A15, GLIB_001:87; v2 in P1 .vertices() by A14, A16, GLIB_001:87; then A21: {v1,v2} c= P1 .vertices() by A20, ZFMISC_1:32; m + 0 < m + 2 by XREAL_1:8; then m <= len P2 by A10, XXREAL_0:2; then A22: u1 in P2 .vertices() by A11, GLIB_001:87; u2 in P2 .vertices() by A10, A12, GLIB_001:87; then A23: {u1,u2} c= P2 .vertices() by A22, ZFMISC_1:32; A24: ( ( v1 = u1 & v2 = u2 ) or ( v1 = u2 & v2 = u1 ) ) by A17, A13, GLIB_000:15; then v1 = P1 .last() by A4, A21, A23, XBOOLE_1:19, ZFMISC_1:20; hence contradiction by A4, A19, A24, A21, A23, XBOOLE_1:19, ZFMISC_1:20; ::_thesis: verum end; supposeA25: v1 = v2 ; ::_thesis: contradiction then P1 .first() = v1 by A14, A15, A16, A18, GLIB_001:def_28 .= P1 .last() by A14, A15, A16, A18, A25, GLIB_001:def_28 ; hence contradiction by A2, GLIB_001:def_24; ::_thesis: verum end; end; end; (P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} by A4, ZFMISC_1:7; hence P1 .append P2 is Path-like by A1, A2, A3, A8, A6, Th18; ::_thesis: verum end; theorem Th20: :: HELLY:20 for G being _Graph for P1, P2 being Path of G st P1 .last() = P2 .first() & P2 .last() = P1 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last()),(P1 .first())} holds P1 .append P2 is Cycle-like proof let G be _Graph; ::_thesis: for P1, P2 being Path of G st P1 .last() = P2 .first() & P2 .last() = P1 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last()),(P1 .first())} holds P1 .append P2 is Cycle-like let P1, P2 be Path of G; ::_thesis: ( P1 .last() = P2 .first() & P2 .last() = P1 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last()),(P1 .first())} implies P1 .append P2 is Cycle-like ) assume that A1: P1 .last() = P2 .first() and A2: P2 .last() = P1 .first() and A3: P1 is open and A4: ( P2 is open & P1 .edges() misses P2 .edges() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last()),(P1 .first())} ) ; ::_thesis: P1 .append P2 is Cycle-like set P = P1 .append P2; ( (P1 .append P2) .first() = P1 .first() & (P1 .append P2) .last() = P2 .last() ) by A1, GLIB_001:30; hence P1 .append P2 is closed by A2, GLIB_001:def_24; :: according to GLIB_001:def_31 ::_thesis: ( P1 .append P2 is Path-like & not P1 .append P2 is trivial ) thus P1 .append P2 is Path-like by A1, A2, A3, A4, Th18; ::_thesis: not P1 .append P2 is trivial P1 .first() <> P1 .last() by A3, GLIB_001:def_24; then not P1 is trivial by GLIB_001:127; then A5: len P1 >= 3 by GLIB_001:125; len (P1 .append P2) >= len P1 by A1, GLIB_001:29; then len (P1 .append P2) >= 3 by A5, XXREAL_0:2; hence not P1 .append P2 is trivial by GLIB_001:125; ::_thesis: verum end; theorem :: HELLY:21 for G being simple _Graph for W1, W2 being Walk of G for k being odd Nat st k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds W1 . j = W2 . j ) holds for j being Nat st 1 <= j & j <= k holds W1 . j = W2 . j proof let G be simple _Graph; ::_thesis: for W1, W2 being Walk of G for k being odd Nat st k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds W1 . j = W2 . j ) holds for j being Nat st 1 <= j & j <= k holds W1 . j = W2 . j let W1, W2 be Walk of G; ::_thesis: for k being odd Nat st k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds W1 . j = W2 . j ) holds for j being Nat st 1 <= j & j <= k holds W1 . j = W2 . j let k be odd Nat; ::_thesis: ( k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds W1 . j = W2 . j ) implies for j being Nat st 1 <= j & j <= k holds W1 . j = W2 . j ) assume that A1: k <= len W1 and A2: k <= len W2 and A3: for j being odd Nat st j <= k holds W1 . j = W2 . j ; ::_thesis: for j being Nat st 1 <= j & j <= k holds W1 . j = W2 . j let j be Nat; ::_thesis: ( 1 <= j & j <= k implies W1 . j = W2 . j ) assume that A4: 1 <= j and A5: j <= k ; ::_thesis: W1 . j = W2 . j percases ( j is odd or j is even ) ; suppose j is odd ; ::_thesis: W1 . j = W2 . j hence W1 . j = W2 . j by A3, A5; ::_thesis: verum end; suppose j is even ; ::_thesis: W1 . j = W2 . j then reconsider j9 = j as even Nat ; 1 - 1 <= j - 1 by A4, XREAL_1:9; then reconsider j1 = j9 - 1 as odd Element of NAT by INT_1:3; A6: j1 < j by XREAL_1:44; j <= len W1 by A1, A5, XXREAL_0:2; then j1 < len W1 by A6, XXREAL_0:2; then A7: W1 . (j1 + 1) Joins W1 . j1,W1 . (j1 + 2),G by GLIB_001:def_3; j1 + 1 < k by A5, XXREAL_0:1; then (j1 + 1) + 1 <= k by NAT_1:13; then A8: W1 . (j1 + 2) = W2 . (j1 + 2) by A3; j <= len W2 by A2, A5, XXREAL_0:2; then j1 < len W2 by A6, XXREAL_0:2; then A9: W2 . (j1 + 1) Joins W2 . j1,W2 . (j1 + 2),G by GLIB_001:def_3; W1 . j1 = W2 . j1 by A3, A5, A6, XXREAL_0:2; hence W1 . j = W2 . j by A7, A9, A8, GLIB_000:def_20; ::_thesis: verum end; end; end; theorem Th22: :: HELLY:22 for G being _Graph for W1, W2 being Walk of G st W1 .first() = W2 .first() holds len (maxPrefix (W1,W2)) is odd proof let G be _Graph; ::_thesis: for W1, W2 being Walk of G st W1 .first() = W2 .first() holds len (maxPrefix (W1,W2)) is odd let W1, W2 be Walk of G; ::_thesis: ( W1 .first() = W2 .first() implies len (maxPrefix (W1,W2)) is odd ) assume that A1: W1 .first() = W2 .first() and A2: len (maxPrefix (W1,W2)) is even ; ::_thesis: contradiction set dI = len (maxPrefix (W1,W2)); reconsider dIp = (len (maxPrefix (W1,W2))) - 1 as odd Element of NAT by A1, A2, Th5, INT_1:5; A3: dIp < len (maxPrefix (W1,W2)) by XREAL_1:146; set mP = maxPrefix (W1,W2); set lmP = (maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>; A4: len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) = (len (maxPrefix (W1,W2))) + 1 by FINSEQ_2:16; A5: now__::_thesis:_for_x_being_set_st_x_in_dom_((maxPrefix_(W1,W2))_^_<*(W1_._((len_(maxPrefix_(W1,W2)))_+_1))*>)_holds_ ((maxPrefix_(W1,W2))_^_<*(W1_._((len_(maxPrefix_(W1,W2)))_+_1))*>)_._x_=_W1_._x let x be set ; ::_thesis: ( x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) implies ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W1 . b1 ) assume A6: x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) ; ::_thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W1 . b1 reconsider n = x as Nat by A6; A7: 1 <= n by A6, FINSEQ_3:25; n <= len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) by A6, FINSEQ_3:25; then A8: n <= (len (maxPrefix (W1,W2))) + 1 by FINSEQ_2:16; percases ( n <= len (maxPrefix (W1,W2)) or n = (len (maxPrefix (W1,W2))) + 1 ) by A8, NAT_1:8; supposeA9: n <= len (maxPrefix (W1,W2)) ; ::_thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W1 . b1 then n in dom (maxPrefix (W1,W2)) by A7, FINSEQ_3:25; hence ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = (maxPrefix (W1,W2)) . x by FINSEQ_1:def_7 .= W1 . x by A9, Th6 ; ::_thesis: verum end; suppose n = (len (maxPrefix (W1,W2))) + 1 ; ::_thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W1 . b1 hence ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = W1 . x by FINSEQ_1:42; ::_thesis: verum end; end; end; A10: len (maxPrefix (W1,W2)) = dIp + 1 ; A11: len (maxPrefix (W1,W2)) <= len W2 by Th3; then dIp < len W2 by XREAL_1:146, XXREAL_0:2; then A12: W2 . (len (maxPrefix (W1,W2))) Joins W2 . dIp,W2 . (dIp + 2),G by A10, GLIB_001:def_3; A13: len (maxPrefix (W1,W2)) <= len W1 by Th3; then dIp < len W1 by XREAL_1:146, XXREAL_0:2; then A14: W1 . (len (maxPrefix (W1,W2))) Joins W1 . dIp,W1 . (dIp + 2),G by A10, GLIB_001:def_3; W1 . (len (maxPrefix (W1,W2))) = W2 . (len (maxPrefix (W1,W2))) by Th7; then A15: ( ( W1 . dIp = W2 . dIp & W1 . (dIp + 2) = W2 . (dIp + 2) ) or ( W1 . dIp = W2 . (dIp + 2) & W1 . (dIp + 2) = W2 . dIp ) ) by A14, A12, GLIB_000:15; A16: now__::_thesis:_for_x_being_set_st_x_in_dom_((maxPrefix_(W1,W2))_^_<*(W1_._((len_(maxPrefix_(W1,W2)))_+_1))*>)_holds_ ((maxPrefix_(W1,W2))_^_<*(W1_._((len_(maxPrefix_(W1,W2)))_+_1))*>)_._x_=_W2_._x let x be set ; ::_thesis: ( x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) implies ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W2 . b1 ) assume A17: x in dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) ; ::_thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W2 . b1 reconsider n = x as Nat by A17; A18: 1 <= n by A17, FINSEQ_3:25; n <= len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) by A17, FINSEQ_3:25; then A19: n <= (len (maxPrefix (W1,W2))) + 1 by FINSEQ_2:16; percases ( n <= len (maxPrefix (W1,W2)) or n = (len (maxPrefix (W1,W2))) + 1 ) by A19, NAT_1:8; supposeA20: n <= len (maxPrefix (W1,W2)) ; ::_thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W2 . b1 then n in dom (maxPrefix (W1,W2)) by A18, FINSEQ_3:25; hence ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = (maxPrefix (W1,W2)) . x by FINSEQ_1:def_7 .= W2 . x by A20, Th6 ; ::_thesis: verum end; supposeA21: n = (len (maxPrefix (W1,W2))) + 1 ; ::_thesis: ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . b1 = W2 . b1 hence ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) . x = W1 . ((len (maxPrefix (W1,W2))) + 1) by FINSEQ_1:42 .= W2 . x by A3, A15, A21, Th7 ; ::_thesis: verum end; end; end; len (maxPrefix (W1,W2)) < len W2 by A2, A11, XXREAL_0:1; then len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) <= len W2 by A4, NAT_1:13; then dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) c= dom W2 by FINSEQ_3:30; then A22: (maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*> c= W2 by A16, GRFUNC_1:2; len (maxPrefix (W1,W2)) < len W1 by A2, A13, XXREAL_0:1; then len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) <= len W1 by A4, NAT_1:13; then dom ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) c= dom W1 by FINSEQ_3:30; then (maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*> c= W1 by A5, GRFUNC_1:2; then (maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*> c= maxPrefix (W1,W2) by A22, Def1; then len ((maxPrefix (W1,W2)) ^ <*(W1 . ((len (maxPrefix (W1,W2))) + 1))*>) <= len (maxPrefix (W1,W2)) by FINSEQ_1:63; then (len (maxPrefix (W1,W2))) + 1 <= len (maxPrefix (W1,W2)) by FINSEQ_2:16; hence contradiction by NAT_1:13; ::_thesis: verum end; theorem Th23: :: HELLY:23 for G being _Graph for W1, W2 being Walk of G st W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 holds (len (maxPrefix (W1,W2))) + 2 <= len W1 proof let G be _Graph; ::_thesis: for W1, W2 being Walk of G st W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 holds (len (maxPrefix (W1,W2))) + 2 <= len W1 let W1, W2 be Walk of G; ::_thesis: ( W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 implies (len (maxPrefix (W1,W2))) + 2 <= len W1 ) assume ( W1 .first() = W2 .first() & not W1 c= W2 ) ; ::_thesis: (len (maxPrefix (W1,W2))) + 2 <= len W1 then ( len (maxPrefix (W1,W2)) < len W1 & len (maxPrefix (W1,W2)) is odd Nat ) by Th8, Th22; hence (len (maxPrefix (W1,W2))) + 2 <= len W1 by CHORD:4; ::_thesis: verum end; theorem Th24: :: HELLY:24 for G being non-multi _Graph for W1, W2 being Walk of G st W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 & not W2 is_a_prefix_of W1 holds W1 . ((len (maxPrefix (W1,W2))) + 2) <> W2 . ((len (maxPrefix (W1,W2))) + 2) proof let G be non-multi _Graph; ::_thesis: for W1, W2 being Walk of G st W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 & not W2 is_a_prefix_of W1 holds W1 . ((len (maxPrefix (W1,W2))) + 2) <> W2 . ((len (maxPrefix (W1,W2))) + 2) let W1, W2 be Walk of G; ::_thesis: ( W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 & not W2 is_a_prefix_of W1 implies W1 . ((len (maxPrefix (W1,W2))) + 2) <> W2 . ((len (maxPrefix (W1,W2))) + 2) ) assume that A1: W1 .first() = W2 .first() and A2: not W1 c= W2 and A3: not W2 c= W1 and A4: W1 . ((len (maxPrefix (W1,W2))) + 2) = W2 . ((len (maxPrefix (W1,W2))) + 2) ; ::_thesis: contradiction set dI = len (maxPrefix (W1,W2)); A5: len (maxPrefix (W1,W2)) is odd by A1, Th22; len (maxPrefix (W1,W2)) < len W1 by A2, Th8; then A6: W1 . ((len (maxPrefix (W1,W2))) + 1) Joins W1 . (len (maxPrefix (W1,W2))),W1 . ((len (maxPrefix (W1,W2))) + 2),G by A5, GLIB_001:def_3; A7: W1 . (len (maxPrefix (W1,W2))) = W2 . (len (maxPrefix (W1,W2))) by Th7; len (maxPrefix (W1,W2)) < len W2 by A3, Th8; then A8: W2 . ((len (maxPrefix (W1,W2))) + 1) Joins W2 . (len (maxPrefix (W1,W2))),W2 . ((len (maxPrefix (W1,W2))) + 2),G by A5, GLIB_001:def_3; W1 . ((len (maxPrefix (W1,W2))) + 1) <> W2 . ((len (maxPrefix (W1,W2))) + 1) by A2, A3, Th9; hence contradiction by A4, A7, A6, A8, GLIB_000:def_20; ::_thesis: verum end; begin definition mode _Tree is Tree-like _Graph; let G be _Graph; mode _Subtree of G is Tree-like Subgraph of G; end; registration let T be _Tree; cluster Trail-like -> Path-like for Walk of T; correctness coherence for b1 being Walk of T st b1 is Trail-like holds b1 is Path-like ; proof let W be Walk of T; ::_thesis: ( W is Trail-like implies W is Path-like ) assume A1: W is Trail-like ; ::_thesis: W is Path-like defpred S1[ Nat] means ( T is odd & T <= len W & ex k being odd Element of NAT st ( k < T & W . k = W . T ) ); assume not W is Path-like ; ::_thesis: contradiction then ex m, n being odd Element of NAT st ( m < n & n <= len W & W . m = W . n & ( m <> 1 or n <> len W ) ) by A1, GLIB_001:def_28; then A2: ex p being Nat st S1[p] ; consider p being Nat such that A3: S1[p] and A4: for r being Nat st S1[r] holds p <= r from NAT_1:sch_5(A2); reconsider P = p as Element of NAT by ORDINAL1:def_12; consider k being odd Element of NAT such that A5: k < p and p <= len W and A6: W . k = W . p by A3; set Wc = W .cut (k,P); (len (W .cut (k,P))) + k = P + 1 by A3, A5, GLIB_001:36; then len (W .cut (k,P)) <> 1 by A5; then A7: not W .cut (k,P) is trivial by GLIB_001:126; A8: (W .cut (k,P)) .last() = W . p by A3, A5, GLIB_001:37; A9: W .cut (k,P) is Path-like proof assume not W .cut (k,P) is Path-like ; ::_thesis: contradiction then consider m, n being odd Element of NAT such that A10: m < n and A11: n <= len (W .cut (k,P)) and A12: (W .cut (k,P)) . m = (W .cut (k,P)) . n and A13: ( m <> 1 or n <> len (W .cut (k,P)) ) by A1, GLIB_001:def_28; A14: m < len (W .cut (k,P)) by A10, A11, XXREAL_0:2; consider kn1 being odd Nat such that A15: (W .cut (k,P)) . n = W . kn1 and A16: kn1 = (k + n) - 1 and A17: kn1 <= len W by A3, A5, A11, Th12; reconsider kn1 = kn1 as odd Element of NAT by ORDINAL1:def_12; A18: 1 <= m by ABIAN:12; m <= len (W .cut (k,P)) by A10, A11, XXREAL_0:2; then consider km1 being odd Nat such that A19: (W .cut (k,P)) . m = W . km1 and A20: km1 = (k + m) - 1 and A21: km1 <= len W by A3, A5, Th12; reconsider km1 = km1 as odd Element of NAT by ORDINAL1:def_12; percases ( n < len (W .cut (k,P)) or n = len (W .cut (k,P)) ) by A11, XXREAL_0:1; suppose n < len (W .cut (k,P)) ; ::_thesis: contradiction then k + n < k + (len (W .cut (k,P))) by XREAL_1:6; then k + n < p + 1 by A3, A5, GLIB_001:36; then A22: kn1 < p by A16, XREAL_1:19; k + m < k + n by A10, XREAL_1:6; then km1 < kn1 by A20, A16, XREAL_1:9; hence contradiction by A4, A12, A19, A15, A17, A22; ::_thesis: verum end; supposeA23: n = len (W .cut (k,P)) ; ::_thesis: contradiction k + m < (len (W .cut (k,P))) + k by A14, XREAL_1:6; then k + m < p + 1 by A3, A5, GLIB_001:36; then A24: km1 < p by A20, XREAL_1:19; 1 < m by A13, A18, A23, XXREAL_0:1; then k + 1 < k + m by XREAL_1:6; then k < km1 by A20, XREAL_1:20; hence contradiction by A4, A6, A8, A12, A19, A21, A23, A24; ::_thesis: verum end; end; end; (W .cut (k,P)) .first() = W . k by A3, A5, GLIB_001:37; then W .cut (k,P) is closed by A6, A8, GLIB_001:def_24; then W .cut (k,P) is Cycle-like by A7, A9, GLIB_001:def_31; hence contradiction by GLIB_002:def_2; ::_thesis: verum end; end; theorem Th25: :: HELLY:25 for T being _Tree for P being Path of T st not P is trivial holds P is open proof let T be _Tree; ::_thesis: for P being Path of T st not P is trivial holds P is open let P be Path of T; ::_thesis: ( not P is trivial implies P is open ) assume ( not P is trivial & not P is open ) ; ::_thesis: contradiction then P is Cycle-like by GLIB_001:def_31; hence contradiction by GLIB_002:def_2; ::_thesis: verum end; registration let T be _Tree; cluster non trivial Path-like -> open for Walk of T; correctness coherence for b1 being Path of T st not b1 is trivial holds b1 is open ; by Th25; end; theorem Th26: :: HELLY:26 for T being _Tree for P being Path of T for i, j being odd Nat st i < j & j <= len P holds P . i <> P . j proof let T be _Tree; ::_thesis: for P being Path of T for i, j being odd Nat st i < j & j <= len P holds P . i <> P . j let P be Path of T; ::_thesis: for i, j being odd Nat st i < j & j <= len P holds P . i <> P . j let i, j be odd Nat; ::_thesis: ( i < j & j <= len P implies P . i <> P . j ) assume that A1: i < j and A2: j <= len P and A3: P . i = P . j ; ::_thesis: contradiction reconsider i = i, j = j as odd Element of NAT by ORDINAL1:def_12; A4: i < j by A1; then A5: i = 1 by A2, A3, GLIB_001:def_28; then A6: not P is trivial by A1, A2, GLIB_001:126; P .first() = P .last() by A2, A3, A4, A5, GLIB_001:def_28; hence contradiction by A6, GLIB_001:def_24; ::_thesis: verum end; theorem Th27: :: HELLY:27 for T being _Tree for a, b being Vertex of T for P1, P2 being Path of T st P1 is_Walk_from a,b & P2 is_Walk_from a,b holds P1 = P2 proof let T be _Tree; ::_thesis: for a, b being Vertex of T for P1, P2 being Path of T st P1 is_Walk_from a,b & P2 is_Walk_from a,b holds P1 = P2 let a, b be Vertex of T; ::_thesis: for P1, P2 being Path of T st P1 is_Walk_from a,b & P2 is_Walk_from a,b holds P1 = P2 let P1, P2 be Path of T; ::_thesis: ( P1 is_Walk_from a,b & P2 is_Walk_from a,b implies P1 = P2 ) assume that A1: P1 is_Walk_from a,b and A2: P2 is_Walk_from a,b ; ::_thesis: P1 = P2 set di = len (maxPrefix (P1,P2)); A3: ( P1 .first() = a & P2 .first() = a ) by A1, A2, GLIB_001:def_23; then reconsider di = len (maxPrefix (P1,P2)) as odd Element of NAT by Th22; defpred S1[ Nat] means ( $1 is odd & di < $1 & $1 <= len P2 & P2 . $1 in P1 .vertices() ); assume A4: P1 <> P2 ; ::_thesis: contradiction A5: not P2 c= P1 proof assume A6: P2 c= P1 ; ::_thesis: contradiction then len P2 <= len P1 by FINSEQ_1:63; then A7: len P2 < len P1 by A4, A6, FINSEQ_2:129, XXREAL_0:1; 1 <= len P2 by ABIAN:12; then len P2 in dom P2 by FINSEQ_3:25; then A8: P2 . (len P2) = P1 . (len P2) by A6, GRFUNC_1:2; A9: P1 . (len P1) = P1 .last() .= b by A1, GLIB_001:def_23 ; P2 . (len P2) = P2 .last() .= b by A2, GLIB_001:def_23 ; hence contradiction by A7, A8, A9, Th26; ::_thesis: verum end; A10: ex k being Nat st S1[k] proof take k = len P2; ::_thesis: S1[k] thus k is odd ; ::_thesis: ( di < k & k <= len P2 & P2 . k in P1 .vertices() ) ( di + 2 <= len P2 & di < di + 2 ) by A3, A5, Th23, NAT_1:19; hence di < k by XXREAL_0:2; ::_thesis: ( k <= len P2 & P2 . k in P1 .vertices() ) thus k <= len P2 ; ::_thesis: P2 . k in P1 .vertices() P2 . k = P2 .last() .= b by A2, GLIB_001:def_23 .= P1 .last() by A1, GLIB_001:def_23 ; hence P2 . k in P1 .vertices() by GLIB_001:88; ::_thesis: verum end; consider ei being Nat such that A11: S1[ei] and A12: for n being Nat st S1[n] holds ei <= n from NAT_1:sch_5(A10); reconsider ei = ei as odd Element of NAT by A11, ORDINAL1:def_12; set e = P2 . ei; set fi = P1 .find (P2 . ei); set pde = P2 .cut (di,ei); set pdf = P1 .cut (di,(P1 .find (P2 . ei))); A13: P1 .find (P2 . ei) <= len P1 by A11, GLIB_001:def_19; set rpdf = (P1 .cut (di,(P1 .find (P2 . ei)))) .reverse() ; A14: ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() = (P1 .cut (di,(P1 .find (P2 . ei)))) .vertices() by GLIB_001:92; set C = (P2 .cut (di,ei)) .append ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()); set d = P1 . di; A15: P2 . di = P1 . di by Th7; then A16: (P2 .cut (di,ei)) .first() = P1 . di by A11, GLIB_001:37; A17: P2 . ei = P1 . (P1 .find (P2 . ei)) by A11, GLIB_001:def_19; len P2 <> 1 proof assume len P2 = 1 ; ::_thesis: contradiction then di < 1 by A11, XXREAL_0:2; hence contradiction by ABIAN:12; ::_thesis: verum end; then A18: not P2 is trivial by GLIB_001:126; A19: di < P1 .find (P2 . ei) proof assume di >= P1 .find (P2 . ei) ; ::_thesis: contradiction then ( P1 . (P1 .find (P2 . ei)) = P2 . (P1 .find (P2 . ei)) & ei > P1 .find (P2 . ei) ) by A11, Th7, XXREAL_0:2; then ( P2 .first() = P2 . ei & P2 .last() = P2 . ei ) by A11, A17, GLIB_001:def_28; hence contradiction by A18, GLIB_001:def_24; ::_thesis: verum end; then A20: not P1 .cut (di,(P1 .find (P2 . ei))) is trivial by A13, GLIB_001:131; then A21: not P1 is trivial ; P1 .find (P2 . ei) <= len P1 by A11, GLIB_001:def_19; then A22: ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() c= P1 .vertices() by A19, A14, GLIB_001:94; A23: ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) c= {(P2 . ei),(P1 . di)} proof assume not ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) c= {(P2 . ei),(P1 . di)} ; ::_thesis: contradiction then consider g being set such that A24: g in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) and A25: not g in {(P2 . ei),(P1 . di)} by TARSKI:def_3; g in (P2 .cut (di,ei)) .vertices() by A24, XBOOLE_0:def_4; then consider gii being odd Element of NAT such that A26: gii <= len (P2 .cut (di,ei)) and A27: (P2 .cut (di,ei)) . gii = g by GLIB_001:87; consider gi being odd Nat such that A28: P2 . gi = (P2 .cut (di,ei)) . gii and A29: gi = (di + gii) - 1 and A30: gi <= len P2 by A11, A26, Th12; reconsider gi = gi as odd Element of NAT by ORDINAL1:def_12; A31: gii >= 1 by ABIAN:12; A32: gi < ei proof A33: (len (P2 .cut (di,ei))) + di = ei + 1 by A11, GLIB_001:36; assume A34: gi >= ei ; ::_thesis: contradiction percases ( gi = ei or gi > ei ) by A34, XXREAL_0:1; suppose gi = ei ; ::_thesis: contradiction then (P2 .cut (di,ei)) . gii = (P2 .cut (di,ei)) .last() by A29, A33 .= P2 . ei by A11, GLIB_001:37 ; hence contradiction by A25, A27, TARSKI:def_2; ::_thesis: verum end; suppose gi > ei ; ::_thesis: contradiction then gi + 1 > ei + 1 by XREAL_1:6; hence contradiction by A26, A29, A33, XREAL_1:6; ::_thesis: verum end; end; end; gii <> 1 by A16, A25, A27, TARSKI:def_2; then A35: gii > 1 by A31, XXREAL_0:1; A36: di < gi proof assume di >= gi ; ::_thesis: contradiction then di + gii > gi + 1 by A35, XREAL_1:8; hence contradiction by A29; ::_thesis: verum end; g in ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() by A24, XBOOLE_0:def_4; hence contradiction by A12, A22, A27, A28, A30, A36, A32; ::_thesis: verum end; A37: (P2 .cut (di,ei)) .last() = P2 . ei by A11, GLIB_001:37; (P1 .cut (di,(P1 .find (P2 . ei)))) .first() = P1 . di by A13, A19, GLIB_001:37; then A38: ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .last() = P1 . di by GLIB_001:22; (P1 .cut (di,(P1 .find (P2 . ei)))) .last() = P2 . ei by A13, A17, A19, GLIB_001:37; then A39: ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .first() = P2 . ei by GLIB_001:22; {(P2 . ei),(P1 . di)} c= ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(P2 . ei),(P1 . di)} or x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) ) assume A40: x in {(P2 . ei),(P1 . di)} ; ::_thesis: x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) percases ( x = P2 . ei or x = P1 . di ) by A40, TARSKI:def_2; suppose x = P2 . ei ; ::_thesis: x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) then ( x in (P2 .cut (di,ei)) .vertices() & x in ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() ) by A37, A39, GLIB_001:88; hence x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) by XBOOLE_0:def_4; ::_thesis: verum end; suppose x = P1 . di ; ::_thesis: x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) then ( x in (P2 .cut (di,ei)) .vertices() & x in ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() ) by A16, A38, GLIB_001:88; hence x in ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) by XBOOLE_0:def_4; ::_thesis: verum end; end; end; then A41: ((P2 .cut (di,ei)) .vertices()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices()) = {(P2 . ei),(P1 . di)} by A23, XBOOLE_0:def_10; A42: not P2 .cut (di,ei) is trivial by A11, GLIB_001:131; then A43: not P2 is trivial ; A44: not P1 c= P2 proof assume A45: P1 c= P2 ; ::_thesis: contradiction then len P1 <= len P2 by FINSEQ_1:63; then A46: len P1 < len P2 by A4, A45, FINSEQ_2:129, XXREAL_0:1; 1 <= len P1 by ABIAN:12; then len P1 in dom P1 by FINSEQ_3:25; then A47: P1 . (len P1) = P2 . (len P1) by A45, GRFUNC_1:2; A48: P2 . (len P2) = P2 .last() .= b by A2, GLIB_001:def_23 ; P1 . (len P1) = P1 .last() .= b by A1, GLIB_001:def_23 ; hence contradiction by A46, A47, A48, Th26; ::_thesis: verum end; A49: (P2 .cut (di,ei)) .edges() misses ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges() proof A50: (P1 .cut (di,(P1 .find (P2 . ei)))) .vertices() = ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() by GLIB_001:92; A51: (P1 .cut (di,(P1 .find (P2 . ei)))) .edges() = ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges() by GLIB_001:107; assume ((P2 .cut (di,ei)) .edges()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges()) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being set such that A52: x in ((P2 .cut (di,ei)) .edges()) /\ (((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges()) by XBOOLE_0:def_1; x in ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .edges() by A52, XBOOLE_0:def_4; then consider u1, u2 being Vertex of T, m being odd Element of NAT such that A53: m + 2 <= len (P1 .cut (di,(P1 .find (P2 . ei)))) and A54: u1 = (P1 .cut (di,(P1 .find (P2 . ei)))) . m and x = (P1 .cut (di,(P1 .find (P2 . ei)))) . (m + 1) and A55: u2 = (P1 .cut (di,(P1 .find (P2 . ei)))) . (m + 2) and A56: x Joins u1,u2,T by A51, GLIB_001:103; x in (P2 .cut (di,ei)) .edges() by A52, XBOOLE_0:def_4; then consider v1, v2 being Vertex of T, n being odd Element of NAT such that A57: n + 2 <= len (P2 .cut (di,ei)) and A58: v1 = (P2 .cut (di,ei)) . n and x = (P2 .cut (di,ei)) . (n + 1) and A59: v2 = (P2 .cut (di,ei)) . (n + 2) and A60: x Joins v1,v2,T by GLIB_001:103; A61: n + 0 < n + 2 by XREAL_1:8; percases ( v1 <> v2 or v1 = v2 ) ; supposeA62: v1 <> v2 ; ::_thesis: contradiction A63: n + 2 = (n + 1) + 1 ; then A64: n + 1 < len (P2 .cut (di,ei)) by A57, NAT_1:13; then A65: (P2 .cut (di,ei)) . (n + 2) = P2 . (di + (n + 1)) by A11, A63, GLIB_001:36; consider ni being Nat such that A66: n = ni + 1 by NAT_1:6; reconsider ni = ni as Element of NAT by ORDINAL1:def_12; A67: u2 in (P1 .cut (di,(P1 .find (P2 . ei)))) .vertices() by A53, A55, GLIB_001:87; m + 0 < m + 2 by XREAL_1:8; then A68: m <= len (P1 .cut (di,(P1 .find (P2 . ei)))) by A53, XXREAL_0:2; then u1 in (P1 .cut (di,(P1 .find (P2 . ei)))) .vertices() by A54, GLIB_001:87; then A69: {u1,u2} c= ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) .vertices() by A50, A67, ZFMISC_1:32; A70: m + 2 = (m + 1) + 1 ; then A71: m + 1 < len (P1 .cut (di,(P1 .find (P2 . ei)))) by A53, NAT_1:13; then A72: (P1 .cut (di,(P1 .find (P2 . ei)))) . (m + 2) = P1 . (di + (m + 1)) by A13, A19, A70, GLIB_001:36; n <= len (P2 .cut (di,ei)) by A57, A61, XXREAL_0:2; then A73: v1 in (P2 .cut (di,ei)) .vertices() by A58, GLIB_001:87; v2 in (P2 .cut (di,ei)) .vertices() by A57, A59, GLIB_001:87; then A74: {v1,v2} c= (P2 .cut (di,ei)) .vertices() by A73, ZFMISC_1:32; A75: ( ( v1 = u1 & v2 = u2 ) or ( v1 = u2 & v2 = u1 ) ) by A60, A56, GLIB_000:15; then A76: ( v1 = P2 . ei or v1 = P1 . di ) by A41, A74, A69, XBOOLE_1:19, ZFMISC_1:22; n + 0 < n + 2 by XREAL_1:8; then n <= len (P2 .cut (di,ei)) by A57, XXREAL_0:2; then A77: ni < len (P2 .cut (di,ei)) by A66, NAT_1:13; then A78: (P2 .cut (di,ei)) . n = P2 . (di + ni) by A11, A66, GLIB_001:36; A79: P2 . (di + 2) = P2 . ei proof percases ( ( v1 = P2 . ei & v2 = P1 . di ) or ( v1 = P1 . di & v2 = P2 . ei ) ) by A41, A62, A75, A74, A69, A76, XBOOLE_1:19, ZFMISC_1:22; supposeA80: ( v1 = P2 . ei & v2 = P1 . di ) ; ::_thesis: P2 . (di + 2) = P2 . ei di + (n + 2) <= (len (P2 .cut (di,ei))) + di by A57, XREAL_1:6; then ((di + n) + 1) + 1 <= ei + 1 by A11, GLIB_001:36; then (di + n) + 1 <= ei by XREAL_1:6; then A81: di + (n + 1) <= len P2 by A11, XXREAL_0:2; di <= di + n by NAT_1:11; then di < (di + n) + 1 by NAT_1:13; then ( P2 .first() = P1 . di & P2 .last() = P1 . di ) by A15, A59, A65, A80, A81, GLIB_001:def_28; hence P2 . (di + 2) = P2 . ei by A43, GLIB_001:def_24; ::_thesis: verum end; supposeA82: ( v1 = P1 . di & v2 = P2 . ei ) ; ::_thesis: P2 . (di + 2) = P2 . ei ni = 0 proof di + ni < (len (P2 .cut (di,ei))) + di by A77, XREAL_1:6; then di + ni < ei + 1 by A11, GLIB_001:36; then di + ni <= ei by NAT_1:13; then A83: di + ni <= len P2 by A11, XXREAL_0:2; assume A84: ni <> 0 ; ::_thesis: contradiction reconsider ni = ni as even Element of NAT by A66; di + 0 < di + ni by A84, XREAL_1:6; then ( P2 .first() = P1 . di & P2 .last() = P1 . di ) by A15, A58, A78, A82, A83, GLIB_001:def_28; hence contradiction by A43, GLIB_001:def_24; ::_thesis: verum end; hence P2 . (di + 2) = P2 . ei by A11, A59, A66, A64, A82, GLIB_001:36; ::_thesis: verum end; end; end; consider im being Nat such that A85: m = im + 1 by NAT_1:6; A86: ( v2 = P2 . ei or v2 = P1 . di ) by A41, A75, A74, A69, XBOOLE_1:19, ZFMISC_1:22; reconsider im = im as Element of NAT by ORDINAL1:def_12; A87: im < len (P1 .cut (di,(P1 .find (P2 . ei)))) by A68, A85, NAT_1:13; then A88: (P1 .cut (di,(P1 .find (P2 . ei)))) . m = P1 . (di + im) by A13, A19, A85, GLIB_001:36; P1 . (di + 2) = P2 . ei proof percases ( ( u1 = P2 . ei & u2 = P1 . di ) or ( u1 = P1 . di & u2 = P2 . ei ) ) by A60, A56, A62, A76, A86, GLIB_000:15; supposeA89: ( u1 = P2 . ei & u2 = P1 . di ) ; ::_thesis: P1 . (di + 2) = P2 . ei di + (m + 2) <= (len (P1 .cut (di,(P1 .find (P2 . ei))))) + di by A53, XREAL_1:6; then ((di + m) + 1) + 1 <= (P1 .find (P2 . ei)) + 1 by A13, A19, GLIB_001:36; then (di + m) + 1 <= P1 .find (P2 . ei) by XREAL_1:6; then A90: di + (m + 1) <= len P1 by A13, XXREAL_0:2; di <= di + m by NAT_1:11; then di < (di + m) + 1 by NAT_1:13; then ( P1 .first() = P1 . di & P1 .last() = P1 . di ) by A55, A72, A89, A90, GLIB_001:def_28; hence P1 . (di + 2) = P2 . ei by A21, GLIB_001:def_24; ::_thesis: verum end; supposeA91: ( u1 = P1 . di & u2 = P2 . ei ) ; ::_thesis: P1 . (di + 2) = P2 . ei im = 0 proof di + im < (len (P1 .cut (di,(P1 .find (P2 . ei))))) + di by A87, XREAL_1:6; then di + im < (P1 .find (P2 . ei)) + 1 by A13, A19, GLIB_001:36; then di + im <= P1 .find (P2 . ei) by NAT_1:13; then A92: di + im <= len P1 by A13, XXREAL_0:2; assume A93: im <> 0 ; ::_thesis: contradiction reconsider im = im as even Element of NAT by A85; di + 0 < di + im by A93, XREAL_1:6; then ( P1 .first() = P1 . di & P1 .last() = P1 . di ) by A54, A88, A91, A92, GLIB_001:def_28; hence contradiction by A21, GLIB_001:def_24; ::_thesis: verum end; hence P1 . (di + 2) = P2 . ei by A13, A19, A55, A85, A71, A91, GLIB_001:36; ::_thesis: verum end; end; end; hence contradiction by A3, A44, A5, A79, Th24; ::_thesis: verum end; suppose v1 = v2 ; ::_thesis: contradiction then ( (P2 .cut (di,ei)) .first() = v1 & (P2 .cut (di,ei)) .last() = v1 ) by A57, A58, A59, A61, GLIB_001:def_28; hence contradiction by A42, GLIB_001:def_24; ::_thesis: verum end; end; end; not (P1 .cut (di,(P1 .find (P2 . ei)))) .reverse() is trivial by A20, GLIB_001:129; then (P2 .cut (di,ei)) .append ((P1 .cut (di,(P1 .find (P2 . ei)))) .reverse()) is Cycle-like by A42, A16, A37, A39, A38, A41, A49, Th20; hence contradiction ; ::_thesis: verum end; definition let T be _Tree; let a, b be Vertex of T; funcT .pathBetween (a,b) -> Path of T means :Def2: :: HELLY:def 2 it is_Walk_from a,b; existence ex b1 being Path of T st b1 is_Walk_from a,b proof consider W being Walk of T such that A1: W is_Walk_from a,b by GLIB_002:def_1; set P = the Path-like Subwalk of W; take the Path-like Subwalk of W ; ::_thesis: the Path-like Subwalk of W is_Walk_from a,b the Path-like Subwalk of W is_Walk_from W .first() ,W .last() by GLIB_001:def_32; then the Path-like Subwalk of W is_Walk_from a,W .last() by A1, GLIB_001:def_23; hence the Path-like Subwalk of W is_Walk_from a,b by A1, GLIB_001:def_23; ::_thesis: verum end; uniqueness for b1, b2 being Path of T st b1 is_Walk_from a,b & b2 is_Walk_from a,b holds b1 = b2 by Th27; end; :: deftheorem Def2 defines .pathBetween HELLY:def_2_:_ for T being _Tree for a, b being Vertex of T for b4 being Path of T holds ( b4 = T .pathBetween (a,b) iff b4 is_Walk_from a,b ); theorem Th28: :: HELLY:28 for T being _Tree for a, b being Vertex of T holds ( (T .pathBetween (a,b)) .first() = a & (T .pathBetween (a,b)) .last() = b ) proof let T be _Tree; ::_thesis: for a, b being Vertex of T holds ( (T .pathBetween (a,b)) .first() = a & (T .pathBetween (a,b)) .last() = b ) let a, b be Vertex of T; ::_thesis: ( (T .pathBetween (a,b)) .first() = a & (T .pathBetween (a,b)) .last() = b ) A1: T .pathBetween (a,b) is_Walk_from a,b by Def2; hence (T .pathBetween (a,b)) .first() = a by GLIB_001:def_23; ::_thesis: (T .pathBetween (a,b)) .last() = b thus (T .pathBetween (a,b)) .last() = b by A1, GLIB_001:def_23; ::_thesis: verum end; theorem Th29: :: HELLY:29 for T being _Tree for a, b being Vertex of T holds ( a in (T .pathBetween (a,b)) .vertices() & b in (T .pathBetween (a,b)) .vertices() ) proof let T be _Tree; ::_thesis: for a, b being Vertex of T holds ( a in (T .pathBetween (a,b)) .vertices() & b in (T .pathBetween (a,b)) .vertices() ) let a, b be Vertex of T; ::_thesis: ( a in (T .pathBetween (a,b)) .vertices() & b in (T .pathBetween (a,b)) .vertices() ) (T .pathBetween (a,b)) .first() = a by Th28; hence a in (T .pathBetween (a,b)) .vertices() by GLIB_001:88; ::_thesis: b in (T .pathBetween (a,b)) .vertices() (T .pathBetween (a,b)) .last() = b by Th28; hence b in (T .pathBetween (a,b)) .vertices() by GLIB_001:88; ::_thesis: verum end; registration let T be _Tree; let a be Vertex of T; clusterT .pathBetween (a,a) -> closed ; correctness coherence T .pathBetween (a,a) is closed ; proof T .pathBetween (a,a) is_Walk_from a,a by Def2; hence T .pathBetween (a,a) is closed by GLIB_001:119; ::_thesis: verum end; end; registration let T be _Tree; let a be Vertex of T; clusterT .pathBetween (a,a) -> trivial ; correctness coherence T .pathBetween (a,a) is trivial ; ; end; theorem Th30: :: HELLY:30 for T being _Tree for a being Vertex of T holds (T .pathBetween (a,a)) .vertices() = {a} proof let T be _Tree; ::_thesis: for a being Vertex of T holds (T .pathBetween (a,a)) .vertices() = {a} let a be Vertex of T; ::_thesis: (T .pathBetween (a,a)) .vertices() = {a} set P = T .pathBetween (a,a); consider v being Vertex of T such that A1: T .pathBetween (a,a) = T .walkOf v by GLIB_001:128; ( a = (T .pathBetween (a,a)) .first() & (T .walkOf v) .first() = v ) by Th28, GLIB_001:13; hence (T .pathBetween (a,a)) .vertices() = {a} by A1, GLIB_001:90; ::_thesis: verum end; theorem Th31: :: HELLY:31 for T being _Tree for a, b being Vertex of T holds (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a) proof let T be _Tree; ::_thesis: for a, b being Vertex of T holds (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a) let a, b be Vertex of T; ::_thesis: (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a) set P = T .pathBetween (a,b); T .pathBetween (a,b) is_Walk_from a,b by Def2; then (T .pathBetween (a,b)) .reverse() is_Walk_from b,a by GLIB_001:23; hence (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a) by Def2; ::_thesis: verum end; theorem Th32: :: HELLY:32 for T being _Tree for a, b being Vertex of T holds (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices() proof let T be _Tree; ::_thesis: for a, b being Vertex of T holds (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices() let a, b be Vertex of T; ::_thesis: (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices() (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a) by Th31; hence (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices() by GLIB_001:92; ::_thesis: verum end; theorem Th33: :: HELLY:33 for T being _Tree for a, b being Vertex of T for t being _Subtree of T for a9, b9 being Vertex of t st a = a9 & b = b9 holds T .pathBetween (a,b) = t .pathBetween (a9,b9) proof let T be _Tree; ::_thesis: for a, b being Vertex of T for t being _Subtree of T for a9, b9 being Vertex of t st a = a9 & b = b9 holds T .pathBetween (a,b) = t .pathBetween (a9,b9) let a, b be Vertex of T; ::_thesis: for t being _Subtree of T for a9, b9 being Vertex of t st a = a9 & b = b9 holds T .pathBetween (a,b) = t .pathBetween (a9,b9) let t be _Subtree of T; ::_thesis: for a9, b9 being Vertex of t st a = a9 & b = b9 holds T .pathBetween (a,b) = t .pathBetween (a9,b9) let a9, b9 be Vertex of t; ::_thesis: ( a = a9 & b = b9 implies T .pathBetween (a,b) = t .pathBetween (a9,b9) ) assume that A1: a = a9 and A2: b = b9 ; ::_thesis: T .pathBetween (a,b) = t .pathBetween (a9,b9) set tp = t .pathBetween (a9,b9); reconsider tp9 = t .pathBetween (a9,b9) as Walk of T by GLIB_001:167; A3: t .pathBetween (a9,b9) is_Walk_from a9,b9 by Def2; A4: tp9 .last() = (t .pathBetween (a9,b9)) .last() .= b by A2, A3, GLIB_001:def_23 ; tp9 .first() = (t .pathBetween (a9,b9)) .first() .= a by A1, A3, GLIB_001:def_23 ; then ( tp9 is Path-like & tp9 is_Walk_from a,b ) by A4, GLIB_001:176, GLIB_001:def_23; hence T .pathBetween (a,b) = t .pathBetween (a9,b9) by Def2; ::_thesis: verum end; theorem Th34: :: HELLY:34 for T being _Tree for a, b being Vertex of T for t being _Subtree of T st a in the_Vertices_of t & b in the_Vertices_of t holds (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t proof let T be _Tree; ::_thesis: for a, b being Vertex of T for t being _Subtree of T st a in the_Vertices_of t & b in the_Vertices_of t holds (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t let a, b be Vertex of T; ::_thesis: for t being _Subtree of T st a in the_Vertices_of t & b in the_Vertices_of t holds (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t let t be _Subtree of T; ::_thesis: ( a in the_Vertices_of t & b in the_Vertices_of t implies (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t ) assume ( a in the_Vertices_of t & b in the_Vertices_of t ) ; ::_thesis: (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t then reconsider a9 = a, b9 = b as Vertex of t ; set Tp = T .pathBetween (a,b); set tp = t .pathBetween (a9,b9); (T .pathBetween (a,b)) .vertices() = (t .pathBetween (a9,b9)) .vertices() by Th33, GLIB_001:76; hence (T .pathBetween (a,b)) .vertices() c= the_Vertices_of t ; ::_thesis: verum end; theorem Th35: :: HELLY:35 for T being _Tree for P being Path of T for a, b being Vertex of T for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds T .pathBetween (a,b) = P .cut (i,j) proof let T be _Tree; ::_thesis: for P being Path of T for a, b being Vertex of T for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds T .pathBetween (a,b) = P .cut (i,j) let P be Path of T; ::_thesis: for a, b being Vertex of T for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds T .pathBetween (a,b) = P .cut (i,j) let a, b be Vertex of T; ::_thesis: for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds T .pathBetween (a,b) = P .cut (i,j) let i, j be odd Nat; ::_thesis: ( i <= j & j <= len P & P . i = a & P . j = b implies T .pathBetween (a,b) = P .cut (i,j) ) assume A1: ( i <= j & j <= len P & P . i = a & P . j = b ) ; ::_thesis: T .pathBetween (a,b) = P .cut (i,j) reconsider i9 = i, j9 = j as odd Element of NAT by ORDINAL1:def_12; P .cut (i9,j9) is_Walk_from a,b by A1, GLIB_001:37; hence T .pathBetween (a,b) = P .cut (i,j) by Def2; ::_thesis: verum end; theorem Th36: :: HELLY:36 for T being _Tree for a, b, c being Vertex of T holds ( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) ) proof let T be _Tree; ::_thesis: for a, b, c being Vertex of T holds ( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) ) let a, b, c be Vertex of T; ::_thesis: ( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) ) set P = T .pathBetween (a,b); set ci = (T .pathBetween (a,b)) .find c; set pac = T .pathBetween (a,c); set pcb = T .pathBetween (c,b); hereby ::_thesis: ( T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) implies c in (T .pathBetween (a,b)) .vertices() ) A1: T .pathBetween (a,b) = (T .pathBetween (a,b)) .cut (1,(len (T .pathBetween (a,b)))) by GLIB_001:39; A2: ( 1 <= (T .pathBetween (a,b)) .find c & 1 = (2 * 0) + 1 ) by ABIAN:12; assume A3: c in (T .pathBetween (a,b)) .vertices() ; ::_thesis: T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) then A4: (T .pathBetween (a,b)) .find c <= len (T .pathBetween (a,b)) by GLIB_001:def_19; A5: (T .pathBetween (a,b)) . ((T .pathBetween (a,b)) .find c) = c by A3, GLIB_001:def_19; (T .pathBetween (a,b)) . (len (T .pathBetween (a,b))) = (T .pathBetween (a,b)) .last() .= b by Th28 ; then A6: T .pathBetween (c,b) = (T .pathBetween (a,b)) .cut (((T .pathBetween (a,b)) .find c),(len (T .pathBetween (a,b)))) by A4, A5, Th35; (T .pathBetween (a,b)) . 1 = (T .pathBetween (a,b)) .first() .= a by Th28 ; then T .pathBetween (a,c) = (T .pathBetween (a,b)) .cut (1,((T .pathBetween (a,b)) .find c)) by A4, A2, A5, Th35; hence T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) by A4, A2, A6, A1, GLIB_001:38; ::_thesis: verum end; assume T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) ; ::_thesis: c in (T .pathBetween (a,b)) .vertices() then A7: (T .pathBetween (a,c)) .vertices() c= (T .pathBetween (a,b)) .vertices() by Th13, Th15; c in (T .pathBetween (a,c)) .vertices() by Th29; hence c in (T .pathBetween (a,b)) .vertices() by A7; ::_thesis: verum end; theorem Th37: :: HELLY:37 for T being _Tree for a, b, c being Vertex of T holds ( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,c) is_a_prefix_of T .pathBetween (a,b) ) proof let T be _Tree; ::_thesis: for a, b, c being Vertex of T holds ( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,c) is_a_prefix_of T .pathBetween (a,b) ) let a, b, c be Vertex of T; ::_thesis: ( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,c) is_a_prefix_of T .pathBetween (a,b) ) hereby ::_thesis: ( T .pathBetween (a,c) is_a_prefix_of T .pathBetween (a,b) implies c in (T .pathBetween (a,b)) .vertices() ) assume c in (T .pathBetween (a,b)) .vertices() ; ::_thesis: T .pathBetween (a,c) c= T .pathBetween (a,b) then T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) by Th36; hence T .pathBetween (a,c) c= T .pathBetween (a,b) by Th15; ::_thesis: verum end; assume T .pathBetween (a,c) c= T .pathBetween (a,b) ; ::_thesis: c in (T .pathBetween (a,b)) .vertices() then A1: (T .pathBetween (a,c)) .vertices() c= (T .pathBetween (a,b)) .vertices() by Th13; c in (T .pathBetween (a,c)) .vertices() by Th29; hence c in (T .pathBetween (a,b)) .vertices() by A1; ::_thesis: verum end; theorem Th38: :: HELLY:38 for T being _Tree for P1, P2 being Path of T st P1 .last() = P2 .first() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} holds P1 .append P2 is Path-like proof let T be _Tree; ::_thesis: for P1, P2 being Path of T st P1 .last() = P2 .first() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} holds P1 .append P2 is Path-like let P1, P2 be Path of T; ::_thesis: ( P1 .last() = P2 .first() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} implies P1 .append P2 is Path-like ) assume that A1: P1 .last() = P2 .first() and A2: (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} ; ::_thesis: P1 .append P2 is Path-like percases ( P1 is trivial or P2 is trivial or ( not P1 is trivial & not P2 is trivial ) ) ; suppose P1 is trivial ; ::_thesis: P1 .append P2 is Path-like hence P1 .append P2 is Path-like by A1, Th16; ::_thesis: verum end; suppose P2 is trivial ; ::_thesis: P1 .append P2 is Path-like hence P1 .append P2 is Path-like by GLIB_001:130; ::_thesis: verum end; suppose ( not P1 is trivial & not P2 is trivial ) ; ::_thesis: P1 .append P2 is Path-like hence P1 .append P2 is Path-like by A1, A2, Th19; ::_thesis: verum end; end; end; theorem Th39: :: HELLY:39 for T being _Tree for a, b, c being Vertex of T holds ( c in (T .pathBetween (a,b)) .vertices() iff ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} ) proof let T be _Tree; ::_thesis: for a, b, c being Vertex of T holds ( c in (T .pathBetween (a,b)) .vertices() iff ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} ) let a, b, c be Vertex of T; ::_thesis: ( c in (T .pathBetween (a,b)) .vertices() iff ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} ) set Pac = T .pathBetween (a,c); set Pcb = T .pathBetween (c,b); set Pab = T .pathBetween (a,b); A1: (T .pathBetween (a,c)) .last() = c by Th28 .= (T .pathBetween (c,b)) .first() by Th28 ; thus ( c in (T .pathBetween (a,b)) .vertices() implies ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} ) ::_thesis: ( ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} implies c in (T .pathBetween (a,b)) .vertices() ) proof assume A2: c in (T .pathBetween (a,b)) .vertices() ; ::_thesis: ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} thus ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) c= {c} :: according to XBOOLE_0:def_10 ::_thesis: {c} c= ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) or x in {c} ) assume A3: x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) ; ::_thesis: x in {c} then A4: x in (T .pathBetween (a,c)) .vertices() by XBOOLE_0:def_4; A5: x in (T .pathBetween (c,b)) .vertices() by A3, XBOOLE_0:def_4; A6: (T .pathBetween (c,b)) .first() = c by Th28; A7: T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) by A2, Th36; A8: ( (T .pathBetween (a,b)) .first() = a & (T .pathBetween (a,b)) .last() = b ) by Th28; A9: (T .pathBetween (a,c)) .last() = c by Th28; percases ( T .pathBetween (a,b) is trivial or not T .pathBetween (a,b) is trivial ) ; suppose T .pathBetween (a,b) is trivial ; ::_thesis: x in {c} then (T .pathBetween (a,b)) .first() = (T .pathBetween (a,b)) .last() by GLIB_001:127; then A10: (T .pathBetween (a,b)) .vertices() = {a} by A8, Th30; x in ((T .pathBetween (a,c)) .vertices()) \/ ((T .pathBetween (c,b)) .vertices()) by A4, XBOOLE_0:def_3; then x in (T .pathBetween (a,b)) .vertices() by A7, A9, A6, GLIB_001:93; hence x in {c} by A2, A10, TARSKI:def_1; ::_thesis: verum end; supposeA11: not T .pathBetween (a,b) is trivial ; ::_thesis: x in {c} consider n being odd Element of NAT such that A12: n <= len (T .pathBetween (c,b)) and A13: (T .pathBetween (c,b)) . n = x by A5, GLIB_001:87; 1 <= n by ABIAN:12; then 1 - 1 <= n - 1 by XREAL_1:9; then reconsider n1 = n - 1 as even Element of NAT by INT_1:3; consider m being odd Element of NAT such that A14: m <= len (T .pathBetween (a,c)) and A15: (T .pathBetween (a,c)) . m = x by A4, GLIB_001:87; A16: m <= (len (T .pathBetween (a,c))) + n1 by A14, NAT_1:12; 1 <= m by ABIAN:12; then m in dom (T .pathBetween (a,c)) by A14, FINSEQ_3:25; then A17: (T .pathBetween (a,b)) . m = x by A7, A15, GLIB_001:32; (len (T .pathBetween (a,c))) + (n1 + 1) <= (len (T .pathBetween (a,c))) + (len (T .pathBetween (c,b))) by A12, XREAL_1:6; then (((len (T .pathBetween (a,c))) + n1) + 1) - 1 <= ((len (T .pathBetween (a,c))) + (len (T .pathBetween (c,b)))) - 1 by XREAL_1:9; then A18: (((len (T .pathBetween (a,c))) + n1) + 1) - 1 <= ((len (T .pathBetween (a,b))) + 1) - 1 by A7, A9, A6, GLIB_001:28; A19: n1 + 1 = n ; then n1 < len (T .pathBetween (c,b)) by A12, NAT_1:13; then A20: (T .pathBetween (a,b)) . ((len (T .pathBetween (a,c))) + n1) = x by A7, A9, A6, A13, A19, GLIB_001:33; percases ( m < (len (T .pathBetween (a,c))) + n1 or m = (len (T .pathBetween (a,c))) + n1 ) by A16, XXREAL_0:1; supposeA21: m < (len (T .pathBetween (a,c))) + n1 ; ::_thesis: x in {c} then (T .pathBetween (a,b)) .first() = x by A17, A20, A18, GLIB_001:def_28 .= (T .pathBetween (a,b)) .last() by A17, A20, A18, A21, GLIB_001:def_28 ; hence x in {c} by A11, GLIB_001:def_24; ::_thesis: verum end; supposeA22: m = (len (T .pathBetween (a,c))) + n1 ; ::_thesis: x in {c} then n1 = 0 by A14, NAT_1:16; hence x in {c} by A9, A15, A22, TARSKI:def_1; ::_thesis: verum end; end; end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {c} or x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) ) assume x in {c} ; ::_thesis: x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) then A23: x = c by TARSKI:def_1; then x = (T .pathBetween (c,b)) .first() by Th28; then A24: x in (T .pathBetween (c,b)) .vertices() by GLIB_001:88; x = (T .pathBetween (a,c)) .last() by A23, Th28; then x in (T .pathBetween (a,c)) .vertices() by GLIB_001:88; hence x in ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) by A24, XBOOLE_0:def_4; ::_thesis: verum end; ( (T .pathBetween (a,c)) .first() = a & (T .pathBetween (c,b)) .last() = b ) by Th28; then A25: (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) is_Walk_from a,b by A1, GLIB_001:30; assume ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} ; ::_thesis: c in (T .pathBetween (a,b)) .vertices() then ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {((T .pathBetween (a,c)) .last())} by Th28; then (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) is Path-like by A1, Th38; then T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) by A25, Def2; hence c in (T .pathBetween (a,b)) .vertices() by Th36; ::_thesis: verum end; theorem Th40: :: HELLY:40 for T being _Tree for a, b, c, d being Vertex of T for P1, P2 being Path of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not P1 is_a_prefix_of P2 & not P2 is_a_prefix_of P1 & d = P1 . (len (maxPrefix (P1,P2))) holds ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) = {d} proof let T be _Tree; ::_thesis: for a, b, c, d being Vertex of T for P1, P2 being Path of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not P1 is_a_prefix_of P2 & not P2 is_a_prefix_of P1 & d = P1 . (len (maxPrefix (P1,P2))) holds ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) = {d} let a, b, c, d be Vertex of T; ::_thesis: for P1, P2 being Path of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not P1 is_a_prefix_of P2 & not P2 is_a_prefix_of P1 & d = P1 . (len (maxPrefix (P1,P2))) holds ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) = {d} let P1, P2 be Path of T; ::_thesis: ( P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not P1 is_a_prefix_of P2 & not P2 is_a_prefix_of P1 & d = P1 . (len (maxPrefix (P1,P2))) implies ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) = {d} ) assume that A1: P1 = T .pathBetween (a,b) and A2: P2 = T .pathBetween (a,c) and A3: not P1 c= P2 and A4: not P2 c= P1 and A5: d = P1 . (len (maxPrefix (P1,P2))) ; ::_thesis: ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) = {d} set Pad = T .pathBetween (a,d); set di = len (maxPrefix (P1,P2)); A6: P1 .first() = a by A1, Th28; A7: P2 .first() = a by A2, Th28; then reconsider di = len (maxPrefix (P1,P2)) as odd Element of NAT by A6, Th22; A8: di <= di + 2 by NAT_1:11; set Pdb = T .pathBetween (d,b); A9: (T .pathBetween (d,b)) .first() = d by Th28; set Pdc = T .pathBetween (d,c); A10: d = P2 . (len (maxPrefix (P1,P2))) by A5, Th7; A11: di <= di + 2 by NAT_1:11; di + 2 <= len P2 by A4, A6, A7, Th23; then di <= len P2 by A11, XXREAL_0:2; then d in P2 .vertices() by A10, GLIB_001:87; then A12: P2 = (T .pathBetween (a,d)) .append (T .pathBetween (d,c)) by A2, Th36; A13: (T .pathBetween (a,d)) .last() = d by Th28; A14: (T .pathBetween (d,c)) . 1 = (T .pathBetween (d,c)) .first() .= d by Th28 ; A15: (T .pathBetween (d,c)) .first() = d by Th28; di + 2 <= len P1 by A3, A6, A7, Th23; then A16: di <= len P1 by A8, XXREAL_0:2; then d in P1 .vertices() by A5, GLIB_001:87; then A17: P1 = (T .pathBetween (a,d)) .append (T .pathBetween (d,b)) by A1, Th36; A18: 1 <= di by ABIAN:12; then T .pathBetween (a,d) = P1 .cut (((2 * 0) + 1),di) by A5, A6, A16, Th35; then A19: (len (T .pathBetween (a,d))) + ((2 * 0) + 1) = di + 1 by A16, A18, GLIB_001:36; A20: (T .pathBetween (d,b)) . 1 = (T .pathBetween (d,b)) .first() .= d by Th28 ; thus ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) = {d} ::_thesis: verum proof hereby :: according to XBOOLE_0:def_10 ::_thesis: {d} c= ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) assume not ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) c= {d} ; ::_thesis: contradiction then consider e being set such that A21: e in ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) and A22: not e in {d} by TARSKI:def_3; A23: e in (T .pathBetween (d,b)) .vertices() by A21, XBOOLE_0:def_4; A24: e in (T .pathBetween (d,c)) .vertices() by A21, XBOOLE_0:def_4; reconsider e = e as Vertex of T by A21; consider ebi being odd Element of NAT such that A25: ebi <= len (T .pathBetween (d,b)) and A26: e = (T .pathBetween (d,b)) . ebi by A23, GLIB_001:87; set Pdeb = (T .pathBetween (d,b)) .cut (1,ebi); ( 1 <= ebi & (2 * 0) + 1 is odd Element of NAT ) by ABIAN:12; then A27: (T .pathBetween (d,b)) .cut (1,ebi) is_Walk_from d,e by A20, A25, A26, GLIB_001:37; 1 < len ((T .pathBetween (d,b)) .cut (1,ebi)) proof assume A28: 1 >= len ((T .pathBetween (d,b)) .cut (1,ebi)) ; ::_thesis: contradiction percases ( len ((T .pathBetween (d,b)) .cut (1,ebi)) = 2 * 0 or len ((T .pathBetween (d,b)) .cut (1,ebi)) = 1 ) by A28, NAT_1:25; suppose len ((T .pathBetween (d,b)) .cut (1,ebi)) = 2 * 0 ; ::_thesis: contradiction hence contradiction ; ::_thesis: verum end; supposeA29: len ((T .pathBetween (d,b)) .cut (1,ebi)) = 1 ; ::_thesis: contradiction A30: ((T .pathBetween (d,b)) .cut (1,ebi)) . 1 = d by A27, GLIB_001:17; ((T .pathBetween (d,b)) .cut (1,ebi)) . 1 = e by A27, A29, GLIB_001:17; hence contradiction by A22, A30, TARSKI:def_1; ::_thesis: verum end; end; end; then A31: ((2 * 0) + 1) + 2 <= len ((T .pathBetween (d,b)) .cut (1,ebi)) by CHORD:4; then A32: 2 < len ((T .pathBetween (d,b)) .cut (1,ebi)) by XXREAL_0:2; consider eci being odd Element of NAT such that A33: eci <= len (T .pathBetween (d,c)) and A34: e = (T .pathBetween (d,c)) . eci by A24, GLIB_001:87; set Pdec = (T .pathBetween (d,c)) .cut (1,eci); ( 1 <= eci & (2 * 0) + 1 is odd Element of NAT ) by ABIAN:12; then A35: (T .pathBetween (d,c)) .cut (1,eci) is_Walk_from d,e by A14, A33, A34, GLIB_001:37; 1 < len ((T .pathBetween (d,c)) .cut (1,eci)) proof assume A36: 1 >= len ((T .pathBetween (d,c)) .cut (1,eci)) ; ::_thesis: contradiction percases ( len ((T .pathBetween (d,c)) .cut (1,eci)) = 2 * 0 or len ((T .pathBetween (d,c)) .cut (1,eci)) = 1 ) by A36, NAT_1:25; suppose len ((T .pathBetween (d,c)) .cut (1,eci)) = 2 * 0 ; ::_thesis: contradiction hence contradiction ; ::_thesis: verum end; supposeA37: len ((T .pathBetween (d,c)) .cut (1,eci)) = 1 ; ::_thesis: contradiction A38: ((T .pathBetween (d,c)) .cut (1,eci)) . 1 = d by A35, GLIB_001:17; ((T .pathBetween (d,c)) .cut (1,eci)) . 1 = e by A35, A37, GLIB_001:17; hence contradiction by A22, A38, TARSKI:def_1; ::_thesis: verum end; end; end; then A39: ((2 * 0) + 1) + 2 <= len ((T .pathBetween (d,c)) .cut (1,eci)) by CHORD:4; then A40: 2 < len ((T .pathBetween (d,c)) .cut (1,eci)) by XXREAL_0:2; 1 + 2 in dom ((T .pathBetween (d,b)) .cut (1,ebi)) by A31, FINSEQ_3:25; then A41: ((T .pathBetween (d,b)) .cut (1,ebi)) . (1 + 2) = (T .pathBetween (d,b)) . (1 + 2) by A25, GLIB_001:46; len ((T .pathBetween (d,b)) .cut (1,ebi)) <= len (T .pathBetween (d,b)) by Th10; then 2 < len (T .pathBetween (d,b)) by A32, XXREAL_0:2; then A42: P1 . (di + 2) = (T .pathBetween (d,b)) . (1 + 2) by A9, A13, A17, A19, GLIB_001:33; len ((T .pathBetween (d,c)) .cut (1,eci)) <= len (T .pathBetween (d,c)) by Th10; then 2 < len (T .pathBetween (d,c)) by A40, XXREAL_0:2; then A43: P2 . (di + 2) = (T .pathBetween (d,c)) . (1 + 2) by A15, A13, A12, A19, GLIB_001:33; A44: 1 + 2 in dom ((T .pathBetween (d,c)) .cut (1,eci)) by A39, FINSEQ_3:25; ((T .pathBetween (d,b)) .cut (1,ebi)) . (1 + 2) = ((T .pathBetween (d,c)) .cut (1,eci)) . (1 + 2) by A27, A35, Th27; hence contradiction by A3, A4, A6, A7, A33, A42, A41, A43, A44, Th24, GLIB_001:46; ::_thesis: verum end; ( d in (T .pathBetween (d,b)) .vertices() & d in (T .pathBetween (d,c)) .vertices() ) by A9, A15, GLIB_001:88; then d in ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) by XBOOLE_0:def_4; hence {d} c= ((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) by ZFMISC_1:31; ::_thesis: verum end; end; Lm1: for T being _Tree for a, b, c being Vertex of T st c in (T .pathBetween (a,b)) .vertices() holds (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c} proof let T be _Tree; ::_thesis: for a, b, c being Vertex of T st c in (T .pathBetween (a,b)) .vertices() holds (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c} let a, b, c be Vertex of T; ::_thesis: ( c in (T .pathBetween (a,b)) .vertices() implies (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c} ) assume A1: c in (T .pathBetween (a,b)) .vertices() ; ::_thesis: (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c} set P1 = T .pathBetween (a,b); set P2 = T .pathBetween (b,c); set P3 = T .pathBetween (c,a); (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices() by Th32; then ((T .pathBetween (b,c)) .vertices()) /\ ((T .pathBetween (c,a)) .vertices()) = {c} by A1, Th39; then ((T .pathBetween (a,b)) .vertices()) /\ (((T .pathBetween (b,c)) .vertices()) /\ ((T .pathBetween (c,a)) .vertices())) = {c} by A1, ZFMISC_1:46; hence (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c} by XBOOLE_1:16; ::_thesis: verum end; Lm2: for T being _Tree for a, b, c being Vertex of T for P1, P4 being Path of T st P1 = T .pathBetween (a,b) & P4 = T .pathBetween (a,c) & not P1 c= P4 & not P4 c= P1 holds ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))} proof let T be _Tree; ::_thesis: for a, b, c being Vertex of T for P1, P4 being Path of T st P1 = T .pathBetween (a,b) & P4 = T .pathBetween (a,c) & not P1 c= P4 & not P4 c= P1 holds ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))} let a, b, c be Vertex of T; ::_thesis: for P1, P4 being Path of T st P1 = T .pathBetween (a,b) & P4 = T .pathBetween (a,c) & not P1 c= P4 & not P4 c= P1 holds ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))} let P1, P4 be Path of T; ::_thesis: ( P1 = T .pathBetween (a,b) & P4 = T .pathBetween (a,c) & not P1 c= P4 & not P4 c= P1 implies ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))} ) assume that A1: P1 = T .pathBetween (a,b) and A2: P4 = T .pathBetween (a,c) and A3: not P1 c= P4 and A4: not P4 c= P1 ; ::_thesis: ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))} set P3 = T .pathBetween (c,a); A5: (T .pathBetween (c,a)) .vertices() = P4 .vertices() by A2, Th32; set i = len (maxPrefix (P1,P4)); P1 .first() = a by A1, Th28; then A6: P1 .first() = P4 .first() by A2, Th28; then reconsider i9 = len (maxPrefix (P1,P4)) as odd Element of NAT by Th22; set x = P1 . i9; A7: len (maxPrefix (P1,P4)) <= (len (maxPrefix (P1,P4))) + 2 by NAT_1:11; A8: now__::_thesis:_not_b_in_(T_.pathBetween_(c,a))_.vertices() assume b in (T .pathBetween (c,a)) .vertices() ; ::_thesis: contradiction then b in P4 .vertices() by A2, Th32; then P4 = (T .pathBetween (a,b)) .append (T .pathBetween (b,c)) by A2, Th36; hence contradiction by A1, A3, Th15; ::_thesis: verum end; (len (maxPrefix (P1,P4))) + 2 <= len P4 by A4, A6, Th23; then A9: len (maxPrefix (P1,P4)) <= len P4 by A7, XXREAL_0:2; A10: (len (maxPrefix (P1,P4))) + 2 <= len P1 by A3, A6, Th23; then reconsider x = P1 . i9 as Vertex of T by A7, GLIB_001:7, XXREAL_0:2; set P1b = P1 .cut (i9,(len P1)); set P1br = (P1 .cut (i9,(len P1))) .reverse() ; set j = len ((P1 .cut (i9,(len P1))) .reverse()); set P4c = P4 .cut (i9,(len P4)); set Pbc = ((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4))); A11: len (maxPrefix (P1,P4)) <= len P1 by A7, A10, XXREAL_0:2; then (P1 .cut (i9,(len P1))) .first() = P1 . i9 by GLIB_001:37; then A12: ((P1 .cut (i9,(len P1))) .reverse()) .last() = x by GLIB_001:22; 1 <= len ((P1 .cut (i9,(len P1))) .reverse()) by CHORD:2; then len ((P1 .cut (i9,(len P1))) .reverse()) in dom ((P1 .cut (i9,(len P1))) .reverse()) by FINSEQ_3:25; then A13: (((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4)))) . (len ((P1 .cut (i9,(len P1))) .reverse())) = x by A12, GLIB_001:32; set P2 = T .pathBetween (b,c); A14: x in P1 .vertices() by A11, GLIB_001:87; A15: P1 . (len P1) = P1 .last() .= b by A1, Th28 ; then (P1 .cut (i9,(len P1))) .last() = b by A11, GLIB_001:37; then A16: ((P1 .cut (i9,(len P1))) .reverse()) .first() = b by GLIB_001:22; A17: x = P4 . i9 by Th7; then x <> b by A8, A5, A9, GLIB_001:87; then A18: (P1 .cut (i9,(len P1))) .reverse() is open by A12, A16, GLIB_001:def_24; P4 . (len P4) = P4 .last() .= c by A2, Th28 ; then P4 .cut (i9,(len P4)) is_Walk_from x,c by A9, A17, GLIB_001:37; then A19: P4 .cut (i9,(len P4)) = T .pathBetween (x,c) by Def2; then A20: (P4 .cut (i9,(len P4))) .first() = x by Th28; then A21: len ((P1 .cut (i9,(len P1))) .reverse()) <= len (((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4)))) by A12, GLIB_001:29; P1 .cut (i9,(len P1)) is_Walk_from x,b by A11, A15, GLIB_001:37; then P1 .cut (i9,(len P1)) = T .pathBetween (x,b) by Def2; then ( ((P1 .cut (i9,(len P1))) .reverse()) .vertices() = (P1 .cut (i9,(len P1))) .vertices() & ((P1 .cut (i9,(len P1))) .vertices()) /\ ((P4 .cut (i9,(len P4))) .vertices()) = {x} ) by A1, A2, A3, A4, A19, Th40, GLIB_001:92; then A22: (((P1 .cut (i9,(len P1))) .reverse()) .vertices()) /\ ((P4 .cut (i9,(len P4))) .vertices()) c= {(((P1 .cut (i9,(len P1))) .reverse()) .first()),(((P1 .cut (i9,(len P1))) .reverse()) .last())} by A12, ZFMISC_1:7; A23: (P4 .cut (i9,(len P4))) .vertices() c= P4 .vertices() by A9, GLIB_001:94; A24: ((P1 .cut (i9,(len P1))) .reverse()) .edges() misses (P4 .cut (i9,(len P4))) .edges() proof assume not ((P1 .cut (i9,(len P1))) .reverse()) .edges() misses (P4 .cut (i9,(len P4))) .edges() ; ::_thesis: contradiction then (((P1 .cut (i9,(len P1))) .reverse()) .edges()) /\ ((P4 .cut (i9,(len P4))) .edges()) <> {} by XBOOLE_0:def_7; then consider e being set such that A25: e in (((P1 .cut (i9,(len P1))) .reverse()) .edges()) /\ ((P4 .cut (i9,(len P4))) .edges()) by XBOOLE_0:def_1; e in ((P1 .cut (i9,(len P1))) .reverse()) .edges() by A25, XBOOLE_0:def_4; then consider v1br, v2br being Vertex of T, n being odd Element of NAT such that A26: n + 2 <= len ((P1 .cut (i9,(len P1))) .reverse()) and A27: v1br = ((P1 .cut (i9,(len P1))) .reverse()) . n and e = ((P1 .cut (i9,(len P1))) .reverse()) . (n + 1) and A28: v2br = ((P1 .cut (i9,(len P1))) .reverse()) . (n + 2) and A29: e Joins v1br,v2br,T by GLIB_001:103; n <= n + 2 by NAT_1:11; then n <= len ((P1 .cut (i9,(len P1))) .reverse()) by A26, XXREAL_0:2; then A30: v1br in ((P1 .cut (i9,(len P1))) .reverse()) .vertices() by A27, GLIB_001:87; v2br in ((P1 .cut (i9,(len P1))) .reverse()) .vertices() by A26, A28, GLIB_001:87; then A31: {v1br,v2br} c= ((P1 .cut (i9,(len P1))) .reverse()) .vertices() by A30, ZFMISC_1:32; e in (P4 .cut (i9,(len P4))) .edges() by A25, XBOOLE_0:def_4; then consider v1c, v2c being Vertex of T, m being odd Element of NAT such that A32: m + 2 <= len (P4 .cut (i9,(len P4))) and A33: v1c = (P4 .cut (i9,(len P4))) . m and e = (P4 .cut (i9,(len P4))) . (m + 1) and A34: v2c = (P4 .cut (i9,(len P4))) . (m + 2) and A35: e Joins v1c,v2c,T by GLIB_001:103; m <= m + 2 by NAT_1:11; then m <= len (P4 .cut (i9,(len P4))) by A32, XXREAL_0:2; then A36: v1c in (P4 .cut (i9,(len P4))) .vertices() by A33, GLIB_001:87; A37: ( ( v1br = v1c & v2br = v2c ) or ( v1br = v2c & v2br = v1c ) ) by A29, A35, GLIB_000:15; A38: v2c in (P4 .cut (i9,(len P4))) .vertices() by A32, A34, GLIB_001:87; then {v1c,v2c} c= (P4 .cut (i9,(len P4))) .vertices() by A36, ZFMISC_1:32; then A39: {v1c,v2c} c= (((P1 .cut (i9,(len P1))) .reverse()) .vertices()) /\ ((P4 .cut (i9,(len P4))) .vertices()) by A37, A31, XBOOLE_1:19; then A40: ( v2c = b or v2c = x ) by A12, A16, A22, XBOOLE_1:1, ZFMISC_1:22; ( v1c = b or v1c = x ) by A12, A16, A22, A39, XBOOLE_1:1, ZFMISC_1:22; hence contradiction by A8, A5, A23, A35, A36, A38, A40, GLIB_000:18; ::_thesis: verum end; A41: (P4 .cut (i9,(len P4))) .last() = c by A19, Th28; then A42: ((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4))) is_Walk_from b,c by A12, A20, A16, GLIB_001:30; now__::_thesis:_not_c_in_P1_.vertices() assume c in P1 .vertices() ; ::_thesis: contradiction then P1 = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) by A1, Th36; hence contradiction by A2, A4, Th15; ::_thesis: verum end; then x <> c by A11, GLIB_001:87; then A43: P4 .cut (i9,(len P4)) is open by A20, A41, GLIB_001:def_24; not ((P1 .cut (i9,(len P1))) .reverse()) .first() in (P4 .cut (i9,(len P4))) .vertices() by A8, A5, A23, A16; then ((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4))) is Path of T by A12, A20, A18, A43, A22, A24, Th18; then ((P1 .cut (i9,(len P1))) .reverse()) .append (P4 .cut (i9,(len P4))) = T .pathBetween (b,c) by A42, Def2; then A44: x in (T .pathBetween (b,c)) .vertices() by A21, A13, GLIB_001:87; A45: x in P4 .vertices() by A9, A17, GLIB_001:87; A46: ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) c= {x} proof set Pcx = T .pathBetween (c,x); set Pxa = T .pathBetween (x,a); set Pbx = T .pathBetween (b,x); set Pxc = T .pathBetween (x,c); set Pax = T .pathBetween (a,x); set Pxb = T .pathBetween (x,b); let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) or z in {x} ) A47: (T .pathBetween (b,x)) .vertices() = (T .pathBetween (x,b)) .vertices() by Th32; A48: (T .pathBetween (c,x)) .vertices() = (T .pathBetween (x,c)) .vertices() by Th32; A49: (T .pathBetween (c,x)) .last() = x by Th28 .= (T .pathBetween (x,a)) .first() by Th28 ; T .pathBetween (c,a) = (T .pathBetween (c,x)) .append (T .pathBetween (x,a)) by A5, A45, Th36; then A50: (T .pathBetween (c,a)) .vertices() = ((T .pathBetween (c,x)) .vertices()) \/ ((T .pathBetween (x,a)) .vertices()) by A49, GLIB_001:93; A51: (T .pathBetween (b,x)) .last() = x by Th28 .= (T .pathBetween (x,c)) .first() by Th28 ; T .pathBetween (b,c) = (T .pathBetween (b,x)) .append (T .pathBetween (x,c)) by A44, Th36; then A52: (T .pathBetween (b,c)) .vertices() = ((T .pathBetween (b,x)) .vertices()) \/ ((T .pathBetween (x,c)) .vertices()) by A51, GLIB_001:93; A53: (T .pathBetween (a,x)) .last() = x by Th28 .= (T .pathBetween (x,b)) .first() by Th28 ; P1 = (T .pathBetween (a,x)) .append (T .pathBetween (x,b)) by A1, A14, Th36; then A54: P1 .vertices() = ((T .pathBetween (a,x)) .vertices()) \/ ((T .pathBetween (x,b)) .vertices()) by A53, GLIB_001:93; assume A55: z in ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) ; ::_thesis: z in {x} then A56: z in (P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices()) by XBOOLE_0:def_4; then z in P1 .vertices() by XBOOLE_0:def_4; then A57: ( z in (T .pathBetween (a,x)) .vertices() or z in (T .pathBetween (x,b)) .vertices() ) by A54, XBOOLE_0:def_3; z in (T .pathBetween (c,a)) .vertices() by A55, XBOOLE_0:def_4; then A58: ( z in (T .pathBetween (c,x)) .vertices() or z in (T .pathBetween (x,a)) .vertices() ) by A50, XBOOLE_0:def_3; z in (T .pathBetween (b,c)) .vertices() by A56, XBOOLE_0:def_4; then A59: ( z in (T .pathBetween (b,x)) .vertices() or z in (T .pathBetween (x,c)) .vertices() ) by A52, XBOOLE_0:def_3; percases ( ( z in (T .pathBetween (a,x)) .vertices() & z in (T .pathBetween (b,x)) .vertices() ) or ( z in (T .pathBetween (a,x)) .vertices() & z in (T .pathBetween (c,x)) .vertices() ) or ( z in (T .pathBetween (b,x)) .vertices() & z in (T .pathBetween (c,x)) .vertices() ) ) by A57, A59, A58, Th32; suppose ( z in (T .pathBetween (a,x)) .vertices() & z in (T .pathBetween (b,x)) .vertices() ) ; ::_thesis: z in {x} then z in ((T .pathBetween (a,x)) .vertices()) /\ ((T .pathBetween (x,b)) .vertices()) by A47, XBOOLE_0:def_4; hence z in {x} by A1, A14, Th39; ::_thesis: verum end; suppose ( z in (T .pathBetween (a,x)) .vertices() & z in (T .pathBetween (c,x)) .vertices() ) ; ::_thesis: z in {x} then z in ((T .pathBetween (a,x)) .vertices()) /\ ((T .pathBetween (x,c)) .vertices()) by A48, XBOOLE_0:def_4; hence z in {x} by A2, A45, Th39; ::_thesis: verum end; suppose ( z in (T .pathBetween (b,x)) .vertices() & z in (T .pathBetween (c,x)) .vertices() ) ; ::_thesis: z in {x} then z in ((T .pathBetween (b,x)) .vertices()) /\ ((T .pathBetween (x,c)) .vertices()) by A48, XBOOLE_0:def_4; hence z in {x} by A44, Th39; ::_thesis: verum end; end; end; x in (P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices()) by A14, A44, XBOOLE_0:def_4; then x in ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) by A5, A45, XBOOLE_0:def_4; then {x} c= ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) by ZFMISC_1:31; hence ((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))} by A46, XBOOLE_0:def_10; ::_thesis: verum end; definition let T be _Tree; let a, b, c be Vertex of T; func MiddleVertex (a,b,c) -> Vertex of T means :Def3: :: HELLY:def 3 (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {it}; existence ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} proof defpred S1[ Vertex of T, Vertex of T, Vertex of T, Vertex of T] means (((T .pathBetween ($1,$2)) .vertices()) /\ ((T .pathBetween ($2,$3)) .vertices())) /\ ((T .pathBetween ($3,$1)) .vertices()) = {$4}; set P3 = T .pathBetween (c,a); set P2 = T .pathBetween (b,c); set P1 = T .pathBetween (a,b); percases ( c in (T .pathBetween (a,b)) .vertices() or a in (T .pathBetween (b,c)) .vertices() or b in (T .pathBetween (c,a)) .vertices() or ( not c in (T .pathBetween (a,b)) .vertices() & not a in (T .pathBetween (b,c)) .vertices() & not b in (T .pathBetween (c,a)) .vertices() ) ) ; supposeA1: ( c in (T .pathBetween (a,b)) .vertices() or a in (T .pathBetween (b,c)) .vertices() or b in (T .pathBetween (c,a)) .vertices() ) ; ::_thesis: ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} percases ( c in (T .pathBetween (a,b)) .vertices() or a in (T .pathBetween (b,c)) .vertices() or b in (T .pathBetween (c,a)) .vertices() ) by A1; suppose c in (T .pathBetween (a,b)) .vertices() ; ::_thesis: ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} then S1[a,b,c,c] by Lm1; hence ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} ; ::_thesis: verum end; suppose a in (T .pathBetween (b,c)) .vertices() ; ::_thesis: ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} then S1[b,c,a,a] by Lm1; hence ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} by XBOOLE_1:16; ::_thesis: verum end; suppose b in (T .pathBetween (c,a)) .vertices() ; ::_thesis: ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} then S1[c,a,b,b] by Lm1; hence ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} by XBOOLE_1:16; ::_thesis: verum end; end; end; supposeA2: ( not c in (T .pathBetween (a,b)) .vertices() & not a in (T .pathBetween (b,c)) .vertices() & not b in (T .pathBetween (c,a)) .vertices() ) ; ::_thesis: ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} set P4 = T .pathBetween (a,c); set i = len (maxPrefix ((T .pathBetween (a,b)),(T .pathBetween (a,c)))); (T .pathBetween (a,b)) .last() = b by Th28; then A3: b in (T .pathBetween (a,b)) .vertices() by GLIB_001:88; (T .pathBetween (a,c)) .last() = c by Th28; then c in (T .pathBetween (a,c)) .vertices() by GLIB_001:88; then not (T .pathBetween (a,c)) .vertices() c= (T .pathBetween (a,b)) .vertices() by A2; then A4: not T .pathBetween (a,c) c= T .pathBetween (a,b) by Th13; (T .pathBetween (a,b)) .first() = a by Th28; then A5: (T .pathBetween (a,b)) .first() = (T .pathBetween (a,c)) .first() by Th28; then reconsider i9 = len (maxPrefix ((T .pathBetween (a,b)),(T .pathBetween (a,c)))) as odd Element of NAT by Th22; set x = (T .pathBetween (a,b)) . i9; (T .pathBetween (c,a)) .vertices() = (T .pathBetween (a,c)) .vertices() by Th32; then A6: not (T .pathBetween (a,b)) .vertices() c= (T .pathBetween (a,c)) .vertices() by A2, A3; then ( len (maxPrefix ((T .pathBetween (a,b)),(T .pathBetween (a,c)))) <= (len (maxPrefix ((T .pathBetween (a,b)),(T .pathBetween (a,c))))) + 2 & (len (maxPrefix ((T .pathBetween (a,b)),(T .pathBetween (a,c))))) + 2 <= len (T .pathBetween (a,b)) ) by A5, Th13, Th23, NAT_1:11; then reconsider x = (T .pathBetween (a,b)) . i9 as Vertex of T by GLIB_001:7, XXREAL_0:2; take x ; ::_thesis: (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {x} not T .pathBetween (a,b) c= T .pathBetween (a,c) by A6, Th13; hence (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {x} by A4, Lm2; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} & (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b2} holds b1 = b2 by ZFMISC_1:3; end; :: deftheorem Def3 defines MiddleVertex HELLY:def_3_:_ for T being _Tree for a, b, c, b5 being Vertex of T holds ( b5 = MiddleVertex (a,b,c) iff (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b5} ); theorem Th41: :: HELLY:41 for T being _Tree for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (a,c,b) proof let T be _Tree; ::_thesis: for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (a,c,b) let a, b, c be Vertex of T; ::_thesis: MiddleVertex (a,b,c) = MiddleVertex (a,c,b) set PMV1 = MiddleVertex (a,b,c); set PMV2 = MiddleVertex (a,c,b); A1: ( (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices() & (T .pathBetween (b,c)) .vertices() = (T .pathBetween (c,b)) .vertices() ) by Th32; A2: (T .pathBetween (c,a)) .vertices() = (T .pathBetween (a,c)) .vertices() by Th32; ( (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(MiddleVertex (a,b,c))} & (((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices())) /\ ((T .pathBetween (b,a)) .vertices()) = {(MiddleVertex (a,c,b))} ) by Def3; then {(MiddleVertex (a,b,c))} = {(MiddleVertex (a,c,b))} by A1, A2, XBOOLE_1:16; hence MiddleVertex (a,b,c) = MiddleVertex (a,c,b) by ZFMISC_1:3; ::_thesis: verum end; theorem Th42: :: HELLY:42 for T being _Tree for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (b,a,c) proof let T be _Tree; ::_thesis: for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (b,a,c) let a, b, c be Vertex of T; ::_thesis: MiddleVertex (a,b,c) = MiddleVertex (b,a,c) set PMV1 = MiddleVertex (a,b,c); set PMV2 = MiddleVertex (b,a,c); A1: ( (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices() & (T .pathBetween (b,c)) .vertices() = (T .pathBetween (c,b)) .vertices() ) by Th32; A2: (T .pathBetween (c,a)) .vertices() = (T .pathBetween (a,c)) .vertices() by Th32; ( (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(MiddleVertex (a,b,c))} & (((T .pathBetween (b,a)) .vertices()) /\ ((T .pathBetween (a,c)) .vertices())) /\ ((T .pathBetween (c,b)) .vertices()) = {(MiddleVertex (b,a,c))} ) by Def3; then {(MiddleVertex (a,b,c))} = {(MiddleVertex (b,a,c))} by A1, A2, XBOOLE_1:16; hence MiddleVertex (a,b,c) = MiddleVertex (b,a,c) by ZFMISC_1:3; ::_thesis: verum end; theorem :: HELLY:43 for T being _Tree for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (b,c,a) proof let T be _Tree; ::_thesis: for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (b,c,a) let a, b, c be Vertex of T; ::_thesis: MiddleVertex (a,b,c) = MiddleVertex (b,c,a) thus MiddleVertex (a,b,c) = MiddleVertex (b,a,c) by Th42 .= MiddleVertex (b,c,a) by Th41 ; ::_thesis: verum end; theorem Th44: :: HELLY:44 for T being _Tree for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (c,a,b) proof let T be _Tree; ::_thesis: for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (c,a,b) let a, b, c be Vertex of T; ::_thesis: MiddleVertex (a,b,c) = MiddleVertex (c,a,b) thus MiddleVertex (a,b,c) = MiddleVertex (a,c,b) by Th41 .= MiddleVertex (c,a,b) by Th42 ; ::_thesis: verum end; theorem :: HELLY:45 for T being _Tree for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (c,b,a) proof let T be _Tree; ::_thesis: for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (c,b,a) let a, b, c be Vertex of T; ::_thesis: MiddleVertex (a,b,c) = MiddleVertex (c,b,a) thus MiddleVertex (a,b,c) = MiddleVertex (c,a,b) by Th44 .= MiddleVertex (c,b,a) by Th41 ; ::_thesis: verum end; theorem Th46: :: HELLY:46 for T being _Tree for a, b, c being Vertex of T st c in (T .pathBetween (a,b)) .vertices() holds MiddleVertex (a,b,c) = c proof let T be _Tree; ::_thesis: for a, b, c being Vertex of T st c in (T .pathBetween (a,b)) .vertices() holds MiddleVertex (a,b,c) = c let a, b, c be Vertex of T; ::_thesis: ( c in (T .pathBetween (a,b)) .vertices() implies MiddleVertex (a,b,c) = c ) assume c in (T .pathBetween (a,b)) .vertices() ; ::_thesis: MiddleVertex (a,b,c) = c then (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c} by Lm1; hence MiddleVertex (a,b,c) = c by Def3; ::_thesis: verum end; theorem :: HELLY:47 for T being _Tree for a being Vertex of T holds MiddleVertex (a,a,a) = a proof let T be _Tree; ::_thesis: for a being Vertex of T holds MiddleVertex (a,a,a) = a let a be Vertex of T; ::_thesis: MiddleVertex (a,a,a) = a a in {a} by TARSKI:def_1; then a in (T .pathBetween (a,a)) .vertices() by Th30; hence MiddleVertex (a,a,a) = a by Th46; ::_thesis: verum end; theorem Th48: :: HELLY:48 for T being _Tree for a, b being Vertex of T holds MiddleVertex (a,a,b) = a proof let T be _Tree; ::_thesis: for a, b being Vertex of T holds MiddleVertex (a,a,b) = a let a, b be Vertex of T; ::_thesis: MiddleVertex (a,a,b) = a (T .pathBetween (a,b)) .first() = a by Th28; then A1: a in (T .pathBetween (a,b)) .vertices() by GLIB_001:88; MiddleVertex (a,a,b) = MiddleVertex (a,b,a) by Th41; hence MiddleVertex (a,a,b) = a by A1, Th46; ::_thesis: verum end; theorem Th49: :: HELLY:49 for T being _Tree for a, b being Vertex of T holds MiddleVertex (a,b,a) = a proof let T be _Tree; ::_thesis: for a, b being Vertex of T holds MiddleVertex (a,b,a) = a let a, b be Vertex of T; ::_thesis: MiddleVertex (a,b,a) = a MiddleVertex (a,a,b) = MiddleVertex (a,b,a) by Th41; hence MiddleVertex (a,b,a) = a by Th48; ::_thesis: verum end; theorem :: HELLY:50 for T being _Tree for a, b being Vertex of T holds MiddleVertex (a,b,b) = b proof let T be _Tree; ::_thesis: for a, b being Vertex of T holds MiddleVertex (a,b,b) = b let a, b be Vertex of T; ::_thesis: MiddleVertex (a,b,b) = b MiddleVertex (a,b,b) = MiddleVertex (b,a,b) by Th42; hence MiddleVertex (a,b,b) = b by Th49; ::_thesis: verum end; theorem Th51: :: HELLY:51 for T being _Tree for P1, P2 being Path of T for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not b in P2 .vertices() & not c in P1 .vertices() holds MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2))) proof let T be _Tree; ::_thesis: for P1, P2 being Path of T for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not b in P2 .vertices() & not c in P1 .vertices() holds MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2))) let P1, P2 be Path of T; ::_thesis: for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not b in P2 .vertices() & not c in P1 .vertices() holds MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2))) let a, b, c be Vertex of T; ::_thesis: ( P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not b in P2 .vertices() & not c in P1 .vertices() implies MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2))) ) assume that A1: ( P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) ) and A2: ( not b in P2 .vertices() & not c in P1 .vertices() ) ; ::_thesis: MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2))) ( not P1 c= P2 & not P2 c= P1 ) by A1, A2, Th37; then A3: (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P2))))} by A1, Lm2; (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(MiddleVertex (a,b,c))} by Def3; hence MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2))) by A3, ZFMISC_1:3; ::_thesis: verum end; theorem :: HELLY:52 for T being _Tree for P1, P2, P3, P4 being Path of T for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & P3 = T .pathBetween (b,a) & P4 = T .pathBetween (b,c) & not b in P2 .vertices() & not c in P1 .vertices() & not a in P4 .vertices() holds P1 . (len (maxPrefix (P1,P2))) = P3 . (len (maxPrefix (P3,P4))) proof let T be _Tree; ::_thesis: for P1, P2, P3, P4 being Path of T for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & P3 = T .pathBetween (b,a) & P4 = T .pathBetween (b,c) & not b in P2 .vertices() & not c in P1 .vertices() & not a in P4 .vertices() holds P1 . (len (maxPrefix (P1,P2))) = P3 . (len (maxPrefix (P3,P4))) let P1, P2, P3, P4 be Path of T; ::_thesis: for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & P3 = T .pathBetween (b,a) & P4 = T .pathBetween (b,c) & not b in P2 .vertices() & not c in P1 .vertices() & not a in P4 .vertices() holds P1 . (len (maxPrefix (P1,P2))) = P3 . (len (maxPrefix (P3,P4))) let a, b, c be Vertex of T; ::_thesis: ( P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & P3 = T .pathBetween (b,a) & P4 = T .pathBetween (b,c) & not b in P2 .vertices() & not c in P1 .vertices() & not a in P4 .vertices() implies P1 . (len (maxPrefix (P1,P2))) = P3 . (len (maxPrefix (P3,P4))) ) assume that A1: P1 = T .pathBetween (a,b) and A2: P2 = T .pathBetween (a,c) and A3: P3 = T .pathBetween (b,a) and A4: P4 = T .pathBetween (b,c) and A5: not b in P2 .vertices() and A6: not c in P1 .vertices() and A7: not a in P4 .vertices() ; ::_thesis: P1 . (len (maxPrefix (P1,P2))) = P3 . (len (maxPrefix (P3,P4))) now__::_thesis:_not_P4_c=_P3 assume P4 c= P3 ; ::_thesis: contradiction then A8: P4 .vertices() c= P3 .vertices() by Th13; c in P4 .vertices() by A4, Th29; then c in P3 .vertices() by A8; hence contradiction by A1, A3, A6, Th32; ::_thesis: verum end; then not c in P3 .vertices() by A3, A4, Th37; then A9: MiddleVertex (b,a,c) = P3 . (len (maxPrefix (P3,P4))) by A3, A4, A7, Th51; MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2))) by A1, A2, A5, A6, Th51; hence P1 . (len (maxPrefix (P1,P2))) = P3 . (len (maxPrefix (P3,P4))) by A9, Th42; ::_thesis: verum end; theorem Th53: :: HELLY:53 for T being _Tree for a, b, c being Vertex of T for S being non empty set st ( for s being set st s in S holds ( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) ) ) holds meet S <> {} proof let T be _Tree; ::_thesis: for a, b, c being Vertex of T for S being non empty set st ( for s being set st s in S holds ( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) ) ) holds meet S <> {} let a, b, c be Vertex of T; ::_thesis: for S being non empty set st ( for s being set st s in S holds ( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) ) ) holds meet S <> {} let S be non empty set ; ::_thesis: ( ( for s being set st s in S holds ( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) ) ) implies meet S <> {} ) assume A1: for s being set st s in S holds ( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) ) ; ::_thesis: meet S <> {} set m = MiddleVertex (a,b,c); set Pca = T .pathBetween (c,a); set Pbc = T .pathBetween (b,c); set Pac = T .pathBetween (a,c); set Pab = T .pathBetween (a,b); set VPab = (T .pathBetween (a,b)) .vertices() ; set VPac = (T .pathBetween (a,c)) .vertices() ; set VPbc = (T .pathBetween (b,c)) .vertices() ; set VPca = (T .pathBetween (c,a)) .vertices() ; (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(MiddleVertex (a,b,c))} by Def3; then A2: MiddleVertex (a,b,c) in (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) by TARSKI:def_1; then A3: MiddleVertex (a,b,c) in ((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices()) by XBOOLE_0:def_4; then A4: MiddleVertex (a,b,c) in (T .pathBetween (b,c)) .vertices() by XBOOLE_0:def_4; (T .pathBetween (c,a)) .vertices() = (T .pathBetween (a,c)) .vertices() by Th32; then A5: MiddleVertex (a,b,c) in (T .pathBetween (a,c)) .vertices() by A2, XBOOLE_0:def_4; A6: MiddleVertex (a,b,c) in (T .pathBetween (a,b)) .vertices() by A3, XBOOLE_0:def_4; now__::_thesis:_for_s_being_set_st_s_in_S_holds_ MiddleVertex_(a,b,c)_in_s let s be set ; ::_thesis: ( s in S implies MiddleVertex (a,b,c) in b1 ) assume A7: s in S ; ::_thesis: MiddleVertex (a,b,c) in b1 then A8: ex t being _Subtree of T st s = the_Vertices_of t by A1; percases ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by A1, A7; suppose ( a in s & b in s ) ; ::_thesis: MiddleVertex (a,b,c) in b1 then (T .pathBetween (a,b)) .vertices() c= s by A8, Th34; hence MiddleVertex (a,b,c) in s by A6; ::_thesis: verum end; suppose ( a in s & c in s ) ; ::_thesis: MiddleVertex (a,b,c) in b1 then (T .pathBetween (a,c)) .vertices() c= s by A8, Th34; hence MiddleVertex (a,b,c) in s by A5; ::_thesis: verum end; suppose ( b in s & c in s ) ; ::_thesis: MiddleVertex (a,b,c) in b1 then (T .pathBetween (b,c)) .vertices() c= s by A8, Th34; hence MiddleVertex (a,b,c) in s by A4; ::_thesis: verum end; end; end; hence meet S <> {} by SETFAM_1:def_1; ::_thesis: verum end; begin definition let F be set ; attrF is with_Helly_property means :: HELLY:def 4 for H being non empty set st H c= F & ( for x, y being set st x in H & y in H holds x meets y ) holds meet H <> {} ; end; :: deftheorem defines with_Helly_property HELLY:def_4_:_ for F being set holds ( F is with_Helly_property iff for H being non empty set st H c= F & ( for x, y being set st x in H & y in H holds x meets y ) holds meet H <> {} ); theorem :: HELLY:54 for T being _Tree for X being finite set st ( for x being set st x in X holds ex t being _Subtree of T st x = the_Vertices_of t ) holds X is with_Helly_property proof let T be _Tree; ::_thesis: for X being finite set st ( for x being set st x in X holds ex t being _Subtree of T st x = the_Vertices_of t ) holds X is with_Helly_property let X be finite set ; ::_thesis: ( ( for x being set st x in X holds ex t being _Subtree of T st x = the_Vertices_of t ) implies X is with_Helly_property ) assume A1: for x being set st x in X holds ex t being _Subtree of T st x = the_Vertices_of t ; ::_thesis: X is with_Helly_property defpred S1[ Nat] means for H being non empty finite set st card H = $1 & H c= X & ( for x, y being set st x in H & y in H holds x meets y ) holds meet H <> {} ; A2: for k being Nat st ( for n being Nat st n < k holds S1[n] ) holds S1[k] proof let k be Nat; ::_thesis: ( ( for n being Nat st n < k holds S1[n] ) implies S1[k] ) assume A3: for n being Nat st n < k holds S1[n] ; ::_thesis: S1[k] let H be non empty finite set ; ::_thesis: ( card H = k & H c= X & ( for x, y being set st x in H & y in H holds x meets y ) implies meet H <> {} ) assume that A4: card H = k and A5: H c= X and A6: for x, y being set st x in H & y in H holds x meets y ; ::_thesis: meet H <> {} percases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25; suppose k = 0 ; ::_thesis: meet H <> {} hence meet H <> {} by A4; ::_thesis: verum end; suppose k = 1 ; ::_thesis: meet H <> {} then consider x being Element of H such that A7: H = {x} by A4, GRAPH_5:5; x in H ; then ex t being _Subtree of T st x = the_Vertices_of t by A1, A5; hence meet H <> {} by A7, SETFAM_1:10; ::_thesis: verum end; supposeA8: k > 1 ; ::_thesis: meet H <> {} set cH = choose H; set A = H \ {(choose H)}; A9: card (H \ {(choose H)}) = (card H) - (card {(choose H)}) by EULER_1:4 .= k - 1 by A4, CARD_1:30 ; k - 1 > 1 - 1 by A8, XREAL_1:9; then reconsider A = H \ {(choose H)} as non empty finite set by A9; A10: A c= X by A5, XBOOLE_1:1; for x, y being set st x in A & y in A holds x meets y by A6; then reconsider mA = meet A as non empty set by A3, A9, A10, XREAL_1:44; set cA = choose A; set B = H \ {(choose A)}; A11: choose A in A ; then A12: card (H \ {(choose A)}) = (card H) - (card {(choose A)}) by EULER_1:4 .= k - 1 by A4, CARD_1:30 ; set C = {(choose H),(choose A)}; A13: meet {(choose H),(choose A)} = (choose H) /\ (choose A) by SETFAM_1:11; choose H meets choose A by A6, A11; then reconsider mC = meet {(choose H),(choose A)} as non empty set by A13, XBOOLE_0:def_7; k - 1 > 1 - 1 by A8, XREAL_1:9; then reconsider B = H \ {(choose A)} as non empty finite set by A12; A14: B c= X by A5, XBOOLE_1:1; for x, y being set st x in B & y in B holds x meets y by A6; then reconsider mB = meet B as non empty set by A3, A12, A14, XREAL_1:44; set a = choose mA; set b = choose mB; set c = choose mC; ( choose mC in mC & mC c= union {(choose H),(choose A)} ) by SETFAM_1:2; then consider cc being set such that A15: choose mC in cc and A16: cc in {(choose H),(choose A)} by TARSKI:def_4; choose H in H ; then {(choose H),(choose A)} c= X by A5, A11, A10, ZFMISC_1:32; then A17: ex cct being _Subtree of T st cc = the_Vertices_of cct by A1, A16; ( choose mA in mA & mA c= union A ) by SETFAM_1:2; then consider aa being set such that A18: choose mA in aa and A19: aa in A by TARSKI:def_4; ( choose mB in mB & mB c= union B ) by SETFAM_1:2; then consider bb being set such that A20: choose mB in bb and A21: bb in B by TARSKI:def_4; A22: ex bbt being _Subtree of T st bb = the_Vertices_of bbt by A1, A14, A21; ex aat being _Subtree of T st aa = the_Vertices_of aat by A1, A10, A19; then reconsider a = choose mA, b = choose mB, c = choose mC as Vertex of T by A18, A20, A22, A15, A17; A23: choose A <> choose H by ZFMISC_1:56; now__::_thesis:_for_s_being_set_st_s_in_H_holds_ (_ex_t_being__Subtree_of_T_st_s_=_the_Vertices_of_t_&_(_(_a_in_s_&_b_in_s_)_or_(_a_in_s_&_c_in_s_)_or_(_b_in_s_&_c_in_s_)_)_) let s be set ; ::_thesis: ( s in H implies ( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) ) ) assume A24: s in H ; ::_thesis: ( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) ) hence ex t being _Subtree of T st s = the_Vertices_of t by A1, A5; ::_thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) thus ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) ::_thesis: verum proof percases ( s = choose H or s = choose A or ( s <> choose H & s <> choose A ) ) ; suppose s = choose H ; ::_thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) then ( s in {(choose H),(choose A)} & s in B ) by A23, TARSKI:def_2, ZFMISC_1:56; hence ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by SETFAM_1:def_1; ::_thesis: verum end; supposeA25: s = choose A ; ::_thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) then s in {(choose H),(choose A)} by TARSKI:def_2; hence ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by A25, SETFAM_1:def_1; ::_thesis: verum end; suppose ( s <> choose H & s <> choose A ) ; ::_thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) then ( s in A & s in B ) by A24, ZFMISC_1:56; hence ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by SETFAM_1:def_1; ::_thesis: verum end; end; end; end; hence meet H <> {} by Th53; ::_thesis: verum end; end; end; A26: for n being Nat holds S1[n] from NAT_1:sch_4(A2); let H be non empty set ; :: according to HELLY:def_4 ::_thesis: ( H c= X & ( for x, y being set st x in H & y in H holds x meets y ) implies meet H <> {} ) assume that A27: H c= X and A28: for x, y being set st x in H & y in H holds x meets y ; ::_thesis: meet H <> {} reconsider H9 = H as finite set by A27; card H9 = card H9 ; hence meet H <> {} by A26, A27, A28; ::_thesis: verum end;