:: Helly property for subtrees
::  by Jessica Enright and Piotr Rudnicki
::
:: Received January 10, 2008
:: Copyright (c) 2008-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, FINSEQ_1, FUNCT_1, GRAPH_2, ARYTM_3, NAT_1,
      XXREAL_0, SUBSET_1, TREES_1, TARSKI, CARD_1, ORDINAL1, FINSET_1,
      MEMBERED, RELAT_1, ORDINAL4, GLIB_000, GLIB_001, ABIAN, ZFMISC_1,
      ARYTM_1, GRAPH_1, RCOMP_1, SETFAM_1, HELLY;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FINSET_1, CARD_1, NUMBERS,
      XCMPLX_0, XXREAL_0, SETFAM_1, FUNCT_1, FINSEQ_1, MEMBERED, NAT_1,
      TREES_1, XXREAL_2, ABIAN, GRAPH_2, GLIB_000, GLIB_001, GLIB_002,
      FINSEQ_6;
 constructors DOMAIN_1, SETFAM_1, NAT_1, GRAPH_2, GLIB_001, GLIB_002, XXREAL_2,
      RELSET_1, RAT_1, FINSEQ_6;
 registrations FINSET_1, XREAL_0, XXREAL_0, NAT_1, INT_1, RELAT_1, FINSEQ_1,
      ABIAN, MEMBERED, GLIB_000, GLIB_001, GLIB_002, XXREAL_2, CARD_1, FUNCT_1,
      XBOOLE_0, ORDINAL1, FINSEQ_6;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
 definitions TARSKI, XBOOLE_0, GLIB_001;
 equalities GLIB_001;
 expansions TARSKI, XBOOLE_0, GLIB_001;
 theorems TARSKI, NAT_1, SETFAM_1, XBOOLE_0, XBOOLE_1, GRFUNC_1, FUNCT_1,
      ZFMISC_1, ORDINAL1, FINSEQ_1, FINSEQ_2, FINSEQ_3, INT_1, EULER_1, CARD_1,
      XREAL_1, XXREAL_0, CHORD, ABIAN, GLIB_000, GLIB_001, GLIB_002, MSSCYC_1,
      MEMBERED, GRAPH_2, XXREAL_2, FINSEQ_4, PRE_CIRC, FINSEQ_6;
 schemes NAT_1, FINSEQ_1;

begin :: General preliminaries

theorem
  for p being non empty FinSequence holds <*p.1*>^'p = p
proof
  let p be non empty FinSequence;
  set o = <*p.1*>^'p;
A1: len o +1 = len <*p.1*> + len p by FINSEQ_6:139;
A2: len <*p.1*> = 1 by FINSEQ_1:39;
A3: now
    let k be Nat such that
A4: 1<=k and
A5: k <= len o;
    per cases;
    suppose
A6:   k <= len <*p.1*>;
      then k <= 1 by FINSEQ_1:39;
      then
A7:   k = 1 by A4,XXREAL_0:1;
      hence o.k = <*p.1*>.1 by A6,FINSEQ_6:140
        .= p.k by A7,FINSEQ_1:40;
    end;
    suppose
      k > len <*p.1*>;
      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 o.k = p.k by A2,A8,A9,FINSEQ_6:141;
    end;
  end;
  len o +1 = 1 + len p by A1,FINSEQ_1:39;
  hence thesis by A3,FINSEQ_1:14;
end;

definition
  let p, q be FinSequence;
  func maxPrefix(p,q) -> FinSequence means
  :Def1:
  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
  proof
    deffunc F(set) = $1;
    defpred P[set] means
     ex r being FinSequence st r c= p & r c= q & len r = $1;
    set S = { F(k) where k is Nat : k <= len p & P[k] };
A1: for x being object st x in S holds x is natural
    proof
      let x be object;
      assume x in S;
      then ex n being Nat st x = n & n <= len p & P[n];
      hence thesis;
    end;
A2: S is finite from FINSEQ_1:sch 6;
    {} c= p & {} c= q & len {} = 0;
    then 0 in S;
    then reconsider S as finite non empty natural-membered set by A1,A2,
MEMBERED:def 6;
    set maxk = max S;
    maxk in S by XXREAL_2:def 8;
    then consider K being Nat such that
A3: K = maxk and
    K <= len p and
A4: P[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;
    thus R c= p by A5;
    thus R c= q by A6;
    let r be FinSequence such that
A8: r c= p and
A9: r c= q;
    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
      let x be object;
      assume
A11:  x in dom r;
      hence r.x = p.x by A8,GRFUNC_1:2
        .= R.x by A5,A10,A11,GRFUNC_1:2;
    end;
    hence thesis by A10,GRFUNC_1:2;
  end;
  uniqueness;
  commutativity;
end;

theorem
  for p, q being FinSequence holds p is_a_prefix_of q iff maxPrefix(p,q) = p
by Def1;

theorem Th3:
  for p, q being FinSequence holds len maxPrefix(p,q)<= len p
proof
  let p, q be FinSequence;
  maxPrefix(p,q) c= p by Def1;
  hence thesis by FINSEQ_1:63;
end;

theorem Th4:
  for p being non empty FinSequence holds <*p.1*> is_a_prefix_of p
proof
  let p be non empty FinSequence;
A1: now
    let x be object;
A2: dom <*p.1*> = Seg 1 by FINSEQ_1:def 8;
    assume x in dom <*p.1*>;
    then x = 1 by A2,FINSEQ_1:2,TARSKI:def 1;
    hence <*p.1*>.x = p.x by FINSEQ_1:def 8;
  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 thesis by A1,GRFUNC_1:2;
end;

theorem Th5:
  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 such that
A1: p.1 = q.1 and
A2: 1 > len maxPrefix(p,q);
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;
end;

theorem Th6:
  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;
  let j be Nat such that
A1: j <= len maxPrefix(p,q);
A2: maxPrefix(p,q) c= p by Def1;
  per cases;
  suppose
A3: j = 0;
    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;
  end;
  suppose
    j <> 0;
    then 0+1 <= j by NAT_1:13;
    then j in dom maxPrefix(p,q) by A1,FINSEQ_3:25;
    hence thesis by A2,GRFUNC_1:2;
  end;
end;

theorem Th7:
  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;
  let j be Nat such that
A1: j <= len maxPrefix(p,q);
  thus p.j = maxPrefix(p,q).j by A1,Th6
    .= q.j by A1,Th6;
end;

theorem Th8:
  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;
A1: maxPrefix(p,q) c= p by Def1;
  hereby
    assume
A2: not p c= q;
A3: now
      assume len maxPrefix(p,q) = len p;
      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;
    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;
  end;
  assume that
A5: len maxPrefix(p,q) < len p and
A6: p c= q;
  p c= maxPrefix(p,q) by A6,Def1;
  hence contradiction by A5,A1,XBOOLE_0:def 10;
end;

theorem Th9:
  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 such 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);
  set dI = len maxPrefix(p,q);
  set mP = maxPrefix(p,q);
  set lmP = mP^<*p.(dI+1)*>;
A4: now
    let x be object such that
A5: x in dom lmP;
    reconsider n = x as Nat by A5;
A6: 1 <= n by A5,FINSEQ_3:25;
    n <= len lmP by A5,FINSEQ_3:25;
    then
A7: n <= len mP + 1 by FINSEQ_2:16;
    per cases by A7,NAT_1:8;
    suppose
A8:   n <= dI;
      then n in dom mP by A6,FINSEQ_3:25;
      hence lmP.x = mP.x by FINSEQ_1:def 7
        .= q.x by A8,Th6;
    end;
    suppose
      n = dI + 1;
      hence lmP.x = q.x by A3,FINSEQ_1:42;
    end;
  end;
A9: now
    let x be object such that
A10: x in dom lmP;
    reconsider n = x as Nat by A10;
A11: 1 <= n by A10,FINSEQ_3:25;
    n <= len lmP by A10,FINSEQ_3:25;
    then
A12: n <= len mP + 1 by FINSEQ_2:16;
    per cases by A12,NAT_1:8;
    suppose
A13:  n <= dI;
      then n in dom mP by A11,FINSEQ_3:25;
      hence lmP.x = mP.x by FINSEQ_1:def 7
        .= p.x by A13,Th6;
    end;
    suppose
      n = dI + 1;
      hence lmP.x = p.x by FINSEQ_1:42;
    end;
  end;
A14: len lmP = len mP + 1 by FINSEQ_2:16;
  len mP < len q by A2,Th8;
  then len lmP <= len q by A14,NAT_1:13;
  then dom lmP c= dom q by FINSEQ_3:30;
  then
A15: lmP c= q by A4,GRFUNC_1:2;
  len mP < len p by A1,Th8;
  then len lmP <= len p by A14,NAT_1:13;
  then dom lmP c= dom p by FINSEQ_3:30;
  then lmP c= p by A9,GRFUNC_1:2;
  then lmP c= mP by A15,Def1;
  then len lmP <= len mP by FINSEQ_1:63;
  then len mP + 1 <= len mP by FINSEQ_2:16;
  hence contradiction by NAT_1:13;
end;

begin :: Graph preliminaries

theorem Th10:
  for G being _Graph, W be Walk of G, m, n being Nat holds len W
  .cut(m,n) <= len W
proof
  let G be _Graph, W be Walk of G, m, n be Nat;
  reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def 12;
  per cases;
  suppose
    m is odd & n is odd & m <= n & 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 thesis;
  end;
  suppose
    not (m is odd & n is odd & m <= n & n <= len W);
    hence thesis by GLIB_001:def 11;
  end;
end;

theorem
  for G being _Graph, W being Walk of G, m, n being Nat st W.cut(m,n) is
  non trivial holds W is non trivial
proof
  let G be _Graph, W be Walk of G, m, n be Nat such that
A1: W.cut(m,n) is non trivial and
A2: W is trivial;
  reconsider 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 thesis by A1;
end;

theorem Th12:
  for G being _Graph, W being Walk of G for m, n, i being odd Nat
st m <= n & n <= len W & i <= len W.cut(m,n) 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, W be Walk of G;
  let m, n, i being odd Nat such that
A1: m <= n and
A2: n <= len W and
A3: i <= len W.cut(m,n);
  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 j is odd Element of NAT by INT_1:3;
  then reconsider j as odd Nat;
  take j;
  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;
  thus j = m+i-1;
  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 thesis by A2,XXREAL_0:2;
end;

registration
  let G be _Graph;
  cluster -> non empty for Walk of G;
  correctness by CARD_1:27;
end;

theorem Th13:
  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, W1, W2 be Walk of G such that
A1: W1 c= W2;
  let x be object;
  assume x in W1.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 thesis by A4,GLIB_001:87;
end;

theorem
  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, W1, W2 be Walk of G such that
A1: W1 c= W2;
  let x be object;
  assume x in W1.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 thesis by A2,A5,GLIB_001:99;
end;

theorem Th15:
  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, W1, W2 be Walk of G;
  set W1a = W1.append(W2);
  per cases;
  suppose
    W1.last() = W2.first();
    then len W1 <= len W1a by GLIB_001:29;
    then
A1: dom W1 c= dom W1a by FINSEQ_3:30;
    for x being object st x in dom W1 holds W1.x = W1a.x by GLIB_001:32;
    hence thesis by A1,GRFUNC_1:2;
  end;
  suppose
    W1.last() <> W2.first();
    hence thesis by GLIB_001:def 10;
  end;
end;

theorem Th16:
  for G being _Graph, W1,W2 being Walk of G st W1 is trivial & W1
  .last() = W2.first() holds W1.append(W2) = W2
proof
  let G be _Graph, W1,W2 be Walk of G such that
A1: W1 is trivial and
A2: W1.last() = W2.first();
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
    let k be Nat such that
A5: 1 <= k and
A6: k <= len W1.append(W2);
    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;
  end;
  hence thesis by A4,FINSEQ_1:14;
end;

theorem Th17:
  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, W1, W2 be Trail of G such that
A1: W1.last() = W2.first() and
A2: W1.edges() misses W2.edges();
  set W = W1.append(W2);
  now
    let m,n be even Element of NAT such that
A3: 1 <= m and
A4: m < n and
A5: n <= len W;
    1 <= n by A3,A4,XXREAL_0:2;
    then
A6: n in dom W by A5,FINSEQ_3:25;
    m <= len W by A4,A5,XXREAL_0:2;
    then
A7: m in dom W by A3,FINSEQ_3:25;
    per cases by A6,GLIB_001:34;
    suppose
A8:   n in dom W1;
      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 = W.m by GLIB_001:32;
      W1.m <> W1.n by A3,A4,A9,GLIB_001:138;
      hence W.m <> W.n by A8,A10,GLIB_001:32;
    end;
    suppose
      ex k being Element of NAT st k < len W2 & n = len W1 + k;
      then consider k being Element of NAT such that
A11:  k < len W2 and
A12:  n = len W1 + k;
      reconsider k as odd Element of NAT by A12;
A13:  W.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;
      per cases by A7,GLIB_001:34;
      suppose
A16:    m in dom W1;
        then 1 <= m & m <= len W1 by FINSEQ_3:25;
        then
A17:    W1.m in W1.edges() by GLIB_001:99;
        W.m = W1.m by A16,GLIB_001:32;
        hence W.m <> W.n by A2,A13,A15,A17,XBOOLE_0:3;
      end;
      suppose
        ex l being Element of NAT st l < len W2 & m = len W1 + l;
        then consider l being Element of NAT such that
A18:    l < len W2 and
A19:    m = len W1 + l;
        reconsider 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;
        W.m = W2.(l+1) by A1,A18,A19,GLIB_001:33;
        hence W.m <> W.n by A13,A14,A20,GLIB_001:138;
      end;
    end;
  end;
  hence thesis by GLIB_001:138;
end;

theorem Th18:
  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, P1, P2 be Path of G such 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()};
  thus P1.append(P2) is Trail-like by A1,A4,Th17;
  set P = P1.append(P2);
  let m, n be odd Element of NAT such that
A7: m < n and
A8: n <= len P and
A9: P.m = P.n and
A10: m <> 1 or n <> len P;
A11: 1 <= m by ABIAN:12;
  1 <= n by ABIAN:12;
  then
A12: n in dom P by A8,FINSEQ_3:25;
  m <= len P by A7,A8,XXREAL_0:2;
  then
A13: m in dom P by A11,FINSEQ_3:25;
  per cases by A12,GLIB_001:34;
  suppose
    ex k being Element of NAT st k < len P2 & n = len P1 + k;
    then consider k being Element of NAT such that
A14: k < len P2 and
A15: n = len P1 + k;
A16: P.n = P2.(k+1) by A1,A14,A15,GLIB_001:33;
    reconsider 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;
    per cases by A13,GLIB_001:34;
    suppose
      ex k being Element of NAT st k < len P2 & m = len P1 + k;
      then consider l being Element of NAT such that
A19:  l < len P2 and
A20:  m = len P1 + l;
A21:  P.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 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;
    end;
    suppose
A24:  m in dom P1;
      set x = P1.m;
A25:  P1.m = P.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:  x in P1.vertices() /\ P2.vertices() by A9,A16,A18,A25,XBOOLE_0:def 4;
      per cases by A6,A27,TARSKI:def 2;
      suppose
A28:    x = P1.last();
        then
A29:    m >= len P1 by GLIB_001:def 28,A2;
A30:    2*0+1 >= k+1 by A1,A3,A9,A16,A17,A25,A28,GLIB_001:def 28;
        1 <= k+1 by NAT_1:11;
        then 1 = k+1 by A30,XXREAL_0:1;
        hence contradiction by A7,A15,A29;
      end;
      suppose
A31:    x = P1.first();
        then
A32:    x = P1.(2*0+1);
A33:    now
          assume m <> 1;
          then 1 < m by A11,XXREAL_0:1;
          then x = P1.last() by A26,A32,GLIB_001:def 28;
          hence contradiction by A2,A31;
        end;
        now
          assume k+1 = len P2;
          then len P +1 = len P1 + (k+1) by A1,GLIB_001:28;
          hence contradiction by A10,A15,A33;
        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;
      end;
    end;
  end;
  suppose
A35: n in dom P1;
    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 = P.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;
  end;
end;

theorem Th19:
  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 Path-like
proof
  let G be _Graph, P1, P2 be Path of G such that
A1: P1.last() = P2.first() and
A2: P1 is open and
A3: P2 is open and
A4: P1.vertices() /\ P2.vertices() = {P1.last()};
  set P = P1.append(P2);
  thus P is open
  proof
    assume
A5: P.first() = P.last();
    P.first() = P1.first() & P.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;
  end;
A6: now
A7: P1.first() in P1.vertices() by GLIB_001:88;
    assume P1.first() in P2.vertices();
    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;
  end;
A8: P1.edges() misses P2.edges()
  proof
    assume P1.edges() /\ P2.edges() <> {};
    then consider x being object 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;
    per cases;
    suppose
A19:  v1 <> v2;
      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;
    end;
    suppose
A25:  v1 = v2;
      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;
    end;
  end;
  P1.vertices() /\ P2.vertices() c= {P1.first(), P1.last()} by A4,ZFMISC_1:7;
  hence thesis by A1,A2,A3,A8,A6,Th18;
end;

theorem Th20:
  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, P1, P2 be Path of G such 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()};
  set P = P1.append(P2);
  P.first() = P1.first() & P.last() = P2.last() by A1,GLIB_001:30;
  hence P is closed by A2;
  thus P is Path-like by A1,A2,A3,A4,Th18;
  P1.first() <> P1.last() by A3;
  then P1 is non trivial by GLIB_001:127;
  then
A5: len P1 >= 3 by GLIB_001:125;
  len P >= len P1 by A1,GLIB_001:29;
  then len P >= 3 by A5,XXREAL_0:2;
  hence thesis by GLIB_001:125;
end;

theorem
  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, W1, W2 be Walk of G, k be odd Nat such 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;
  let j be Nat such that
A4: 1 <= j and
A5: j <= k;
  per cases;
  suppose
    j is odd;
    hence thesis by A3,A5;
  end;
  suppose
    j is even;
    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 thesis by A7,A9,A8,GLIB_000:def 20;
  end;
end;

theorem Th22:
  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, W1, W2 be Walk of G;
  assume that
A1: W1.first() = W2.first() and
A2: len maxPrefix(W1,W2) is even;
  set dI = len maxPrefix(W1,W2);
  reconsider dIp = dI-1 as odd Element of NAT by A1,A2,Th5,INT_1:5;
A3: dIp < dI by XREAL_1:146;
  set mP = maxPrefix(W1,W2);
  set lmP = mP^<*W1.(dI+1)*>;
A4: len lmP = len mP + 1 by FINSEQ_2:16;
A5: now
    let x be object such that
A6: x in dom lmP;
    reconsider n = x as Nat by A6;
A7: 1 <= n by A6,FINSEQ_3:25;
    n <= len lmP by A6,FINSEQ_3:25;
    then
A8: n <= len mP + 1 by FINSEQ_2:16;
    per cases by A8,NAT_1:8;
    suppose
A9:   n <= dI;
      then n in dom mP by A7,FINSEQ_3:25;
      hence lmP.x = mP.x by FINSEQ_1:def 7
        .= W1.x by A9,Th6;
    end;
    suppose
      n = dI + 1;
      hence lmP.x = W1.x by FINSEQ_1:42;
    end;
  end;
A10: dI = dIp+1;
A11: dI <= len W2 by Th3;
  then dIp < len W2 by XREAL_1:146,XXREAL_0:2;
  then
A12: W2.dI Joins W2.dIp, W2.(dIp+2), G by A10,GLIB_001:def 3;
A13: dI <= len W1 by Th3;
  then dIp < len W1 by XREAL_1:146,XXREAL_0:2;
  then
A14: W1.dI Joins W1.dIp, W1.(dIp+2), G by A10,GLIB_001:def 3;
  W1.dI = W2.dI 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
    let x be object such that
A17: x in dom lmP;
    reconsider n = x as Nat by A17;
A18: 1 <= n by A17,FINSEQ_3:25;
    n <= len lmP by A17,FINSEQ_3:25;
    then
A19: n <= len mP + 1 by FINSEQ_2:16;
    per cases by A19,NAT_1:8;
    suppose
A20:  n <= dI;
      then n in dom mP by A18,FINSEQ_3:25;
      hence lmP.x = mP.x by FINSEQ_1:def 7
        .= W2.x by A20,Th6;
    end;
    suppose
A21:  n = dI + 1;
      hence lmP.x = W1.(dI+1) by FINSEQ_1:42
        .= W2.x by A3,A15,A21,Th7;
    end;
  end;
  dI < len W2 by A2,A11,XXREAL_0:1;
  then len lmP <= len W2 by A4,NAT_1:13;
  then dom lmP c= dom W2 by FINSEQ_3:30;
  then
A22: lmP c= W2 by A16,GRFUNC_1:2;
  dI < len W1 by A2,A13,XXREAL_0:1;
  then len lmP <= len W1 by A4,NAT_1:13;
  then dom lmP c= dom W1 by FINSEQ_3:30;
  then lmP c= W1 by A5,GRFUNC_1:2;
  then lmP c= mP by A22,Def1;
  then len lmP <= len mP by FINSEQ_1:63;
  then len mP + 1 <= len mP by FINSEQ_2:16;
  hence contradiction by NAT_1:13;
end;

theorem Th23:
  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, W1, W2 be Walk of G;
  assume W1.first() = W2.first() & not W1 c= W2;
  then len maxPrefix(W1,W2) < len W1 & len maxPrefix(W1,W2) is odd Nat by Th8
,Th22;
  hence thesis by CHORD:4;
end;

theorem Th24:
  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, W1, W2 be Walk of G such 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);
  set dI = len maxPrefix(W1,W2);
A5: dI is odd by A1,Th22;
  dI < len W1 by A2,Th8;
  then
A6: W1.(dI+1) Joins W1.dI,W1.(dI+2), G by A5,GLIB_001:def 3;
A7: W1.dI = W2.dI by Th7;
  dI < len W2 by A3,Th8;
  then
A8: W2.(dI+1) Joins W2.dI,W2.(dI+2), G by A5,GLIB_001:def 3;
  W1.(dI +1) <> W2.(dI +1) by A2,A3,Th9;
  hence contradiction by A4,A7,A6,A8,GLIB_000:def 20;
end;

begin :: Trees

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
  proof
    let W be Walk of T such that
A1: W is Trail-like;
    defpred P[Nat] means $1 is odd & $1 <= len W & ex k being odd Element of
    NAT st k < $1 & W.k = W.$1;
    assume not W is Path-like;
    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;
    then
A2: ex p being Nat st P[p];
    consider p being Nat such that
A3: P[p] and
A4: for r being Nat st P[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 Wc + k = P+1 by A3,A5,GLIB_001:36;
    then len Wc <> 1 by A5;
    then
A7: Wc is non trivial by GLIB_001:126;
A8: Wc.last() = W.p by A3,A5,GLIB_001:37;
A9: Wc is Path-like
    proof
      assume not thesis;
      then consider m, n being odd Element of NAT such that
A10:  m < n and
A11:  n <= len Wc and
A12:  Wc.m = Wc.n and
A13:  m <> 1 or n <> len Wc by A1;
A14:  m < len Wc by A10,A11,XXREAL_0:2;
      consider kn1 being odd Nat such that
A15:  Wc.n = W.kn1 and
A16:  kn1 = k+n-1 and
A17:  kn1 <= len W by A3,A5,A11,Th12;
      reconsider kn1 as odd Element of NAT by ORDINAL1:def 12;
A18:  1 <= m by ABIAN:12;
      m <= len Wc by A10,A11,XXREAL_0:2;
      then consider km1 being odd Nat such that
A19:  Wc.m = W.km1 and
A20:  km1 = k+m-1 and
A21:  km1 <= len W by A3,A5,Th12;
      reconsider km1 as odd Element of NAT by ORDINAL1:def 12;
      per cases by A11,XXREAL_0:1;
      suppose
        n < len Wc;
        then k+n < k+len Wc 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;
      end;
      suppose
A23:    n = len Wc;
        k+m < len Wc + 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;
      end;
    end;
    Wc.first() = W.k by A3,A5,GLIB_001:37;
    then Wc is closed by A6,A8;
    then Wc is Cycle-like by A7,A9;
    hence contradiction by GLIB_002:def 2;
  end;
end;

theorem Th25:
  for T being _Tree for P being Path of T st P is non trivial holds P is open
by GLIB_001:def 31,GLIB_002:def 2;

registration
  let T be _Tree;
  cluster non trivial -> open for Path of T;
  correctness by Th25;
end;

theorem Th26: :: Only for _Tree as it is not true for cyclic paths
  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, P be Path of T, i, j be odd Nat such that
A1: i < j and
A2: j <= len P and
A3: P.i = P.j;
  reconsider i, 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: P is non 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;
end;

theorem Th27:
  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;
  let a, b be Vertex of T;
  let P1, P2 be Path of T such that
A1: P1 is_Walk_from a, b and
A2: P2 is_Walk_from a, b;
  set di = len maxPrefix(P1,P2);
A3: P1.first() = a & P2.first() = a by A1,A2;
  then reconsider di as odd Element of NAT by Th22;
  defpred P[Nat] means $1 is odd & di < $1 & $1 <= len P2 & P2.$1 in P1
  .vertices();
  assume
A4: P1 <> P2;
A5: not P2 c= P1
  proof
    assume
A6: P2 c= P1;
    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;
    P2.len P2 = P2.last() .= b by A2;
    hence contradiction by A7,A8,A9,Th26;
  end;
A10: ex k being Nat st P[k]
  proof
    take k = len P2;
    thus k is odd;
    di +2 <= len P2 & di < di+2 by A3,A5,Th23,NAT_1:19;
    hence di < k by XXREAL_0:2;
    thus k <= len P2;
    P2.k = P2.last() .= b by A2
      .= P1.last() by A1;
    hence thesis by GLIB_001:88;
  end;
  consider ei being Nat such that
A11: P[ei] and
A12: for n being Nat st P[n] holds ei <= n from NAT_1:sch 5(A10);
  reconsider ei as odd Element of NAT by A11,ORDINAL1:def 12;
  set e = P2.ei;
  set fi = P1.find(e);
  set pde = P2.cut(di,ei), pdf = P1.cut(di,fi);
A13: fi <= len P1 by A11,GLIB_001:def 19;
  set rpdf = pdf.reverse();
A14: rpdf.vertices() = pdf.vertices() by GLIB_001:92;
  set C = pde.append(rpdf);
  set d = P1.di;
A15: P2.di = P1.di by Th7;
  then
A16: pde.first() = d by A11,GLIB_001:37;
A17: e = P1.fi by A11,GLIB_001:def 19;
  len P2 <> 1
  proof
    assume len P2 = 1;
    then di < 1 by A11,XXREAL_0:2;
    hence contradiction by ABIAN:12;
  end;
  then
A18: not P2 is trivial by GLIB_001:126;
A19: di < fi
  proof
    assume di >= fi;
    then P1.fi = P2.fi & ei > fi by A11,Th7,XXREAL_0:2;
    then P2.first() = e & P2.last() = e by A11,A17,GLIB_001:def 28;
    hence contradiction by A18,GLIB_001:def 24;
  end;
  then
A20: pdf is non trivial by A13,GLIB_001:131;
  then
A21: P1 is non trivial;
  fi <= len P1 by A11,GLIB_001:def 19;
  then
A22: rpdf.vertices() c= P1.vertices() by A19,A14,GLIB_001:94;
A23: pde.vertices() /\ rpdf.vertices() c= {e, d}
  proof
    assume not thesis;
    then consider g being object such that
A24: g in pde.vertices() /\ rpdf.vertices() and
A25: not g in {e, d};
    g in pde.vertices() by A24,XBOOLE_0:def 4;
    then consider gii being odd Element of NAT such that
A26: gii <= len pde and
A27: pde.gii = g by GLIB_001:87;
    consider gi being odd Nat such that
A28: P2.gi = pde.gii and
A29: gi = di+gii-1 and
A30: gi <= len P2 by A11,A26,Th12;
    reconsider gi as odd Element of NAT by ORDINAL1:def 12;
A31: gii >= 1 by ABIAN:12;
A32: gi < ei
    proof
A33:  len pde + di = ei+1 by A11,GLIB_001:36;
      assume
A34:  gi >= ei;
      per cases by A34,XXREAL_0:1;
      suppose
        gi = ei;
        then pde.gii = pde.last() by A29,A33
          .= e by A11,GLIB_001:37;
        hence contradiction by A25,A27,TARSKI:def 2;
      end;
      suppose
        gi > ei;
        then gi+1 > ei+1 by XREAL_1:6;
        hence contradiction by A26,A29,A33,XREAL_1:6;
      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;
      then di+gii > gi+1 by A35,XREAL_1:8;
      hence contradiction by A29;
    end;
    g in rpdf.vertices() by A24,XBOOLE_0:def 4;
    hence contradiction by A12,A22,A27,A28,A30,A36,A32;
  end;
A37: pde.last() = e by A11,GLIB_001:37;
  pdf.first() = d by A13,A19,GLIB_001:37;
  then
A38: rpdf.last() = d by GLIB_001:22;
  pdf.last() = e by A13,A17,A19,GLIB_001:37;
  then
A39: rpdf.first() = e by GLIB_001:22;
  {e, d} c= pde.vertices() /\ rpdf.vertices()
  proof
    let x be object;
    assume
A40: x in {e, d};
    per cases by A40,TARSKI:def 2;
    suppose
      x = e;
      then x in pde.vertices() & x in rpdf.vertices() by A37,A39,GLIB_001:88;
      hence thesis by XBOOLE_0:def 4;
    end;
    suppose
      x = d;
      then x in pde.vertices() & x in rpdf.vertices() by A16,A38,GLIB_001:88;
      hence thesis by XBOOLE_0:def 4;
    end;
  end;
  then
A41: pde.vertices() /\ rpdf.vertices() = {e, d} by A23;
A42: pde is non trivial by A11,GLIB_001:131;
  then
A43: P2 is non trivial;
A44: not P1 c= P2
  proof
    assume
A45: P1 c= P2;
    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;
    P1.len P1 = P1.last() .= b by A1;
    hence contradiction by A46,A47,A48,Th26;
  end;
A49: pde.edges() misses rpdf.edges()
  proof
A50: pdf.vertices() = rpdf.vertices() by GLIB_001:92;
A51: pdf.edges() = rpdf.edges() by GLIB_001:107;
    assume pde.edges() /\ rpdf.edges() <> {};
    then consider x being object such that
A52: x in pde.edges() /\ rpdf.edges() by XBOOLE_0:def 1;
    x in rpdf.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 pdf and
A54: u1 = pdf.m and
    x = pdf.(m+1) and
A55: u2 = pdf.(m+2) and
A56: x Joins u1, u2, T by A51,GLIB_001:103;
    x in pde.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 pde and
A58: v1 = pde.n and
    x = pde.(n+1) and
A59: v2 = pde.(n+2) and
A60: x Joins v1, v2, T by GLIB_001:103;
A61: n+0 < n+2 by XREAL_1:8;
    per cases;
    suppose
A62:  v1 <> v2;
A63:  n+2 = n+1+1;
      then
A64:  n+1 < len pde by A57,NAT_1:13;
      then
A65:  pde.(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 as Element of NAT by ORDINAL1:def 12;
A67:  u2 in pdf.vertices() by A53,A55,GLIB_001:87;
      m+0 < m+2 by XREAL_1:8;
      then
A68:  m <= len pdf by A53,XXREAL_0:2;
      then u1 in pdf.vertices() by A54,GLIB_001:87;
      then
A69:  {u1, u2} c= rpdf.vertices() by A50,A67,ZFMISC_1:32;
A70:  m+2 = m+1+1;
      then
A71:  m+1 < len pdf by A53,NAT_1:13;
      then
A72:  pdf.(m+2) = P1.(di+(m+1)) by A13,A19,A70,GLIB_001:36;
      n <= len pde by A57,A61,XXREAL_0:2;
      then
A73:  v1 in pde.vertices() by A58,GLIB_001:87;
      v2 in pde.vertices() by A57,A59,GLIB_001:87;
      then
A74:  {v1, v2} c= pde.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 = e or v1 = d by A41,A74,A69,XBOOLE_1:19,ZFMISC_1:22;
      n+0 < n+2 by XREAL_1:8;
      then n <= len pde by A57,XXREAL_0:2;
      then
A77:  ni < len pde by A66,NAT_1:13;
      then
A78:  pde.n = P2.(di+ni) by A11,A66,GLIB_001:36;
A79:  P2.(di+2) = e
      proof
        per cases by A41,A62,A75,A74,A69,A76,XBOOLE_1:19,ZFMISC_1:22;
        suppose
A80:      v1 = e & v2 = d;
          di+(n+2) <= len pde +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() = d & P2.last() = d by A15,A59,A65,A80,A81,
GLIB_001:def 28;
          hence thesis by A43,GLIB_001:def 24;
        end;
        suppose
A82:      v1 = d & v2 = e;
          ni = 0
          proof
            di+ni < len pde +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;
            reconsider ni as even Element of NAT by A66;
            di+0 < di+ni by A84,XREAL_1:6;
            then P2.first() = d & P2.last() = d by A15,A58,A78,A82,A83,
GLIB_001:def 28;
            hence contradiction by A43,GLIB_001:def 24;
          end;
          hence thesis by A11,A59,A66,A64,A82,GLIB_001:36;
        end;
      end;
      consider im being Nat such that
A85:  m = im+1 by NAT_1:6;
A86:  v2 = e or v2 = d by A41,A75,A74,A69,XBOOLE_1:19,ZFMISC_1:22;
      reconsider im as Element of NAT by ORDINAL1:def 12;
A87:  im < len pdf by A68,A85,NAT_1:13;
      then
A88:  pdf.m = P1.(di+im) by A13,A19,A85,GLIB_001:36;
      P1.(di+2) = e
      proof
        per cases by A60,A56,A62,A76,A86,GLIB_000:15;
        suppose
A89:      u1 = e & u2 = d;
          di+(m+2) <= len pdf +di by A53,XREAL_1:6;
          then di+m+1+1 <= fi+1 by A13,A19,GLIB_001:36;
          then di+m+1 <= fi 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() = d & P1.last() = d by A55,A72,A89,A90,
GLIB_001:def 28;
          hence thesis by A21,GLIB_001:def 24;
        end;
        suppose
A91:      u1 = d & u2 = e;
          im = 0
          proof
            di+im < len pdf +di by A87,XREAL_1:6;
            then di+im < fi+1 by A13,A19,GLIB_001:36;
            then di+im <= fi by NAT_1:13;
            then
A92:        di+im <= len P1 by A13,XXREAL_0:2;
            assume
A93:        im <> 0;
            reconsider im as even Element of NAT by A85;
            di+0 < di+im by A93,XREAL_1:6;
            then P1.first() = d & P1.last() = d by A54,A88,A91,A92,
GLIB_001:def 28;
            hence contradiction by A21,GLIB_001:def 24;
          end;
          hence thesis by A13,A19,A55,A85,A71,A91,GLIB_001:36;
        end;
      end;
      hence contradiction by A3,A44,A5,A79,Th24;
    end;
    suppose
      v1 = v2;
      then pde.first() = v1 & pde.last() = v1 by A57,A58,A59,A61,
GLIB_001:def 28;
      hence contradiction by A42,GLIB_001:def 24;
    end;
  end;
  rpdf is non trivial by A20,GLIB_001:129;
  then C is Cycle-like by A42,A16,A37,A39,A38,A41,A49,Th20;
  hence contradiction;
end;

definition
  let T be _Tree;
  let a, b be Vertex of T;
  func T.pathBetween(a,b) -> Path of T means
  :Def2:
  it is_Walk_from a, b;
  existence
  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 P;
    P is_Walk_from W.first(), W.last() by GLIB_001:def 32;
    then P is_Walk_from a, W.last() by A1;
    hence thesis by A1;
  end;
  uniqueness by Th27;
end;

theorem Th28:
  for T being _Tree, a, b being Vertex of T holds T.pathBetween(a,
  b).first() = a & T.pathBetween(a,b).last() = b
proof
  let T be _Tree, a, b be Vertex of T;
A1: T.pathBetween(a,b) is_Walk_from a, b by Def2;
  hence T.pathBetween(a,b).first() = a;
  thus thesis by A1;
end;

:: more theorems about pathBetween ?

theorem Th29:
  for T being _Tree, 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, a, b be Vertex of T;
  T.pathBetween(a,b).first() = a by Th28;
  hence a in T.pathBetween(a,b).vertices() by GLIB_001:88;
  T.pathBetween(a,b).last() = b by Th28;
  hence thesis by GLIB_001:88;
end;

registration
  let T be _Tree, a be Vertex of T;
  cluster T.pathBetween(a, a) -> closed;
  correctness
  by Def2,GLIB_001:119;
end;

registration
  let T be _Tree, a be Vertex of T;
  cluster T.pathBetween(a, a) -> trivial;
  correctness;
end;

theorem Th30:
  for T being _Tree, a being Vertex of T holds T.pathBetween(a,a)
  .vertices() = {a}
proof
  let T be _Tree, a be Vertex of T;
  set P = T.pathBetween(a,a);
  consider v being Vertex of T such that
A1: P = T.walkOf(v) by GLIB_001:128;
  a = P.first() & T.walkOf(v).first() = v by Th28,GLIB_001:13;
  hence thesis by A1,GLIB_001:90;
end;

theorem Th31:
  for T being _Tree, a, b being Vertex of T holds T.pathBetween(a,
  b).reverse() = T.pathBetween(b,a)
proof
  let T be _Tree, a, b be Vertex of T;
  set P = T.pathBetween(a,b);
  P is_Walk_from a, b by Def2;
  then P.reverse() is_Walk_from b, a by GLIB_001:23;
  hence thesis by Def2;
end;

theorem Th32:
  for T being _Tree, a, b being Vertex of T holds T.pathBetween(a,
  b).vertices() = T.pathBetween(b,a).vertices()
proof
  let T be _Tree, a, b be Vertex of T;
  T.pathBetween(a,b).reverse() = T.pathBetween(b,a) by Th31;
  hence thesis by GLIB_001:92;
end;

theorem Th33:
  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;
  let a, b be Vertex of T;
  let t be _Subtree of T;
  let a9, b9 be Vertex of t such that
A1: a = a9 and
A2: b = b9;
  set tp = t.pathBetween(a9,b9);
  reconsider tp9 = tp as Walk of T by GLIB_001:167;
A3: tp is_Walk_from a9, b9 by Def2;
A4: tp9.last() = tp.last() .= b by A2,A3;
  tp9.first() = tp.first() .= a by A1,A3;
  then tp9 is Path-like & tp9 is_Walk_from a, b by A4,GLIB_001:176;
  hence thesis by Def2;
end;

theorem Th34:
  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, a, b be Vertex of T, t be _Subtree of T;
  assume a in the_Vertices_of t & b in the_Vertices_of t;
  then reconsider a9 = a, b9 = b as Vertex of t;
  set Tp = T.pathBetween(a,b), tp = t.pathBetween(a9,b9);
  Tp.vertices() = tp.vertices() by Th33,GLIB_001:76;
  hence thesis;
end;

theorem Th35:
  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, P be Path of T, a, b be Vertex of T, i, j be odd Nat such
  that
A1: i <= j & j <= len P & P.i = a & P.j = b;
  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 thesis by Def2;
end;

theorem Th36:
  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, a, b, c be Vertex of T;
  set P = T.pathBetween(a,b);
  set ci = P.find(c);
  set pac = T.pathBetween(a,c), pcb = T.pathBetween(c,b);
  hereby
A1: P = P.cut(1, len P) by GLIB_001:39;
A2: 1 <= ci & 1 = 2*0+1 by ABIAN:12;
    assume
A3: c in P.vertices();
    then
A4: ci <= len P by GLIB_001:def 19;
A5: P.ci = c by A3,GLIB_001:def 19;
    P.len P = P.last() .= b by Th28;
    then
A6: pcb = P.cut(ci, len P) by A4,A5,Th35;
    P.1 = P.first() .= a by Th28;
    then pac = P.cut(1,ci) by A4,A2,A5,Th35;
    hence P = T.pathBetween(a,c).append(T.pathBetween(c,b)) by A4,A2,A6,A1,
GLIB_001:38;
  end;
  assume P = pac.append(pcb);
  then
A7: pac.vertices() c= P.vertices() by Th13,Th15;
  c in pac.vertices() by Th29;
  hence thesis by A7;
end;

theorem Th37:
  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, a, b, c be Vertex of T;
  hereby
    assume c in T.pathBetween(a,b).vertices();
    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;
  end;
  assume T.pathBetween(a,c) c= T.pathBetween(a,b);
  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 thesis by A1;
end;

theorem Th38:
  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, P1, P2 be Path of T such that
A1: P1.last() = P2.first() and
A2: P1.vertices() /\ P2.vertices() = {P1.last()};
  per cases;
  suppose
    P1 is trivial;
    hence thesis by A1,Th16;
  end;
  suppose
    P2 is trivial;
    hence thesis by GLIB_001:130;
  end;
  suppose
    P1 is non trivial & P2 is non trivial;
    hence thesis by A1,A2,Th19;
  end;
end;

theorem Th39:
  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, a, b, c be Vertex of T;
  set Pac = T.pathBetween(a,c), Pcb = T.pathBetween(c,b), Pab = T.pathBetween(
  a,b);
A1: Pac.last() = c by Th28
    .= Pcb.first() by Th28;
  thus c in Pab.vertices() implies Pac.vertices() /\ Pcb.vertices() = {c}
  proof
    assume
A2: c in T.pathBetween(a,b).vertices();
    thus Pac.vertices() /\ Pcb.vertices() c= {c}
    proof
      let x be object;
      assume
A3:   x in Pac.vertices() /\ Pcb.vertices();
      then
A4:   x in Pac.vertices() by XBOOLE_0:def 4;
A5:   x in Pcb.vertices() by A3,XBOOLE_0:def 4;
A6:   Pcb.first() = c by Th28;
A7:   Pab = Pac.append(Pcb) by A2,Th36;
A8:   Pab.first() = a & Pab.last() = b by Th28;
A9:   Pac.last() = c by Th28;
      per cases;
      suppose
        Pab is trivial;
        then Pab.first() = Pab.last() by GLIB_001:127;
        then
A10:    Pab.vertices() = {a} by A8,Th30;
        x in Pac.vertices() \/ Pcb.vertices() by A4,XBOOLE_0:def 3;
        then x in Pab.vertices() by A7,A9,A6,GLIB_001:93;
        hence thesis by A2,A10,TARSKI:def 1;
      end;
      suppose
A11:    Pab is non trivial;
        consider n being odd Element of NAT such that
A12:    n <= len Pcb and
A13:    Pcb.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 Pac and
A15:    Pac.m = x by A4,GLIB_001:87;
A16:    m <= len Pac + n1 by A14,NAT_1:12;
        1 <= m by ABIAN:12;
        then m in dom Pac by A14,FINSEQ_3:25;
        then
A17:    Pab.m = x by A7,A15,GLIB_001:32;
        len Pac + (n1+1) <= len Pac + len Pcb by A12,XREAL_1:6;
        then len Pac + n1+1 -1 <= len Pac + len Pcb -1 by XREAL_1:9;
        then
A18:    len Pac + n1+1-1 <= len Pab +1 -1 by A7,A9,A6,GLIB_001:28;
A19:    n1+1 = n;
        then n1 < len Pcb by A12,NAT_1:13;
        then
A20:    Pab.(len Pac + n1) = x by A7,A9,A6,A13,A19,GLIB_001:33;
        per cases by A16,XXREAL_0:1;
        suppose
A21:      m < len Pac + n1;
          then Pab.first() = x by A17,A20,A18,GLIB_001:def 28
            .= Pab.last() by A17,A20,A18,A21,GLIB_001:def 28;
          hence thesis by A11,GLIB_001:def 24;
        end;
        suppose
A22:      m = len Pac + n1;
          then n1 = 0 by A14,NAT_1:16;
          hence thesis by A9,A15,A22,TARSKI:def 1;
        end;
      end;
    end;
    let x be object;
    assume x in {c};
    then
A23: x = c by TARSKI:def 1;
    then x = Pcb.first() by Th28;
    then
A24: x in Pcb.vertices() by GLIB_001:88;
    x = Pac.last() by A23,Th28;
    then x in Pac.vertices() by GLIB_001:88;
    hence thesis by A24,XBOOLE_0:def 4;
  end;
  Pac.first() = a & Pcb.last() = b by Th28;
  then
A25: Pac.append(Pcb) is_Walk_from a, b by A1,GLIB_001:30;
  assume Pac.vertices() /\ Pcb.vertices() = {c};
  then Pac.vertices() /\ Pcb.vertices() = {Pac.last()} by Th28;
  then Pac.append(Pcb) is Path-like by A1,Th38;
  then Pab = Pac.append(Pcb) by A25,Def2;
  hence thesis by Th36;
end;

theorem Th40:
  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 being _Tree;
  let a, b, c, d being Vertex of T;
  let P1, P2 being Path of T such 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);
  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 as odd Element of NAT by A6,Th22;
A8: di <= di+2 by NAT_1:11;
  set Pdb = T.pathBetween(d,b);
A9: Pdb.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 = Pad.append(Pdc) by A2,Th36;
A13: Pad.last() = d by Th28;
A14: Pdc.1 = Pdc.first() .= d by Th28;
A15: Pdc.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 = Pad.append(Pdb) by A1,Th36;
A18: 1 <= di by ABIAN:12;
  then Pad = P1.cut(2*0+1,di) by A5,A6,A16,Th35;
  then
A19: len Pad + ((2*0)+1) = di + 1 by A16,A18,GLIB_001:36;
A20: Pdb.1 = Pdb.first() .= d by Th28;
  thus Pdb.vertices() /\ Pdc.vertices() = {d}
  proof
    hereby
      assume not Pdb.vertices() /\ Pdc.vertices() c= {d};
      then consider e being object such that
A21:  e in Pdb.vertices() /\ Pdc.vertices() and
A22:  not e in {d};
A23:  e in Pdb.vertices() by A21,XBOOLE_0:def 4;
A24:  e in Pdc.vertices() by A21,XBOOLE_0:def 4;
      reconsider e as Vertex of T by A21;
      consider ebi be odd Element of NAT such that
A25:  ebi <= len Pdb and
A26:  e = Pdb.ebi by A23,GLIB_001:87;
      set Pdeb = Pdb.cut(1,ebi);
      1 <= ebi & 2*0+1 is odd Element of NAT by ABIAN:12;
      then
A27:  Pdeb is_Walk_from d, e by A20,A25,A26,GLIB_001:37;
      1 < len Pdeb
      proof
        assume
A28:    1 >= len Pdeb;
        per cases by A28,NAT_1:25;
        suppose
          len Pdeb = 2*0;
          hence contradiction;
        end;
        suppose
A29:      len Pdeb = 1;
A30:      Pdeb.1 = d by A27;
          Pdeb.1 = e by A27,A29;
          hence contradiction by A22,A30,TARSKI:def 1;
        end;
      end;
      then
A31:  (2*0+1)+2 <= len Pdeb by CHORD:4;
      then
A32:  2 < len Pdeb by XXREAL_0:2;
      consider eci be odd Element of NAT such that
A33:  eci <= len Pdc and
A34:  e = Pdc.eci by A24,GLIB_001:87;
      set Pdec = Pdc.cut(1,eci);
      1 <= eci & 2*0+1 is odd Element of NAT by ABIAN:12;
      then
A35:  Pdec is_Walk_from d, e by A14,A33,A34,GLIB_001:37;
      1 < len Pdec
      proof
        assume
A36:    1 >= len Pdec;
        per cases by A36,NAT_1:25;
        suppose
          len Pdec = 2*0;
          hence contradiction;
        end;
        suppose
A37:      len Pdec = 1;
A38:      Pdec.1 = d by A35;
          Pdec.1 = e by A35,A37;
          hence contradiction by A22,A38,TARSKI:def 1;
        end;
      end;
      then
A39:  (2*0+1)+2 <= len Pdec by CHORD:4;
      then
A40:  2 < len Pdec by XXREAL_0:2;
      1+2 in dom Pdeb by A31,FINSEQ_3:25;
      then
A41:  Pdeb.(1+2) = Pdb.(1+2) by A25,GLIB_001:46;
      len Pdeb <= len Pdb by Th10;
      then 2 < len Pdb by A32,XXREAL_0:2;
      then
A42:  P1.(di+2) = Pdb.(1+2) by A9,A13,A17,A19,GLIB_001:33;
      len Pdec <= len Pdc by Th10;
      then 2 < len Pdc by A40,XXREAL_0:2;
      then
A43:  P2.(di+2) = Pdc.(1+2) by A15,A13,A12,A19,GLIB_001:33;
A44:  1+2 in dom Pdec by A39,FINSEQ_3:25;
      Pdeb.(1+2) = Pdec.(1+2) by A27,A35,Th27;
      hence contradiction by A3,A4,A6,A7,A33,A42,A41,A43,A44,Th24,GLIB_001:46;
    end;
    d in Pdb.vertices() & d in Pdc.vertices() by A9,A15,GLIB_001:88;
    then d in Pdb.vertices() /\ Pdc.vertices() by XBOOLE_0:def 4;
    hence thesis by ZFMISC_1:31;
  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, a, b, c be Vertex of T such that
A1: c in T.pathBetween(a,b).vertices();
  set P1 = T.pathBetween(a,b), P2 = T.pathBetween(b,c), P3 = T.pathBetween(c,a
  );
  P1.vertices() = T.pathBetween(b,a).vertices() by Th32;
  then P2.vertices() /\ P3.vertices() = {c} by A1,Th39;
  then P1.vertices() /\ (P2.vertices() /\ P3.vertices())={c} by A1,ZFMISC_1:46;
  hence thesis by XBOOLE_1:16;
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, a, b, c be Vertex of T, P1, P4 be Path of T such 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;
  set P3 = T.pathBetween(c,a);
A5: P3.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 = i as odd Element of NAT by Th22;
  set x = P1.i9;
A7: i <= i+2 by NAT_1:11;
A8: now
    assume b in P3.vertices();
    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;
  end;
  i+2 <= len P4 by A4,A6,Th23;
  then
A9: i <= len P4 by A7,XXREAL_0:2;
A10: i+2 <= len P1 by A3,A6,Th23;
  then reconsider x as Vertex of T by A7,GLIB_001:7,XXREAL_0:2;
  set P1b = P1.cut(i9,len P1);
  set P1br = P1b.reverse();
  set j = len P1br;
  set P4c = P4.cut(i9,len P4);
  set Pbc = P1br.append(P4c);
A11: i <= len P1 by A7,A10,XXREAL_0:2;
  then P1b.first() = P1.i9 by GLIB_001:37;
  then
A12: P1br.last() = x by GLIB_001:22;
  1 <= j by CHORD:2;
  then j in dom P1br by FINSEQ_3:25;
  then
A13: Pbc.j = 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 P1b.last() = b by A11,GLIB_001:37;
  then
A16: P1br.first() = b by GLIB_001:22;
A17: x = P4.i9 by Th7;
  then x <> b by A8,A5,A9,GLIB_001:87;
  then
A18: P1br is open by A12,A16;
  P4.len P4 = P4.last() .= c by A2,Th28;
  then P4c is_Walk_from x, c by A9,A17,GLIB_001:37;
  then
A19: P4c = T.pathBetween(x,c) by Def2;
  then
A20: P4c.first() = x by Th28;
  then
A21: j <= len Pbc by A12,GLIB_001:29;
  P1b is_Walk_from x, b by A11,A15,GLIB_001:37;
  then P1b = T.pathBetween(x,b) by Def2;
  then
  P1br.vertices() = P1b.vertices() & P1b.vertices() /\ P4c.vertices() = {
  x} by A1,A2,A3,A4,A19,Th40,GLIB_001:92;
  then
A22: P1br.vertices() /\ P4c.vertices() c= {P1br.first(), P1br.last()} by A12,
ZFMISC_1:7;
A23: P4c.vertices() c= P4.vertices() by A9,GLIB_001:94;
A24: P1br.edges() misses P4c.edges()
  proof
    assume not thesis;
    then P1br.edges() /\ P4c.edges() <> {};
    then consider e being object such that
A25: e in P1br.edges() /\ P4c.edges() by XBOOLE_0:def 1;
    e in P1br.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 P1br and
A27: v1br = P1br.n and
    e = P1br.(n+1) and
A28: v2br = P1br.(n+2) and
A29: e Joins v1br, v2br, T by GLIB_001:103;
    n <= n+2 by NAT_1:11;
    then n <= len P1br by A26,XXREAL_0:2;
    then
A30: v1br in P1br.vertices() by A27,GLIB_001:87;
    v2br in P1br.vertices() by A26,A28,GLIB_001:87;
    then
A31: {v1br, v2br} c= P1br.vertices() by A30,ZFMISC_1:32;
    e in P4c.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 P4c and
A33: v1c = P4c.m and
    e = P4c.(m+1) and
A34: v2c = P4c.(m+2) and
A35: e Joins v1c, v2c, T by GLIB_001:103;
    m <= m+2 by NAT_1:11;
    then m <= len P4c by A32,XXREAL_0:2;
    then
A36: v1c in P4c.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 P4c.vertices() by A32,A34,GLIB_001:87;
    then {v1c, v2c} c= P4c.vertices() by A36,ZFMISC_1:32;
    then
A39: {v1c, v2c} c= P1br.vertices() /\ P4c.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;
  end;
A41: P4c.last() = c by A19,Th28;
  then
A42: Pbc is_Walk_from b,c by A12,A20,A16,GLIB_001:30;
  now
    assume c in P1.vertices();
    then P1 = T.pathBetween(a,c).append(T.pathBetween(c,b)) by A1,Th36;
    hence contradiction by A2,A4,Th15;
  end;
  then x <> c by A11,GLIB_001:87;
  then
A43: P4c is open by A20,A41;
  not P1br.first() in P4c.vertices() by A8,A5,A23,A16;
  then Pbc is Path of T by A12,A20,A18,A43,A22,A24,Th18;
  then Pbc = P2 by A42,Def2;
  then
A44: x in P2.vertices() by A21,A13,GLIB_001:87;
A45: x in P4.vertices() by A9,A17,GLIB_001:87;
A46: P1.vertices() /\ P2.vertices() /\ P3.vertices() c= {x}
  proof
    set Pcx = T.pathBetween(c,x), Pxa = T.pathBetween(x,a);
    set Pbx = T.pathBetween(b,x), Pxc = T.pathBetween(x,c);
    set Pax = T.pathBetween(a,x), Pxb = T.pathBetween(x,b);
    let z be object;
A47: Pbx.vertices() = Pxb.vertices() by Th32;
A48: Pcx.vertices() = Pxc.vertices() by Th32;
A49: Pcx.last() = x by Th28
      .= Pxa.first() by Th28;
    P3 = Pcx.append(Pxa) by A5,A45,Th36;
    then
A50: P3.vertices() = Pcx.vertices() \/ Pxa.vertices() by A49,GLIB_001:93;
A51: Pbx.last() = x by Th28
      .= Pxc.first() by Th28;
    P2 = Pbx.append(Pxc) by A44,Th36;
    then
A52: P2.vertices() = Pbx.vertices() \/ Pxc.vertices() by A51,GLIB_001:93;
A53: Pax.last() = x by Th28
      .= Pxb.first() by Th28;
    P1 = Pax.append(Pxb) by A1,A14,Th36;
    then
A54: P1.vertices() = Pax.vertices() \/ Pxb.vertices() by A53,GLIB_001:93;
    assume
A55: z in P1.vertices() /\ P2.vertices() /\ P3.vertices();
    then
A56: z in P1.vertices() /\ P2.vertices() by XBOOLE_0:def 4;
    then z in P1.vertices() by XBOOLE_0:def 4;
    then
A57: z in Pax.vertices() or z in Pxb.vertices() by A54,XBOOLE_0:def 3;
    z in P3.vertices() by A55,XBOOLE_0:def 4;
    then
A58: z in Pcx.vertices() or z in Pxa.vertices() by A50,XBOOLE_0:def 3;
    z in P2.vertices() by A56,XBOOLE_0:def 4;
    then
A59: z in Pbx.vertices() or z in Pxc.vertices() by A52,XBOOLE_0:def 3;
    per cases by A57,A59,A58,Th32;
    suppose
      z in Pax.vertices() & z in Pbx.vertices();
      then z in Pax.vertices() /\ Pxb.vertices() by A47,XBOOLE_0:def 4;
      hence thesis by A1,A14,Th39;
    end;
    suppose
      z in Pax.vertices() & z in Pcx.vertices();
      then z in Pax.vertices() /\ Pxc.vertices() by A48,XBOOLE_0:def 4;
      hence thesis by A2,A45,Th39;
    end;
    suppose
      z in Pbx.vertices() & z in Pcx.vertices();
      then z in Pbx.vertices() /\ Pxc.vertices() by A48,XBOOLE_0:def 4;
      hence thesis by A44,Th39;
    end;
  end;
  x in P1.vertices() /\ P2.vertices() by A14,A44,XBOOLE_0:def 4;
  then x in P1.vertices() /\ P2.vertices() /\ P3.vertices() by A5,A45,
XBOOLE_0:def 4;
  then {x} c= P1.vertices() /\ P2.vertices() /\ P3.vertices() by ZFMISC_1:31;
  hence thesis by A46;
end;

definition
  let T be _Tree, a, b, c be Vertex of T;
  func MiddleVertex(a, b, c) -> Vertex of T means
  :Def3:
  T.pathBetween(a,b)
.vertices() /\ T.pathBetween(b,c).vertices() /\ T.pathBetween(c,a).vertices() =
  { it };
  existence
  proof
    defpred P[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);
    per cases;
    suppose
A1:   c in P1.vertices() or a in P2.vertices() or b in P3.vertices();
      per cases by A1;
      suppose
        c in P1.vertices();
        then P[a, b, c, c] by Lm1;
        hence thesis;
      end;
      suppose
        a in P2.vertices();
        then P[b, c, a, a] by Lm1;
        hence thesis by XBOOLE_1:16;
      end;
      suppose
        b in P3.vertices();
        then P[c, a, b, b] by Lm1;
        hence thesis by XBOOLE_1:16;
      end;
    end;
    suppose
A2:   not c in P1.vertices() & not a in P2.vertices() & not b in P3
      .vertices();
      set P4 = T.pathBetween(a,c);
      set i = len maxPrefix(P1,P4);
      P1.last() = b by Th28;
      then
A3:   b in P1.vertices() by GLIB_001:88;
      P4.last() = c by Th28;
      then c in P4.vertices() by GLIB_001:88;
      then not P4.vertices() c= P1.vertices() by A2;
      then
A4:   not P4 c= P1 by Th13;
      P1.first() = a by Th28;
      then
A5:   P1.first() = P4.first() by Th28;
      then reconsider i9 = i as odd Element of NAT by Th22;
      set x = P1.i9;
      P3.vertices() = P4.vertices() by Th32;
      then
A6:   not P1.vertices() c= P4.vertices() by A2,A3;
      then i <= i+2 & i+2 <= len P1 by A5,Th13,Th23,NAT_1:11;
      then reconsider x as Vertex of T by GLIB_001:7,XXREAL_0:2;
      take x;
      not P1 c= P4 by A6,Th13;
      hence thesis by A4,Lm2;
    end;
  end;
  uniqueness by ZFMISC_1:3;
end;

theorem Th41: :: PMV(a,b,c) = PMV(a,c,b)
  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;
  let a, b, c be Vertex of T;
  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() = { PMV1 } & T.pathBetween(a,c).vertices() /\ T
  .pathBetween(c,b).vertices() /\ T.pathBetween(b,a).vertices() = { PMV2 } by
Def3;
  then {PMV1} = {PMV2} by A1,A2,XBOOLE_1:16;
  hence thesis by ZFMISC_1:3;
end;

theorem Th42: :: PMV(a,b,c) = PMV(b,a,c)
  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;
  let a, b, c be Vertex of T;
  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() = { PMV1 } & T.pathBetween(b,a).vertices() /\ T
  .pathBetween(a,c).vertices() /\ T.pathBetween(c,b).vertices() = { PMV2 } by
Def3;
  then {PMV1} = {PMV2} by A1,A2,XBOOLE_1:16;
  hence thesis by ZFMISC_1:3;
end;

theorem ::PMV102: :: PMV(a,b,c) = PMV(b,c,a)
  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;
  let a, b, c be Vertex of T;
  thus MiddleVertex(a,b,c) = MiddleVertex(b,a,c) by Th42
    .= MiddleVertex(b,c,a) by Th41;
end;

theorem Th44: :: PMV(a,b,c) = PMV(c,a,b)
  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;
  let a, b, c be Vertex of T;
  thus MiddleVertex(a,b,c) = MiddleVertex(a,c,b) by Th41
    .= MiddleVertex(c,a,b) by Th42;
end;

theorem :: PMV104: :: PMV(a,b,c) = PMV(c,b,a)
  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;
  let a, b, c be Vertex of T;
  thus MiddleVertex(a,b,c) = MiddleVertex(c,a,b) by Th44
    .= MiddleVertex(c,b,a) by Th41;
end;

theorem Th46:
  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;
  let a, b, c be Vertex of T;
  assume c in T.pathBetween(a,b).vertices();
  then T.pathBetween(a,b).vertices() /\ T.pathBetween(b,c).vertices() /\ T
  .pathBetween(c,a).vertices() = {c} by Lm1;
  hence thesis by Def3;
end;

theorem :: PMV200: :: PMV(a,a,a) = a;
  for T being _Tree for a being Vertex of T holds MiddleVertex(a,a,a) = a
proof
  let T be _Tree;
  let a be Vertex of T;
  a in {a} by TARSKI:def 1;
  then a in T.pathBetween(a,a).vertices() by Th30;
  hence thesis by Th46;
end;

theorem Th48: :: PMV(a,a,b) = a;
  for T being _Tree for a, b being Vertex of T holds MiddleVertex( a,a,b) = a
proof
  let T be _Tree;
  let a,b be Vertex of T;
  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 thesis by A1,Th46;
end;

theorem Th49: :: PMV(a,b,a) = a;
  for T being _Tree for a, b being Vertex of T holds MiddleVertex( a,b,a) = a
proof
  let T be _Tree;
  let a,b be Vertex of T;
  MiddleVertex(a,a,b) = MiddleVertex(a,b,a) by Th41;
  hence thesis by Th48;
end;

theorem :: PMV203: :: PMV(a,b,b) = b;
  for T being _Tree for a, b being Vertex of T holds MiddleVertex(a,b,b) = b
proof
  let T be _Tree;
  let a,b be Vertex of T;
  MiddleVertex(a,b,b) = MiddleVertex(b,a,b) by Th42;
  hence thesis by Th49;
end;

theorem Th51:
  for T being _Tree for P1, P2 be 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, P1, P2 be Path of T, a, b, c be Vertex of T such that
A1: P1 = T.pathBetween(a,b) & P2 = T.pathBetween(a,c) and
A2: ( not b in P2.vertices())& not c in P1.vertices();
  ( 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 thesis by A3,ZFMISC_1:3;
end;

theorem :: PMV302:
  for T being _Tree for P1, P2, P3, P4 be 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, P1, P2, P3, P4 be Path of T, a, b, c be Vertex of T such
  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();
  now
    assume P4 c= P3;
    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;
  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 thesis by A9,Th42;
end;

theorem Th53:
  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;
  let a, b, c be Vertex of T;
  let S be non empty set;
  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);
  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 = Pab.vertices();
  set VPac = Pac.vertices();
  set VPbc = Pbc.vertices();
  set VPca = Pca.vertices();
  VPab /\ VPbc /\ VPca = {m} by Def3;
  then
A2: m in VPab /\ VPbc /\ VPca by TARSKI:def 1;
  then
A3: m in VPab /\ VPbc by XBOOLE_0:def 4;
  then
A4: m in VPbc by XBOOLE_0:def 4;
  VPca = VPac by Th32;
  then
A5: m in VPac by A2,XBOOLE_0:def 4;
A6: m in VPab by A3,XBOOLE_0:def 4;
  now
    let s be set;
    assume
A7: s in S;
    then
A8: ex t being _Subtree of T st s = the_Vertices_of t by A1;
    per cases by A1,A7;
    suppose
      a in s & b in s;
      then VPab c= s by A8,Th34;
      hence m in s by A6;
    end;
    suppose
      a in s & c in s;
      then VPac c= s by A8,Th34;
      hence m in s by A5;
    end;
    suppose
      b in s & c in s;
      then VPbc c= s by A8,Th34;
      hence m in s by A4;
    end;
  end;
  hence thesis by SETFAM_1:def 1;
end;

begin :: The Helly property

definition
  let F be set;
  attr F is with_Helly_property means
  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;

:: At some point one would like to define allSubtrees of a Tree
:: The claim below does not hold when T is infinite and we consider
:: infinite families of subtrees.  Example: half-line tree with
:: subtrees T_i = {j >= i}.
:: main Prop4p7:

theorem
  for T being _Tree, X being finite set st for x being set st x in X ex
  t being _Subtree of T st x = the_Vertices_of t holds X is with_Helly_property
proof
  let T be _Tree, X be finite set such that
A1: for x being set st x in X ex t being _Subtree of T st x =
  the_Vertices_of t;
  defpred P[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 P[n] holds P[k]
  proof
    let k be Nat such that
A3: for n being Nat st n < k holds P[n];
    let H be non empty finite set such 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;
    per cases by NAT_1:25;
    suppose
      k = 0;
      hence thesis by A4;
    end;
    suppose
      k = 1;
      then consider x being Element of H such that
A7:   H = { x } by A4,PRE_CIRC:25;
      ex t being _Subtree of T st x = the_Vertices_of t by A1,A5;
      hence thesis by A7,SETFAM_1:10;
    end;
    suppose
A8:   k > 1;
      set cH = the Element of H;
      set A = H \ {cH};
A9:   card A = card H - card {cH} by EULER_1:4
        .= k - 1 by A4,CARD_1:30;
      k-1 > 1-1 by A8,XREAL_1:9;
      then reconsider A as non empty finite set by A9;
A10:  A c= X by A5;
      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 = the Element of A;
      set B = H \ {cA};
A11:  cA in A;
      then
A12:  card B = card H - card {cA} by EULER_1:4
        .= k - 1 by A4,CARD_1:30;
      set C = {cH, cA};
A13:  meet C = cH /\ cA by SETFAM_1:11;
      cH meets cA by A6,A11;
      then reconsider mC = meet C as non empty set by A13;
      k-1 > 1-1 by A8,XREAL_1:9;
      then reconsider B as non empty finite set by A12;
A14:  B c= X by A5;
      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 = the Element of  mA, b = the Element of  mB,
          c = the Element of  mC;
      c in mC & mC c= union C by SETFAM_1:2;
      then consider cc being set such that
A15:  c in cc and
A16:  cc in C by TARSKI:def 4;
      cH in H;
      then C 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;
      a in mA & mA c= union A by SETFAM_1:2;
      then consider aa being set such that
A18:  a in aa and
A19:  aa in A by TARSKI:def 4;
      b in mB & mB c= union B by SETFAM_1:2;
      then consider bb being set such that
A20:  b 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, b, c as Vertex of T by A18,A20,A22,A15,A17;
A23:  cA <> cH by ZFMISC_1:56;
      now
        let s be set;
        assume
A24:    s in H;
        hence ex t being _Subtree of T st s = the_Vertices_of t by A1,A5;
        thus a in s & b in s or a in s & c in s or b in s & c in s
        proof
          per cases;
          suppose
            s = cH;
            then s in C & s in B by A23,TARSKI:def 2,ZFMISC_1:56;
            hence thesis by SETFAM_1:def 1;
          end;
          suppose
A25:        s = cA;
            then s in C by TARSKI:def 2;
            hence thesis by A25,SETFAM_1:def 1;
          end;
          suppose
            s <> cH & s <> cA;
            then s in A & s in B by A24,ZFMISC_1:56;
            hence thesis by SETFAM_1:def 1;
          end;
        end;
      end;
      hence thesis by Th53;
    end;
  end;
A26: for n being Nat holds P[n] from NAT_1:sch 4 (A2);
  let H be non empty set such that
A27: H c= X and
A28: for x, y being set st x in H & y in H holds x meets y;
  reconsider H9 = H as finite set by A27;
  card H9 = card H9;
  hence thesis by A26,A27,A28;
end;