helly.miz



    begin

    theorem :: HELLY:1

    for p be 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 be 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;

      :: HELLY:def1

      func maxPrefix (p,q) -> FinSequence means

      : Def1: it is_a_prefix_of p & it is_a_prefix_of q & for r be 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 be FinSequence st r c= p & r c= q & ( len r) = $1;

        set S = { F(k) where k be Nat : k <= ( len p) & P[k] };

        

         A1: for x be object st x in S holds x is natural

        proof

          let x be object;

          assume x in S;

          then ex n be 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 be Nat such that

         A3: K = maxk and K <= ( len p) and

         A4: P[K];

        consider R be 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 :: HELLY:2

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

    theorem :: HELLY:3

    

     Th3: for p,q be 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 :: HELLY:4

    

     Th4: for p be 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 :: HELLY:5

    

     Th5: for p,q be 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 :: HELLY:6

    

     Th6: for p,q be FinSequence holds for j be 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 :: HELLY:7

    

     Th7: for p,q be FinSequence holds for j be 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 :: HELLY:8

    

     Th8: for p,q be 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 :: HELLY:9

    

     Th9: for p,q be 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

    theorem :: HELLY:10

    

     Th10: for G be _Graph, W be Walk of G, m,n be 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 :: HELLY:11

    for G be _Graph, W be Walk of G, m,n be 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 :: HELLY:12

    

     Th12: for G be _Graph, W be Walk of G holds for m,n,i be odd Nat st m <= n & n <= ( len W) & i <= ( len (W .cut (m,n))) holds ex j be 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 be 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 :: HELLY:13

    

     Th13: for G be _Graph holds for W1,W2 be 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 be 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 :: HELLY:14

    for G be _Graph holds for W1,W2 be 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 be 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 :: HELLY:15

    

     Th15: for G be _Graph holds for W1,W2 be 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 be 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 :: HELLY:16

    

     Th16: for G be _Graph, W1,W2 be 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 :: HELLY:17

    

     Th17: for G be _Graph holds for W1,W2 be 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 be Element of NAT st k < ( len W2) & n = (( len W1) + k);

          then

          consider k be 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 be Element of NAT st l < ( len W2) & m = (( len W1) + l);

            then

            consider l be 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 :: HELLY:18

    

     Th18: for G be _Graph holds for P1,P2 be 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 be Element of NAT st k < ( len P2) & n = (( len P1) + k);

        then

        consider k be 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 be Element of NAT st k < ( len P2) & m = (( len P1) + k);

          then

          consider l be 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 :: HELLY:19

    

     Th19: for G be _Graph holds for P1,P2 be 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 be 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 be Vertex of G, m be 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 be Vertex of G, n be 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 :: HELLY:20

    

     Th20: for G be _Graph holds for P1,P2 be 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 :: HELLY:21

    for G be simple _Graph holds for W1,W2 be Walk of G holds for k be odd Nat st k <= ( len W1) & k <= ( len W2) & for j be odd Nat st j <= k holds (W1 . j) = (W2 . j) holds for j be 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 be 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 :: HELLY:22

    

     Th22: for G be _Graph holds for W1,W2 be 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 :: HELLY:23

    

     Th23: for G be _Graph holds for W1,W2 be 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 :: HELLY:24

    

     Th24: for G be non-multi _Graph holds for W1,W2 be 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

    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 be odd Element of NAT st k < $1 & (W . k) = (W . $1);

        assume not W is Path-like;

        then ex m,n be 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 be Nat st P[p];

        consider p be Nat such that

         A3: P[p] and

         A4: for r be 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 be 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 be 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 be 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 be 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 :: HELLY:25

    

     Th25: for T be _Tree holds for P be 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 :: HELLY:26

    

     Th26: for T be _Tree holds for P be Path of T holds for i,j be 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 :: HELLY:27

    

     Th27: for T be _Tree holds for a,b be Vertex of T holds for P1,P2 be 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 be 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 be Nat such that

       A11: P[ei] and

       A12: for n be 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 be 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 be odd Element of NAT such that

         A26: gii <= ( len pde) and

         A27: (pde . gii) = g by GLIB_001: 87;

        consider gi be 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 be 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 be Vertex of T, m be 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 be Vertex of T, n be 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 be 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 be 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;

      :: HELLY:def2

      func T .pathBetween (a,b) -> Path of T means

      : Def2: it is_Walk_from (a,b);

      existence

      proof

        consider W be 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 :: HELLY:28

    

     Th28: for T be _Tree, a,b be 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;

    theorem :: HELLY:29

    

     Th29: for T be _Tree, a,b be 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 :: HELLY:30

    

     Th30: for T be _Tree, a be 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 be 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 :: HELLY:31

    

     Th31: for T be _Tree, a,b be 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 :: HELLY:32

    

     Th32: for T be _Tree, a,b be 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 :: HELLY:33

    

     Th33: for T be _Tree holds for a,b be Vertex of T holds for t be _Subtree of T holds for a9,b9 be 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 :: HELLY:34

    

     Th34: for T be _Tree holds for a,b be Vertex of T holds for t be _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 :: HELLY:35

    

     Th35: for T be _Tree holds for P be Path of T holds for a,b be Vertex of T holds for i,j be 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 :: HELLY:36

    

     Th36: for T be _Tree holds for a,b,c be 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 :: HELLY:37

    

     Th37: for T be _Tree holds for a,b,c be 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 :: HELLY:38

    

     Th38: for T be _Tree holds for P1,P2 be 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 :: HELLY:39

    

     Th39: for T be _Tree holds for a,b,c be 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 be 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 be 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 :: HELLY:40

    

     Th40: for T be _Tree holds for a,b,c,d be Vertex of T holds for P1,P2 be 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;

      let a,b,c,d be Vertex of T;

      let P1,P2 be 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 be 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 be _Tree holds for a,b,c be 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 be _Tree holds for a,b,c be Vertex of T holds for P1,P4 be 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 be 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 be Vertex of T, n be 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 be Vertex of T, m be 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;

      :: HELLY:def3

      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 :: HELLY:41

    

     Th41: for T be _Tree holds for a,b,c be 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 :: HELLY:42

    

     Th42: for T be _Tree holds for a,b,c be 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 :: HELLY:43

    for T be _Tree holds for a,b,c be 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 :: HELLY:44

    

     Th44: for T be _Tree holds for a,b,c be 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 :: HELLY:45

    for T be _Tree holds for a,b,c be 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 :: HELLY:46

    

     Th46: for T be _Tree holds for a,b,c be 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 :: HELLY:47

    for T be _Tree holds for a be 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 :: HELLY:48

    

     Th48: for T be _Tree holds for a,b be 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 :: HELLY:49

    

     Th49: for T be _Tree holds for a,b be 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 :: HELLY:50

    for T be _Tree holds for a,b be 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 :: HELLY:51

    

     Th51: for T be _Tree holds for P1,P2 be Path of T holds for a,b,c be 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 :: HELLY:52

    for T be _Tree holds for P1,P2,P3,P4 be Path of T holds for a,b,c be 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 :: HELLY:53

    

     Th53: for T be _Tree holds for a,b,c be Vertex of T holds for S be non empty set st for s be set st s in S holds (ex t be _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 be set st s in S holds (ex t be _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 be _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

    definition

      let F be set;

      :: HELLY:def4

      attr F is with_Helly_property means for H be non empty set st H c= F & for x,y be set st x in H & y in H holds x meets y holds ( meet H) <> {} ;

    end

    theorem :: HELLY:54

    for T be _Tree, X be finite set st for x be set st x in X holds ex t be _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 be set st x in X holds ex t be _Subtree of T st x = ( the_Vertices_of t);

      defpred P[ Nat] means for H be non empty finite set st ( card H) = $1 & H c= X & for x,y be set st x in H & y in H holds x meets y holds ( meet H) <> {} ;

      

       A2: for k be Nat st for n be Nat st n < k holds P[n] holds P[k]

      proof

        let k be Nat such that

         A3: for n be 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 be 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 be Element of H such that

           A7: H = {x} by A4, PRE_CIRC: 25;

          ex t be _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 be 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 be 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 be 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 be _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 be 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 be set such that

           A20: b in bb and

           A21: bb in B by TARSKI:def 4;

          

           A22: ex bbt be _Subtree of T st bb = ( the_Vertices_of bbt) by A1, A14, A21;

          ex aat be _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 be _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 be 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 be 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;