glib_002.miz



    begin

    definition

      let G be _Graph;

      :: GLIB_002:def1

      attr G is connected means

      : Def1: for u,v be Vertex of G holds ex W be Walk of G st W is_Walk_from (u,v);

    end

    definition

      let G be _Graph;

      :: GLIB_002:def2

      attr G is acyclic means

      : Def2: not ex W be Walk of G st W is Cycle-like;

    end

    definition

      let G be _Graph;

      :: GLIB_002:def3

      attr G is Tree-like means G is acyclic & G is connected;

    end

    registration

      cluster _trivial -> connected for _Graph;

      coherence

      proof

        let G be _Graph;

        assume G is _trivial;

        then

        consider x be Vertex of G such that

         A1: ( the_Vertices_of G) = {x} by GLIB_000: 22;

        now

          set W = (G .walkOf x);

          let u,v be Vertex of G;

          u = x & v = x by A1, TARSKI:def 1;

          then W is_Walk_from (u,v) by GLIB_001: 13;

          hence ex W be Walk of G st W is_Walk_from (u,v);

        end;

        hence thesis;

      end;

    end

    registration

      cluster _trivial loopless -> Tree-like for _Graph;

      coherence

      proof

        let G be _Graph;

        assume that

         A1: G is _trivial and

         A2: G is loopless;

        now

          given W be Walk of G such that

           A3: W is Cycle-like;

          (W .edges() ) <> {} by A3, GLIB_001: 136;

          then ex e be object st e in (W .edges() ) by XBOOLE_0:def 1;

          hence contradiction by A1, A2, GLIB_000: 23;

        end;

        then

         A4: G is acyclic;

        reconsider G9 = G as _trivial _Graph by A1;

        G9 is connected;

        hence thesis by A4;

      end;

    end

    registration

      cluster acyclic -> simple for _Graph;

      coherence

      proof

        let G be _Graph;

        assume

         A1: not ex W be Walk of G st W is Cycle-like;

        now

          given e be object such that

           A2: e in ( the_Edges_of G) and

           A3: (( the_Source_of G) . e) = (( the_Target_of G) . e);

          set v1 = (( the_Source_of G) . e);

          reconsider v1 as Vertex of G by A2, FUNCT_2: 5;

          set W = (G .walkOf (v1,e,v1));

          e Joins (v1,v1,G) by A2, A3, GLIB_000:def 13;

          then ( len W) = 3 by GLIB_001: 14;

          then W is non trivial by GLIB_001: 125;

          then W is Cycle-like by GLIB_001:def 31;

          hence contradiction by A1;

        end;

        then

         A4: G is loopless by GLIB_000:def 18;

        now

          let e1,e2,v1,v2 be object;

          assume that

           A5: e1 Joins (v1,v2,G) and

           A6: e2 Joins (v1,v2,G);

          

           A7: e2 Joins (v2,v1,G) by A6, GLIB_000: 14;

          

           A8: v1 <> v2 by A4, A5, GLIB_000: 18;

          now

            set W1 = (G .walkOf (v1,e1,v2)), W = (W1 .addEdge e2);

            assume

             A9: e1 <> e2;

            reconsider W1 as Path of G;

            

             A10: (W1 .last() ) = v2 by A5, GLIB_001: 15;

            then

             A11: (W .last() ) = v1 by A7, GLIB_001: 63;

            

             A12: ( len W1) = 3 by A5, GLIB_001: 14;

             A13:

            now

              let n be odd Element of NAT ;

              assume that

               A14: 1 < n and

               A15: n <= ( len W1);

              (1 + 1) <= n by A14, NAT_1: 13;

              then (2 * 1) < n by XXREAL_0: 1;

              then ((2 * 1) + 1) <= n by NAT_1: 13;

              then

               A16: n = 3 by A12, A15, XXREAL_0: 1;

              W1 = <*v1, e1, v2*> by A5, GLIB_001:def 5;

              hence (W1 . n) <> v1 by A8, A16, FINSEQ_1: 45;

            end;

            (W1 .first() ) = v1 & (W1 .last() ) = v2 by A5, GLIB_001: 15;

            then

             A17: W1 is open by A8, GLIB_001:def 24;

            (W1 .first() ) = v1 by A5, GLIB_001: 15;

            then (W .first() ) = v1 by A7, A10, GLIB_001: 63;

            then

             A18: W is closed by A11, GLIB_001:def 24;

            

             A19: e2 Joins ((W1 .last() ),v1,G) by A5, A7, GLIB_001: 15;

            then

             A20: W is non trivial by GLIB_001: 132;

            (W1 .edges() ) = {e1} by A5, GLIB_001: 108;

            then not e2 in (W1 .edges() ) by A9, TARSKI:def 1;

            hence W is Path-like by A19, A17, A13, GLIB_001: 150;

            then W is Cycle-like by A18, A20, GLIB_001:def 31;

            hence contradiction by A1;

          end;

          hence e1 = e2;

        end;

        then G is non-multi by GLIB_000:def 20;

        hence thesis by A4;

      end;

    end

    registration

      cluster Tree-like -> acyclic connected for _Graph;

      coherence ;

    end

    registration

      cluster acyclic connected -> Tree-like for _Graph;

      coherence ;

    end

    registration

      let G be _Graph, v be Vertex of G;

      cluster -> Tree-like for inducedSubgraph of G, {v}, {} ;

      coherence ;

    end

    definition

      let G be _Graph, v be set;

      :: GLIB_002:def4

      pred G is_DTree_rooted_at v means G is Tree-like & for x be Vertex of G holds ex W be DWalk of G st W is_Walk_from (v,x);

    end

    registration

      cluster _trivial _finite Tree-like for _Graph;

      existence

      proof

        set V = {1}, E = {} ;

        reconsider S = {} as Function of E, V by RELSET_1: 12;

        set G = ( createGraph (V,E,S,S));

        take G;

        thus thesis;

      end;

      cluster non _trivial _finite Tree-like for _Graph;

      existence

      proof

        set V = { 0 , 1}, E = { 0 }, S = ( 0 .--> 0 ), T = ( 0 .--> 1);

        

         A1: ( dom T) = E;

         A2:

        now

          let x be object;

          assume x in E;

          then x = 0 by TARSKI:def 1;

          then (T . x) = 1 by FUNCOP_1: 72;

          hence (T . x) in V by TARSKI:def 2;

        end;

         A3:

        now

          let x be object;

          assume x in E;

          (S . x) = 0 ;

          hence (S . x) in V by TARSKI:def 2;

        end;

        reconsider T as Function of E, V by A1, A2, FUNCT_2: 3;

        ( dom S) = E;

        then

        reconsider S as Function of E, V by A3, FUNCT_2: 3;

        set G = ( createGraph (V,E,S,T));

        

         A4: ( the_Edges_of G) = E by GLIB_000: 6;

        ( the_Target_of G) = T by GLIB_000: 6;

        then

         A5: (( the_Target_of G) . 0 ) = 1 by FUNCOP_1: 72;

        ( the_Source_of G) = S by GLIB_000: 6;

        then

         A6: (( the_Source_of G) . 0 ) = 0 ;

        now

          given W be Walk of G such that

           A7: W is Cycle-like;

          now

            per cases ;

              suppose

               A8: ( len W) = 3;

              set e = (W . (1 + 1)), v1 = (W . 1), v2 = (W . (1 + 2));

              

               A9: (W . (1 + 1)) Joins ((W . 1),(W . (1 + 2)),G) by A8, GLIB_001:def 3, JORDAN12: 2;

              v1 = v2 by A7, A8, GLIB_001: 118;

              then

               A10: (( the_Source_of G) . e) = v1 & (( the_Target_of G) . e) = v1 or (( the_Source_of G) . e) = v1 & (( the_Target_of G) . e) = v1 by A9, GLIB_000:def 13;

              e in ( the_Edges_of G) by A9, GLIB_000:def 13;

              then v1 = 0 & v1 = 1 or v1 = 1 & v1 = 0 by A4, A6, A5, A10, TARSKI:def 1;

              hence contradiction;

            end;

              suppose

               A11: ( len W) <> 3;

              

               A12: 3 <= ( len W) by A7, GLIB_001: 125;

              then (3 - 1) <= (( len W) - 0 ) by XREAL_1: 13;

              then (2 * 1) in ( dom W) by FINSEQ_3: 25;

              then (W . (2 * 1)) in { 0 } by A4, GLIB_001: 8;

              then

               A13: (W . (2 * 1)) = 0 by TARSKI:def 1;

              3 < ( len W) by A11, A12, XXREAL_0: 1;

              then

               A14: (3 + 1) <= ( len W) by NAT_1: 13;

              then (2 * 2) in ( dom W) by FINSEQ_3: 25;

              then (W . (2 * 2)) in { 0 } by A4, GLIB_001: 8;

              then (W . (2 * 2)) = 0 by TARSKI:def 1;

              hence contradiction by A7, A14, A13, GLIB_001: 138;

            end;

          end;

          hence contradiction;

        end;

        then

         A15: G is acyclic;

        set W1 = (G .walkOf ( 0 , 0 ,1)), W2 = (W1 .reverse() );

        take G;

        

         A16: ( the_Vertices_of G) = V by GLIB_000: 6;

        then

        reconsider a0 = 0 , a1 = 1 as Vertex of G by TARSKI:def 2;

        now

          assume ( card ( the_Vertices_of G)) = 1;

          then ex x be object st ( the_Vertices_of G) = {x} by CARD_2: 42;

          hence contradiction by A16, ZFMISC_1: 5;

        end;

        hence G is non _trivial & G is _finite by GLIB_000:def 19;

         0 in ( the_Edges_of G) by A4, TARSKI:def 1;

        then 0 Joins ( 0 ,1,G) by A6, A5, GLIB_000:def 13;

        then

         A17: W1 is_Walk_from ( 0 ,1) by GLIB_001: 15;

        then

         A18: W2 is_Walk_from (1, 0 ) by GLIB_001: 23;

        now

          let u,v be Vertex of G;

          now

            per cases by A16, TARSKI:def 2;

              suppose u = 0 & v = 0 ;

              then (G .walkOf a0) is_Walk_from (u,v) by GLIB_001: 13;

              hence ex W be Walk of G st W is_Walk_from (u,v);

            end;

              suppose u = 0 & v = 1;

              hence ex W be Walk of G st W is_Walk_from (u,v) by A17;

            end;

              suppose u = 1 & v = 0 ;

              hence ex W be Walk of G st W is_Walk_from (u,v) by A18;

            end;

              suppose u = 1 & v = 1;

              then (G .walkOf a1) is_Walk_from (u,v) by GLIB_001: 13;

              hence ex W be Walk of G st W is_Walk_from (u,v);

            end;

          end;

          hence ex W be Walk of G st W is_Walk_from (u,v);

        end;

        then G is connected;

        hence thesis by A15;

      end;

    end

    registration

      let G be _Graph;

      cluster _trivial _finite Tree-like for Subgraph of G;

      existence

      proof

        set IT = the _finite _trivial simple Subgraph of G;

        take IT;

        thus thesis;

      end;

    end

    registration

      let G be acyclic _Graph;

      cluster -> acyclic for Subgraph of G;

      coherence

      proof

        let G2 be Subgraph of G;

        now

          given W2 be Walk of G2 such that

           A1: W2 is Cycle-like;

          reconsider W = W2 as Walk of G by GLIB_001: 167;

          

           A2: W is Path-like by A1, GLIB_001: 176;

          W is closed & W is non trivial by A1, GLIB_001: 176;

          then W is Cycle-like by A2, GLIB_001:def 31;

          hence contradiction by Def2;

        end;

        hence thesis;

      end;

    end

    definition

      let G be _Graph, v be Vertex of G;

      :: GLIB_002:def5

      func G .reachableFrom (v) -> non empty Subset of ( the_Vertices_of G) means

      : Def5: for x be object holds x in it iff ex W be Walk of G st W is_Walk_from (v,x);

      existence

      proof

        defpred P[ set] means ex W be Walk of G st W is_Walk_from (v,$1);

        consider IT be Subset of ( the_Vertices_of G) such that

         A1: for x be set holds x in IT iff x in ( the_Vertices_of G) & P[x] from SUBSET_1:sch 1;

        (G .walkOf v) is_Walk_from (v,v) by GLIB_001: 13;

        then

        reconsider IT as non empty Subset of ( the_Vertices_of G) by A1;

        take IT;

        let x be object;

        thus x in IT implies ex W be Walk of G st W is_Walk_from (v,x) by A1;

        assume

         A2: ex W be Walk of G st W is_Walk_from (v,x);

        then x is Vertex of G by GLIB_001: 18;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let IT1,IT2 be non empty Subset of ( the_Vertices_of G) such that

         A3: for x be object holds x in IT1 iff ex W be Walk of G st W is_Walk_from (v,x) and

         A4: for x be object holds x in IT2 iff ex W be Walk of G st W is_Walk_from (v,x);

        now

          let x be object;

          hereby

            assume x in IT1;

            then ex W be Walk of G st W is_Walk_from (v,x) by A3;

            hence x in IT2 by A4;

          end;

          assume x in IT2;

          then ex W be Walk of G st W is_Walk_from (v,x) by A4;

          hence x in IT1 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let G be _Graph, v be Vertex of G;

      :: GLIB_002:def6

      func G .reachableDFrom (v) -> non empty Subset of ( the_Vertices_of G) means

      : Def6: for x be object holds x in it iff ex W be DWalk of G st W is_Walk_from (v,x);

      existence

      proof

        set W = (G .walkOf v);

        defpred P[ set] means ex W be directed Walk of G st W is_Walk_from (v,$1);

        consider IT be Subset of ( the_Vertices_of G) such that

         A1: for x be set holds x in IT iff x in ( the_Vertices_of G) & P[x] from SUBSET_1:sch 1;

        W is_Walk_from (v,v) by GLIB_001: 13;

        then

        reconsider IT as non empty Subset of ( the_Vertices_of G) by A1;

        take IT;

        let x be object;

        thus x in IT implies ex W be directed Walk of G st W is_Walk_from (v,x) by A1;

        given W be directed Walk of G such that

         A2: W is_Walk_from (v,x);

        x is Vertex of G by A2, GLIB_001: 18;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let IT1,IT2 be non empty Subset of ( the_Vertices_of G) such that

         A3: for x be object holds x in IT1 iff ex W be directed Walk of G st W is_Walk_from (v,x) and

         A4: for x be object holds x in IT2 iff ex W be directed Walk of G st W is_Walk_from (v,x);

        now

          let x be object;

          hereby

            assume x in IT1;

            then ex W be directed Walk of G st W is_Walk_from (v,x) by A3;

            hence x in IT2 by A4;

          end;

          assume x in IT2;

          then ex W be directed Walk of G st W is_Walk_from (v,x) by A4;

          hence x in IT1 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    

     Lm1: for G be _Graph, v be Vertex of G holds v in (G .reachableFrom v)

    proof

      let G be _Graph, v be Vertex of G;

      (G .walkOf v) is_Walk_from (v,v) by GLIB_001: 13;

      hence thesis by Def5;

    end;

    

     Lm2: for G be _Graph, v1 be Vertex of G, e,x,y be object holds x in (G .reachableFrom v1) & e Joins (x,y,G) implies y in (G .reachableFrom v1)

    proof

      let G be _Graph, v1 be Vertex of G, e,x,y be object;

      set RFV = (G .reachableFrom v1);

      assume that

       A1: x in RFV and

       A2: e Joins (x,y,G);

      consider W be Walk of G such that

       A3: W is_Walk_from (v1,x) by A1, Def5;

      (W .addEdge e) is_Walk_from (v1,y) by A2, A3, GLIB_001: 66;

      hence thesis by Def5;

    end;

    

     Lm3: for G be _Graph, v1,v2 be Vertex of G holds v1 in (G .reachableFrom v2) implies (G .reachableFrom v1) = (G .reachableFrom v2)

    proof

      let G be _Graph, v1,v2 be Vertex of G;

      assume v1 in (G .reachableFrom v2);

      then

      consider WA be Walk of G such that

       A1: WA is_Walk_from (v2,v1) by Def5;

      

       A2: (WA .reverse() ) is_Walk_from (v1,v2) by A1, GLIB_001: 23;

      now

        let x be object;

        hereby

          assume x in (G .reachableFrom v1);

          then

          consider WB be Walk of G such that

           A3: WB is_Walk_from (v1,x) by Def5;

          (WA .append WB) is_Walk_from (v2,x) by A1, A3, GLIB_001: 31;

          hence x in (G .reachableFrom v2) by Def5;

        end;

        assume x in (G .reachableFrom v2);

        then

        consider WB be Walk of G such that

         A4: WB is_Walk_from (v2,x) by Def5;

        ((WA .reverse() ) .append WB) is_Walk_from (v1,x) by A2, A4, GLIB_001: 31;

        hence x in (G .reachableFrom v1) by Def5;

      end;

      hence thesis by TARSKI: 2;

    end;

    

     Lm4: for G be _Graph, W be Walk of G, v be Vertex of G holds v in (W .vertices() ) implies (W .vertices() ) c= (G .reachableFrom v)

    proof

      let G be _Graph, W be Walk of G, v be Vertex of G;

      assume v in (W .vertices() );

      then

      consider m be odd Element of NAT such that

       A1: m <= ( len W) and

       A2: (W . m) = v by GLIB_001: 87;

      let x be object;

      assume x in (W .vertices() );

      then

      consider n be odd Element of NAT such that

       A3: n <= ( len W) and

       A4: (W . n) = x by GLIB_001: 87;

      now

        per cases ;

          suppose m <= n;

          then (W .cut (m,n)) is_Walk_from (v,x) by A2, A3, A4, GLIB_001: 37;

          hence ex W2 be Walk of G st W2 is_Walk_from (v,x);

        end;

          suppose m > n;

          then (W .cut (n,m)) is_Walk_from (x,v) by A1, A2, A4, GLIB_001: 37;

          then ((W .cut (n,m)) .reverse() ) is_Walk_from (v,x) by GLIB_001: 23;

          hence ex W2 be Walk of G st W2 is_Walk_from (v,x);

        end;

      end;

      hence thesis by Def5;

    end;

    definition

      let G1 be _Graph, G2 be Subgraph of G1;

      :: GLIB_002:def7

      attr G2 is Component-like means

      : Def7: G2 is connected & not ex G3 be connected Subgraph of G1 st G2 c< G3;

    end

    registration

      let G be _Graph;

      cluster Component-like -> connected for Subgraph of G;

      coherence ;

    end

    registration

      let G be _Graph, v be Vertex of G;

      cluster -> Component-like for inducedSubgraph of G, (G .reachableFrom v);

      coherence

      proof

        let G2 be inducedSubgraph of G, (G .reachableFrom v);

        

         A1: ( the_Vertices_of G2) = (G .reachableFrom v) by GLIB_000:def 37;

        

         A2: ( the_Edges_of G2) = (G .edgesBetween (G .reachableFrom v)) by GLIB_000:def 37;

         A3:

        now

          

           A4: v in ( the_Vertices_of G2) by A1, Lm1;

          given G3 be connected Subgraph of G such that

           A5: G2 c< G3;

          G2 c= G3 by A5, GLIB_000:def 36;

          then

           A6: G2 is Subgraph of G3 by GLIB_000:def 35;

          then

           A7: ( the_Vertices_of G2) c= ( the_Vertices_of G3) by GLIB_000:def 32;

           A8:

          now

            given x be object such that

             A9: x in ( the_Vertices_of G3) and

             A10: not x in ( the_Vertices_of G2);

            consider W be Walk of G3 such that

             A11: W is_Walk_from (v,x) by A4, A7, A9, Def1;

            reconsider W as Walk of G by GLIB_001: 167;

            W is_Walk_from (v,x) by A11, GLIB_001: 19;

            hence contradiction by A1, A10, Def5;

          end;

          

           A12: ( the_Vertices_of G2) c= ( the_Vertices_of G3) by A6, GLIB_000:def 32;

          now

            per cases by A5, GLIB_000: 99;

              suppose ex x be object st x in ( the_Vertices_of G3) & not x in ( the_Vertices_of G2);

              hence contradiction by A8;

            end;

              suppose ex e be object st e in ( the_Edges_of G3) & not e in ( the_Edges_of G2);

              then

              consider e be set such that

               A13: e in ( the_Edges_of G3) and

               A14: not e in ( the_Edges_of G2);

              set v1 = (( the_Source_of G3) . e), v2 = (( the_Target_of G3) . e);

              

               A15: e Joins (v1,v2,G3) by A13, GLIB_000:def 13;

              then

               A16: e Joins (v1,v2,G) by GLIB_000: 72;

              now

                per cases ;

                  suppose ( the_Vertices_of G3) = ( the_Vertices_of G2);

                  then

                  reconsider v1, v2 as Vertex of G2 by A15, GLIB_000: 13;

                  v1 in (G .reachableFrom v) & v2 in (G .reachableFrom v) by A1;

                  hence contradiction by A2, A14, A16, GLIB_000: 32;

                end;

                  suppose ( the_Vertices_of G3) <> ( the_Vertices_of G2);

                  then ( the_Vertices_of G2) c< ( the_Vertices_of G3) by A12, XBOOLE_0:def 8;

                  hence contradiction by A8, XBOOLE_0: 6;

                end;

              end;

              hence contradiction;

            end;

          end;

          hence contradiction;

        end;

        now

          let x,y be Vertex of G2;

          consider W1R be Walk of G such that

           A17: W1R is_Walk_from (v,x) by A1, Def5;

          consider W2 be Walk of G such that

           A18: W2 is_Walk_from (v,y) by A1, Def5;

          set W1 = (W1R .reverse() ), W = (W1 .append W2);

          

           A19: W1 is_Walk_from (x,v) by A17, GLIB_001: 23;

          then

           A20: W is_Walk_from (x,y) by A18, GLIB_001: 31;

          

           A21: (W1 .last() ) = v by A19, GLIB_001:def 23;

          then

           A22: v in (W1 .vertices() ) by GLIB_001: 88;

          

           A23: (W .edges() ) c= (G .edgesBetween (W .vertices() )) by GLIB_001: 109;

          (W2 .first() ) = v by A18, GLIB_001:def 23;

          then (W .vertices() ) = ((W1 .vertices() ) \/ (W2 .vertices() )) by A21, GLIB_001: 93;

          then

           A24: v in (W .vertices() ) by A22, XBOOLE_0:def 3;

          then (G .edgesBetween (W .vertices() )) c= (G .edgesBetween ( the_Vertices_of G2)) by A1, Lm4, GLIB_000: 36;

          then (W .edges() ) c= (G .edgesBetween ( the_Vertices_of G2)) by A23;

          then

          reconsider W as Walk of G2 by A1, A2, A24, Lm4, GLIB_001: 170;

          take W;

          thus W is_Walk_from (x,y) by A20, GLIB_001: 19;

        end;

        then G2 is connected;

        hence thesis by A3;

      end;

    end

    registration

      let G be _Graph;

      cluster Component-like for Subgraph of G;

      existence

      proof

        set v = the Vertex of G;

        set IT = the inducedSubgraph of G, (G .reachableFrom v);

        take IT;

        thus thesis;

      end;

    end

    definition

      let G be _Graph;

      mode Component of G is Component-like Subgraph of G;

    end

    definition

      let G be _Graph;

      :: GLIB_002:def8

      func G .componentSet() -> non empty Subset-Family of ( the_Vertices_of G) means

      : Def8: for x be set holds x in it iff ex v be Vertex of G st x = (G .reachableFrom v);

      existence

      proof

        set v = the Vertex of G;

        defpred P[ set] means ex v be Vertex of G st $1 = (G .reachableFrom v);

        consider IT be Subset-Family of ( the_Vertices_of G) such that

         A1: for x be set holds x in IT iff x in ( bool ( the_Vertices_of G)) & P[x] from SUBSET_1:sch 1;

        set x = (G .reachableFrom v);

        x in IT by A1;

        then

        reconsider IT as non empty Subset-Family of ( the_Vertices_of G);

        take IT;

        thus thesis by A1;

      end;

      uniqueness

      proof

        defpred P[ object] means ex v be Vertex of G st $1 = (G .reachableFrom v);

        let IT1,IT2 be non empty Subset-Family of ( the_Vertices_of G) such that

         A2: for x be set holds x in IT1 iff P[x] and

         A3: for x be set holds x in IT2 iff P[x];

        now

          let x be object;

          x in IT1 iff P[x] by A2;

          hence x in IT1 iff x in IT2 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let G be _Graph, X be Element of (G .componentSet() );

      cluster -> Component-like for inducedSubgraph of G, X;

      coherence

      proof

        let G2 be inducedSubgraph of G, X;

        ex v be Vertex of G st X = (G .reachableFrom v) by Def8;

        hence thesis;

      end;

    end

    definition

      let G be _Graph;

      :: GLIB_002:def9

      func G .numComponents() -> Cardinal equals ( card (G .componentSet() ));

      coherence ;

    end

    definition

      let G be _finite _Graph;

      :: original: .numComponents()

      redefine

      func G .numComponents() -> non zero Element of NAT ;

      coherence

      proof

        (G .numComponents() ) = ( card (G .componentSet() ));

        hence thesis;

      end;

    end

    definition

      let G be _Graph, v be Vertex of G;

      :: GLIB_002:def10

      attr v is cut-vertex means for G2 be removeVertex of G, v holds (G .numComponents() ) in (G2 .numComponents() );

    end

    definition

      let G be _finite _Graph, v be Vertex of G;

      :: original: cut-vertex

      redefine

      :: GLIB_002:def11

      attr v is cut-vertex means for G2 be removeVertex of G, v holds (G .numComponents() ) < (G2 .numComponents() );

      compatibility

      proof

        hereby

          assume

           A1: v is cut-vertex;

          let G2 be removeVertex of G, v;

          ( card ( Segm (G .numComponents() ))) in ( card ( Segm (G2 .numComponents() ))) by A1;

          hence (G .numComponents() ) < (G2 .numComponents() ) by NAT_1: 41;

        end;

        assume

         A2: for G2 be removeVertex of G, v holds (G .numComponents() ) < (G2 .numComponents() );

        now

          let G2 be removeVertex of G, v;

          (G .numComponents() ) < (G2 .numComponents() ) by A2;

          then ( card ( Segm (G .numComponents() ))) in ( card ( Segm (G2 .numComponents() ))) by NAT_1: 41;

          hence (G .numComponents() ) in (G2 .numComponents() );

        end;

        hence thesis;

      end;

    end

    

     Lm5: for G1 be non _trivial connected _Graph, v be Vertex of G1, G2 be removeVertex of G1, v st v is endvertex holds G2 is connected

    proof

      let G1 be non _trivial connected _Graph, v be Vertex of G1, G2 be removeVertex of G1, v;

      set VG = ( the_Vertices_of G1), VG2 = ( the_Vertices_of G2);

      assume

       A1: v is endvertex;

      then

      consider ev be object such that

       A2: (v .edgesInOut() ) = {ev} and not ev Joins (v,v,G1) by GLIB_000:def 51;

      now

        let v19,v29 be Vertex of G2;

        reconsider v1 = v19, v2 = v29 as Vertex of G1 by GLIB_000: 42;

        consider W be Walk of G1 such that

         A3: W is_Walk_from (v1,v2) by Def1;

        set T = the Trail of W;

        

         A4: T is_Walk_from (v1,v2) by A3, GLIB_001: 160;

        then

         A5: (T . ( len T)) = v2 by GLIB_001: 17;

        v19 in VG2;

        then v19 in (VG \ {v}) by GLIB_000: 47;

        then

         A6: not v1 in {v} by XBOOLE_0:def 5;

        v29 in VG2;

        then v29 in (VG \ {v}) by GLIB_000: 47;

        then not v2 in {v} by XBOOLE_0:def 5;

        then

         A7: v2 <> v by TARSKI:def 1;

        

         A8: (T . 1) = v1 by A4, GLIB_001: 17;

        now

          let e be object;

          assume

           A9: e in (T .edges() );

          then

          consider n be even Element of NAT such that

           A10: 1 <= n and

           A11: n <= ( len T) and

           A12: (T . n) = e by GLIB_001: 99;

          n in ( dom T) by A10, A11, FINSEQ_3: 25;

          then

          consider n1 be odd Element of NAT such that

           A13: n1 = (n - 1) and

           A14: (n - 1) in ( dom T) and

           A15: (n + 1) in ( dom T) and

           A16: (T . n) Joins ((T . n1),(T . (n + 1)),G1) by GLIB_001: 9;

          

           A17: (n + 1) <= ( len T) by A15, FINSEQ_3: 25;

          

           A18: n1 <= ( len T) by A13, A14, FINSEQ_3: 25;

          now

            assume

             A19: e in (v .edgesInOut() );

            then

             A20: e = ev by A2, TARSKI:def 1;

            now

              per cases by A12, A16, A19, GLIB_000: 65;

                suppose

                 A21: (T . n1) = v;

                reconsider n2 = (n1 - 1) as even Element of NAT by ABIAN: 12, INT_1: 5;

                

                 A22: 1 <= n1 by ABIAN: 12;

                n1 <> 1 by A6, A8, A21, TARSKI:def 1;

                then

                 A23: 1 < n1 by A22, XXREAL_0: 1;

                then (1 + 1) <= n1 by NAT_1: 13;

                then

                 A24: ((1 + 1) - 1) <= n2 by XREAL_1: 13;

                (T .vertexAt n1) = v by A18, A21, GLIB_001:def 8;

                then (T . n2) in (v .edgesInOut() ) by A18, A23, GLIB_001: 11;

                then

                 A25: (T . n) = (T . n2) by A2, A12, A20, TARSKI:def 1;

                (n - 1) < (n - 0 ) by XREAL_1: 15;

                then (n1 - 1) < (n - 0 ) by A13, XREAL_1: 14;

                hence contradiction by A11, A25, A24, GLIB_001: 138;

              end;

                suppose

                 A26: (T . (n + 1)) = v;

                then

                 A27: (n + 1) < ( len T) by A7, A5, A17, XXREAL_0: 1;

                (T .vertexAt (n + 1)) = v by A17, A26, GLIB_001:def 8;

                then (T . ((n + 1) + 1)) in (v .edgesInOut() ) by A27, GLIB_001: 10;

                then

                 A28: (T . n) = (T . ((n + 1) + 1)) by A2, A12, A20, TARSKI:def 1;

                (n + 0 ) < (n + (1 + 1)) & ((n + 1) + 1) <= ( len T) by A27, NAT_1: 13, XREAL_1: 8;

                hence contradiction by A10, A28, GLIB_001: 138;

              end;

            end;

            hence contradiction;

          end;

          then e in (( the_Edges_of G1) \ (v .edgesInOut() )) by A9, XBOOLE_0:def 5;

          then e in (( the_Edges_of G1) \ (G1 .edgesInOut {v})) by GLIB_000:def 40;

          then e in (G1 .edgesBetween (( the_Vertices_of G1) \ {v})) by GLIB_000: 35;

          hence e in ( the_Edges_of G2) by GLIB_000: 47;

        end;

        then

         A29: (T .edges() ) c= ( the_Edges_of G2);

        

         A30: v1 <> v by A6, TARSKI:def 1;

        now

          let x be object;

          assume

           A31: x in (T .vertices() );

          now

            assume x = v;

            then v = (T .first() ) or v = (T .last() ) by A1, A31, GLIB_001: 143;

            hence contradiction by A30, A7, A4, GLIB_001:def 23;

          end;

          then not x in {v} by TARSKI:def 1;

          then x in (VG \ {v}) by A31, XBOOLE_0:def 5;

          hence x in VG2 by GLIB_000: 47;

        end;

        then (T .vertices() ) c= VG2;

        then

        reconsider W9 = T as Walk of G2 by A29, GLIB_001: 170;

        W9 is_Walk_from (v19,v29) by A4, GLIB_001: 19;

        hence ex W be Walk of G2 st W is_Walk_from (v19,v29);

      end;

      hence thesis;

    end;

    

     Lm6: for G be _Graph holds (ex v1 be Vertex of G st for v2 be Vertex of G holds ex W be Walk of G st W is_Walk_from (v1,v2)) implies G is connected

    proof

      let G be _Graph;

      given v1 be Vertex of G such that

       A1: for v2 be Vertex of G holds ex W be Walk of G st W is_Walk_from (v1,v2);

      now

        let x,y be Vertex of G;

        consider W1 be Walk of G such that

         A2: W1 is_Walk_from (v1,x) by A1;

        consider W2 be Walk of G such that

         A3: W2 is_Walk_from (v1,y) by A1;

        (W1 .reverse() ) is_Walk_from (x,v1) by A2, GLIB_001: 23;

        then ((W1 .reverse() ) .append W2) is_Walk_from (x,y) by A3, GLIB_001: 31;

        hence ex W be Walk of G st W is_Walk_from (x,y);

      end;

      hence thesis;

    end;

    

     Lm7: for G be _Graph holds (ex v be Vertex of G st (G .reachableFrom v) = ( the_Vertices_of G)) implies G is connected

    proof

      let G be _Graph;

      assume ex v be Vertex of G st (G .reachableFrom v) = ( the_Vertices_of G);

      then

      consider v be Vertex of G such that

       A1: (G .reachableFrom v) = ( the_Vertices_of G);

      now

        let x,y be Vertex of G;

        consider W1 be Walk of G such that

         A2: W1 is_Walk_from (v,x) by A1, Def5;

        consider W2 be Walk of G such that

         A3: W2 is_Walk_from (v,y) by A1, Def5;

        (W1 .reverse() ) is_Walk_from (x,v) by A2, GLIB_001: 23;

        then ((W1 .reverse() ) .append W2) is_Walk_from (x,y) by A3, GLIB_001: 31;

        hence ex W be Walk of G st W is_Walk_from (x,y);

      end;

      hence thesis;

    end;

    

     Lm8: for G be _Graph holds G is connected implies for v be Vertex of G holds (G .reachableFrom v) = ( the_Vertices_of G)

    proof

      let G be _Graph;

      assume

       A1: G is connected;

      let v be Vertex of G;

      now

        let x be object;

        thus x in (G .reachableFrom v) implies x in ( the_Vertices_of G);

        assume x in ( the_Vertices_of G);

        then ex W be Walk of G st W is_Walk_from (v,x) by A1;

        hence x in (G .reachableFrom v) by Def5;

      end;

      hence thesis by TARSKI: 2;

    end;

    

     Lm9: for G1,G2 be _Graph, v1 be Vertex of G1, v2 be Vertex of G2 st G1 == G2 & v1 = v2 holds (G1 .reachableFrom v1) = (G2 .reachableFrom v2)

    proof

      let G1,G2 be _Graph, v1 be Vertex of G1, v2 be Vertex of G2;

      assume that

       A1: G1 == G2 and

       A2: v1 = v2;

      now

        let x be object;

        hereby

          assume x in (G1 .reachableFrom v1);

          then

          consider W be Walk of G1 such that

           A3: W is_Walk_from (v2,x) by A2, Def5;

          reconsider W2 = W as Walk of G2 by A1, GLIB_001: 179;

          W2 is_Walk_from (v2,x) by A3, GLIB_001: 19;

          hence x in (G2 .reachableFrom v2) by Def5;

        end;

        assume x in (G2 .reachableFrom v2);

        then

        consider W be Walk of G2 such that

         A4: W is_Walk_from (v1,x) by A2, Def5;

        reconsider W2 = W as Walk of G1 by A1, GLIB_001: 179;

        W2 is_Walk_from (v1,x) by A4, GLIB_001: 19;

        hence x in (G1 .reachableFrom v1) by Def5;

      end;

      hence thesis by TARSKI: 2;

    end;

    

     Lm10: for G1 be _Graph, G2 be connected Subgraph of G1 holds G2 is spanning implies G1 is connected

    proof

      let G1 be _Graph, G2 be connected Subgraph of G1;

      assume

       A1: G2 is spanning;

      now

        let u9,v9 be Vertex of G1;

        reconsider u = u9, v = v9 as Vertex of G2 by A1, GLIB_000:def 33;

        consider W be Walk of G2 such that

         A2: W is_Walk_from (u,v) by Def1;

        reconsider W as Walk of G1 by GLIB_001: 167;

        take W;

        thus W is_Walk_from (u9,v9) by A2, GLIB_001: 19;

      end;

      hence thesis;

    end;

    

     Lm11: for G be _Graph holds G is connected iff (G .componentSet() ) = {( the_Vertices_of G)}

    proof

      let G be _Graph;

      hereby

        assume

         A1: G is connected;

        now

          set v = the Vertex of G;

          let x be object;

          hereby

            assume x in (G .componentSet() );

            then ex v be Vertex of G st x = (G .reachableFrom v) by Def8;

            then x = ( the_Vertices_of G) by A1, Lm8;

            hence x in {( the_Vertices_of G)} by TARSKI:def 1;

          end;

          assume x in {( the_Vertices_of G)};

          then

           A2: x = ( the_Vertices_of G) by TARSKI:def 1;

          (G .reachableFrom v) = ( the_Vertices_of G) by A1, Lm8;

          hence x in (G .componentSet() ) by A2, Def8;

        end;

        hence (G .componentSet() ) = {( the_Vertices_of G)} by TARSKI: 2;

      end;

      assume (G .componentSet() ) = {( the_Vertices_of G)};

      then ( the_Vertices_of G) in (G .componentSet() ) by TARSKI:def 1;

      then ex v be Vertex of G st (G .reachableFrom v) = ( the_Vertices_of G) by Def8;

      hence thesis by Lm7;

    end;

    

     Lm12: for G1,G2 be _Graph holds G1 == G2 implies (G1 .componentSet() ) = (G2 .componentSet() )

    proof

      let G1,G2 be _Graph;

      assume

       A1: G1 == G2;

      now

        let x be object;

        hereby

          assume x in (G1 .componentSet() );

          then

          consider v1 be Vertex of G1 such that

           A2: x = (G1 .reachableFrom v1) by Def8;

          reconsider v2 = v1 as Vertex of G2 by A1, GLIB_000:def 34;

          x = (G2 .reachableFrom v2) by A1, A2, Lm9;

          hence x in (G2 .componentSet() ) by Def8;

        end;

        assume x in (G2 .componentSet() );

        then

        consider v2 be Vertex of G2 such that

         A3: x = (G2 .reachableFrom v2) by Def8;

        reconsider v1 = v2 as Vertex of G1 by A1, GLIB_000:def 34;

        x = (G1 .reachableFrom v1) by A1, A3, Lm9;

        hence x in (G1 .componentSet() ) by Def8;

      end;

      hence thesis by TARSKI: 2;

    end;

    

     Lm13: for G be _Graph, x be set holds x in (G .componentSet() ) implies x is non empty Subset of ( the_Vertices_of G)

    proof

      let G be _Graph, x be set;

      assume x in (G .componentSet() );

      then ex v be Vertex of G st x = (G .reachableFrom v) by Def8;

      hence thesis;

    end;

    

     Lm14: for G be _Graph, C be Component of G holds ( the_Edges_of C) = (G .edgesBetween ( the_Vertices_of C))

    proof

      let G be _Graph, C be Component of G;

      reconsider VC = ( the_Vertices_of C) as Subset of ( the_Vertices_of G);

      set EB = (G .edgesBetween VC);

      (C .edgesBetween ( the_Vertices_of C)) c= EB by GLIB_000: 76;

      then

       A1: ( the_Edges_of C) c= EB by GLIB_000: 34;

      now

        let e be object;

        thus e in ( the_Edges_of C) implies e in EB by A1;

        assume

         A2: e in EB;

        now

          set GX = the inducedSubgraph of G, VC, EB;

          assume

           A3: not e in ( the_Edges_of C);

          

           A4: ( the_Edges_of GX) = EB by GLIB_000:def 37;

          ( the_Vertices_of GX) = VC by GLIB_000:def 37;

          then

           A5: C is spanning Subgraph of GX by A1, A4, GLIB_000: 44, GLIB_000:def 33;

          then GX is connected by Lm10;

          then not C c< GX by Def7;

          then GX == C or not C c= GX by GLIB_000:def 36;

          hence contradiction by A2, A3, A4, A5, GLIB_000:def 34, GLIB_000:def 35;

        end;

        hence e in ( the_Edges_of C);

      end;

      hence thesis by TARSKI: 2;

    end;

    

     Lm15: for G be _Graph, C1,C2 be Component of G holds ( the_Vertices_of C1) = ( the_Vertices_of C2) iff C1 == C2

    proof

      let G be _Graph, C1,C2 be Component of G;

      hereby

        assume

         A1: ( the_Vertices_of C1) = ( the_Vertices_of C2);

        

        then ( the_Edges_of C1) = (G .edgesBetween ( the_Vertices_of C2)) by Lm14

        .= ( the_Edges_of C2) by Lm14;

        hence C1 == C2 by A1, GLIB_000: 86;

      end;

      assume C1 == C2;

      hence thesis by GLIB_000:def 34;

    end;

    

     Lm16: for G be _Graph, C be Component of G, v be Vertex of G holds v in ( the_Vertices_of C) iff ( the_Vertices_of C) = (G .reachableFrom v)

    proof

      let G be _Graph, C be Component of G, v be Vertex of G;

      hereby

        assume

         A1: v in ( the_Vertices_of C);

        now

          let x be object;

          hereby

            assume x in ( the_Vertices_of C);

            then

            reconsider x9 = x as Vertex of C;

            consider W be Walk of C such that

             A2: W is_Walk_from (v,x9) by A1, Def1;

            reconsider W as Walk of G by GLIB_001: 167;

            W is_Walk_from (v,x) by A2, GLIB_001: 19;

            hence x in (G .reachableFrom v) by Def5;

          end;

          assume

           A3: x in (G .reachableFrom v);

          then

          reconsider x9 = x as Vertex of G;

          

           A4: (G .reachableFrom x9) = (G .reachableFrom v) by A3, Lm3;

          set CX = the inducedSubgraph of G, (G .reachableFrom x9);

           not C c< CX by Def7;

          then

           A5: C == CX or not C c= CX by GLIB_000:def 36;

          

           A6: ( the_Edges_of CX) = (G .edgesBetween (G .reachableFrom x9)) by GLIB_000:def 37;

          now

            let e be object;

            set v1 = (( the_Source_of C) . e), v2 = (( the_Target_of C) . e);

            assume

             A7: e in ( the_Edges_of C);

            then

            reconsider v1, v2 as Vertex of C by FUNCT_2: 5;

            e Joins (v1,v2,C) by A7, GLIB_000:def 13;

            then

             A8: e Joins (v1,v2,G) by GLIB_000: 72;

            consider W1 be Walk of C such that

             A9: W1 is_Walk_from (v,v1) by A1, Def1;

            reconsider W1 as Walk of G by GLIB_001: 167;

            consider W2 be Walk of C such that

             A10: W2 is_Walk_from (v,v2) by A1, Def1;

            reconsider W2 as Walk of G by GLIB_001: 167;

            W2 is_Walk_from (v,v2) by A10, GLIB_001: 19;

            then

             A11: v2 in (G .reachableFrom x9) by A4, Def5;

            W1 is_Walk_from (v,v1) by A9, GLIB_001: 19;

            then v1 in (G .reachableFrom x9) by A4, Def5;

            hence e in ( the_Edges_of CX) by A6, A8, A11, GLIB_000: 32;

          end;

          then

           A12: ( the_Edges_of C) c= ( the_Edges_of CX);

          

           A13: ( the_Vertices_of CX) = (G .reachableFrom x9) by GLIB_000:def 37;

          now

            let z be object;

            assume z in ( the_Vertices_of C);

            then

            consider W be Walk of C such that

             A14: W is_Walk_from (v,z) by A1, Def1;

            reconsider W as Walk of G by GLIB_001: 167;

            W is_Walk_from (v,z) by A14, GLIB_001: 19;

            hence z in ( the_Vertices_of CX) by A13, A4, Def5;

          end;

          then ( the_Vertices_of C) c= ( the_Vertices_of CX);

          then

           A15: C is Subgraph of CX by A12, GLIB_000: 44;

          x in ( the_Vertices_of CX) by A13, Lm1;

          hence x in ( the_Vertices_of C) by A5, A15, GLIB_000:def 34, GLIB_000:def 35;

        end;

        hence ( the_Vertices_of C) = (G .reachableFrom v) by TARSKI: 2;

      end;

      assume ( the_Vertices_of C) = (G .reachableFrom v);

      hence thesis by Lm1;

    end;

    

     Lm17: for G be _Graph, C1,C2 be Component of G, v be set st v in ( the_Vertices_of C1) & v in ( the_Vertices_of C2) holds C1 == C2

    proof

      let G be _Graph, C1,C2 be Component of G, v be set;

      assume that

       A1: v in ( the_Vertices_of C1) and

       A2: v in ( the_Vertices_of C2);

      reconsider v9 = v as Vertex of G by A1;

      ( the_Vertices_of C1) = (G .reachableFrom v9) & ( the_Vertices_of C2) = (G .reachableFrom v9) by A1, A2, Lm16;

      hence thesis by Lm15;

    end;

    

     Lm18: for G be _Graph holds G is connected iff (G .numComponents() ) = 1

    proof

      let G be _Graph;

      hereby

        assume G is connected;

        then (G .componentSet() ) = {( the_Vertices_of G)} by Lm11;

        hence (G .numComponents() ) = 1 by CARD_1: 30;

      end;

      assume (G .numComponents() ) = 1;

      then

      consider V be object such that

       A1: (G .componentSet() ) = {V} by CARD_2: 42;

      reconsider V as set by TARSKI: 1;

      now

        let v be object;

        assume v in ( the_Vertices_of G);

        then

        reconsider v9 = v as Vertex of G;

        now

          set V2 = (G .reachableFrom v9);

          assume

           A2: not v in V;

          V2 in (G .componentSet() ) by Def8;

          then not v in V2 by A1, A2, TARSKI:def 1;

          hence contradiction by Lm1;

        end;

        hence v in V;

      end;

      then

       A3: ( the_Vertices_of G) c= V;

      V in (G .componentSet() ) by A1, TARSKI:def 1;

      then V = ( the_Vertices_of G) by A3, XBOOLE_0:def 10;

      hence thesis by A1, Lm11;

    end;

    

     Lm19: for G be connected _Graph, v be Vertex of G holds v is non cut-vertex iff for G2 be removeVertex of G, v holds (G2 .numComponents() ) c= (G .numComponents() )

    proof

      let G be connected _Graph, v be Vertex of G;

      hereby

        assume v is non cut-vertex;

        then

        consider G3 be removeVertex of G, v such that

         A1: not (G .numComponents() ) in (G3 .numComponents() );

        let G2 be removeVertex of G, v;

        (G3 .numComponents() ) c= (G .numComponents() ) by A1, CARD_1: 4;

        hence (G2 .numComponents() ) c= (G .numComponents() ) by Lm12, GLIB_000: 93;

      end;

      assume

       A2: for G2 be removeVertex of G, v holds (G2 .numComponents() ) c= (G .numComponents() );

      now

        set X = the removeVertex of G, v;

        assume for G3 be removeVertex of G, v holds (G .numComponents() ) in (G3 .numComponents() );

        then

         A3: (G .numComponents() ) in (X .numComponents() );

        (X .numComponents() ) c= (G .numComponents() ) by A2;

        hence contradiction by A3, CARD_1: 4;

      end;

      hence thesis;

    end;

    

     Lm20: for G be connected _Graph, v be Vertex of G, G2 be removeVertex of G, v st not v is cut-vertex holds G2 is connected

    proof

      let G be connected _Graph, v be Vertex of G, G2 be removeVertex of G, v;

      assume

       A1: not v is cut-vertex;

      (G .numComponents() ) = 1 by Lm18;

      then (G2 .numComponents() ) c= ( succ 0 ) by A1, Lm19;

      then (G2 .numComponents() ) c= ( {} \/ { {} });

      

      then (G2 .numComponents() ) = ( {} \/ { {} }) by ZFMISC_1: 33

      .= ( succ 0 )

      .= 1;

      hence thesis by Lm18;

    end;

    

     Lm21: for G be non _trivial _finite connected _Graph holds ex v1,v2 be Vertex of G st v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex

    proof

      let G be non _trivial _finite connected _Graph;

      defpred P[ Nat] means for G be non _trivial _finite connected _Graph st (G .order() ) = $1 holds ex v1,v2 be Vertex of G st v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex;

      now

        let k be Nat;

        assume

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

        now

          let G be non _trivial _finite connected _Graph such that

           A2: (G .order() ) = k;

          

           A3: (G .numComponents() ) = 1 by Lm18;

          now

            per cases ;

              suppose

               A4: not ex v be Vertex of G st v is cut-vertex;

              consider v1,v2 be Vertex of G such that

               A5: v1 <> v2 by GLIB_000: 21;

              take v1, v2;

              thus v1 <> v2 by A5;

              thus not v1 is cut-vertex & not v2 is cut-vertex by A4;

            end;

              suppose ex cv be Vertex of G st cv is cut-vertex;

              then

              consider cv be Vertex of G such that

               A6: cv is cut-vertex;

              set G2 = the removeVertex of G, cv;

              1 < (G2 .numComponents() ) by A3, A6;

              then (1 + 1) <= (G2 .numComponents() ) by NAT_1: 13;

              then ( card 2) <= ( card (G2 .componentSet() ));

              then ( Segm ( card 2)) c= ( Segm ( card (G2 .componentSet() ))) by NAT_1: 39;

              then 2 c= ( card (G2 .componentSet() ));

              then

              consider C1,C2 be object such that

               A7: C1 in (G2 .componentSet() ) & C2 in (G2 .componentSet() ) and

               A8: C1 <> C2 by PENCIL_1: 2;

              reconsider C1, C2 as Element of (G2 .componentSet() ) by A7;

              set CC1 = the inducedSubgraph of G2, C1;

              set CC2 = the inducedSubgraph of G2, C2;

              

               A9: ( the_Vertices_of G2) = (( the_Vertices_of G) \ {cv}) by GLIB_000: 47;

              (G .edgesBetween (( the_Vertices_of G) \ {cv})) = (( the_Edges_of G) \ (G .edgesInOut {cv})) by GLIB_000: 35;

              then (G .edgesBetween (( the_Vertices_of G) \ {cv})) = (( the_Edges_of G) \ (cv .edgesInOut() )) by GLIB_000:def 40;

              then

               A10: ( the_Edges_of G2) = (( the_Edges_of G) \ (cv .edgesInOut() )) by GLIB_000: 47;

              

               A11: ((G2 .order() ) + 1) = k by A2, GLIB_000: 48;

               A12:

              now

                let C be Component of G2;

                now

                  set x = the Vertex of C;

                  assume

                   A13: for a be Vertex of C holds not ex e be set st e Joins (cv,a,G);

                  ( the_Vertices_of C) c= ( the_Vertices_of G2);

                  then

                  reconsider x9 = x as Vertex of G2;

                  ( the_Vertices_of G2) c= ( the_Vertices_of G);

                  then

                  reconsider x99 = x9 as Vertex of G;

                  consider W be Walk of G such that

                   A14: W is_Walk_from (cv,x99) by Def1;

                  set P = the Path of W;

                  

                   A15: P is_Walk_from (cv,x99) by A14, GLIB_001: 160;

                  then

                   A16: (P .first() ) = cv by GLIB_001:def 23;

                  set P2 = (P .cut (((2 * 1) + 1),( len P)));

                  

                   A17: 1 <= ( len P) by ABIAN: 12;

                  

                   A18: (P .last() ) = x by A15, GLIB_001:def 23;

                  then

                   A19: (P . ( len P)) = x by GLIB_001:def 7;

                   not x9 in {cv} by A9, XBOOLE_0:def 5;

                  then

                   A20: x <> cv by TARSKI:def 1;

                  then

                   A21: P is non trivial by A16, A18, GLIB_001: 127;

                  then

                   A22: ((2 * 1) + 1) <= ( len P) by GLIB_001: 125;

                  then P2 is_Walk_from ((P . 3),(P . ( len P))) by GLIB_001: 37;

                  then

                   A23: P2 is_Walk_from ((P . 3),x) by A18, GLIB_001:def 7;

                  

                   A24: (P . ((2 * 0 ) + 1)) = cv by A16, GLIB_001:def 6;

                  now

                    assume cv in (P2 .vertices() );

                    then

                    consider n be odd Element of NAT such that

                     A25: n <= ( len P2) and

                     A26: (P2 . n) = cv by GLIB_001: 87;

                    

                     A27: 1 <= n by ABIAN: 12;

                    then

                     A28: (1 + 0 ) < (n + 2) by XREAL_1: 8;

                    

                     A29: n in ( dom P2) by A25, A27, FINSEQ_3: 25;

                    then ((3 + n) - 1) in ( dom P) by A22, GLIB_001: 47;

                    then

                     A30: (2 + n) <= ( len P) by FINSEQ_3: 25;

                    (P . ((3 + n) - 1)) = cv by A22, A26, A29, GLIB_001: 47;

                    hence contradiction by A20, A24, A19, A30, A28, GLIB_001:def 28;

                  end;

                  then

                  reconsider P2 as Walk of G2 by GLIB_001: 171;

                  P2 is_Walk_from ((P . 3),x) by A23, GLIB_001: 19;

                  then (P2 .reverse() ) is_Walk_from (x,(P . 3)) by GLIB_001: 23;

                  then

                   A31: (P . 3) in (G2 .reachableFrom x9) by Def5;

                  ( len P) <> 1 by A21, GLIB_001: 125;

                  then ((2 * 0 ) + 1) < ( len P) by A17, XXREAL_0: 1;

                  then (P . (1 + 1)) Joins ((P . 1),(P . (1 + 2)),G) by GLIB_001:def 3;

                  then

                   A32: (P . 2) Joins (cv,(P . 3),G) by A16, GLIB_001:def 6;

                  ( the_Vertices_of C) = (G2 .reachableFrom x9) by Lm16;

                  hence contradiction by A13, A32, A31;

                end;

                then

                consider a be Vertex of C, e be set such that

                 A33: e Joins (cv,a,G);

                

                 A34: e in ( the_Edges_of G) by A33, GLIB_000:def 13;

                now

                  per cases ;

                    suppose C is _trivial;

                    then

                    consider v99 be Vertex of C such that

                     A35: ( the_Vertices_of C) = {v99} by GLIB_000: 22;

                    ( the_Vertices_of C) c= ( the_Vertices_of G2);

                    then

                    reconsider v9 = v99 as Vertex of G2;

                    reconsider v = v9 as Vertex of G by GLIB_000: 42;

                    take v;

                    thus v in ( the_Vertices_of C);

                     not v9 in {cv} by A9, XBOOLE_0:def 5;

                    then

                     A36: v9 <> cv by TARSKI:def 1;

                    

                     A37: {v9} = (G2 .reachableFrom v9) by A35, Lm16;

                    now

                      set G3 = the removeVertex of G, v;

                       A38:

                      now

                        let e,z be set;

                        assume

                         A39: e Joins (v,z,G);

                        then

                         A40: e in ( the_Edges_of G) by GLIB_000:def 13;

                        now

                          assume that

                           A41: z <> v and

                           A42: z <> cv;

                           not e in (cv .edgesInOut() ) by A36, A39, A42, GLIB_000: 65;

                          then e in ( the_Edges_of G2) by A10, A40, XBOOLE_0:def 5;

                          then e Joins (v,z,G2) by A39, GLIB_000: 73;

                          then z in (G2 .reachableFrom v9) by Lm1, Lm2;

                          hence contradiction by A37, A41, TARSKI:def 1;

                        end;

                        hence z = v or z = cv;

                      end;

                      now

                        let x,y be Vertex of G3;

                        now

                          per cases ;

                            suppose

                             A43: x = y;

                            set W = (G3 .walkOf x);

                            take W;

                            thus W is_Walk_from (x,y) by A43, GLIB_001: 13;

                          end;

                            suppose

                             A44: x <> y;

                            reconsider x9 = x, y9 = y as Vertex of G by GLIB_000: 42;

                            consider W be Walk of G such that

                             A45: W is_Walk_from (x9,y9) by Def1;

                            set P = the Path of W;

                            

                             A46: P is_Walk_from (x9,y9) by A45, GLIB_001: 160;

                            

                             A47: ( the_Vertices_of G3) = (( the_Vertices_of G) \ {v}) by GLIB_000: 47;

                            then not x in {v} by XBOOLE_0:def 5;

                            then x <> v by TARSKI:def 1;

                            then

                             A48: v <> (P . 1) by A46, GLIB_001: 17;

                             not y in {v} by A47, XBOOLE_0:def 5;

                            then y <> v by TARSKI:def 1;

                            then

                             A49: v <> (P . ( len P)) by A46, GLIB_001: 17;

                            now

                              assume v in (P .vertices() );

                              then

                              consider n be odd Element of NAT such that

                               A50: n <= ( len P) and

                               A51: (P . n) = v by GLIB_001: 87;

                              1 <= n by ABIAN: 12;

                              then 1 < n by A48, A51, XXREAL_0: 1;

                              then (1 + 1) <= n by NAT_1: 13;

                              then

                              reconsider n2 = (n - (2 * 1)) as odd Element of NAT by INT_1: 5;

                               A52:

                              now

                                

                                 A53: n2 < (n - 0 ) by XREAL_1: 15;

                                assume (P . n2) = v;

                                hence contradiction by A48, A50, A51, A53, GLIB_001:def 28;

                              end;

                              set e1 = (P . (n2 + 1)), e2 = (P . (n + 1));

                              (n - 2) < (( len P) - 0 ) by A50, XREAL_1: 15;

                              then e1 Joins ((P . n2),(P . (n2 + 2)),G) by GLIB_001:def 3;

                              then

                               A54: (P . n2) = cv by A38, A51, A52, GLIB_000: 14;

                              

                               A55: n < ( len P) by A49, A50, A51, XXREAL_0: 1;

                              then

                               A56: (n + 2) <= ( len P) by GLIB_001: 1;

                               A57:

                              now

                                

                                 A58: (n + 0 ) < (n + 2) by XREAL_1: 8;

                                assume (P . (n + 2)) = v;

                                hence contradiction by A48, A51, A56, A58, GLIB_001:def 28;

                              end;

                              n2 < (n - 0 ) by XREAL_1: 15;

                              then

                               A59: (n2 + 0 ) < (n + 2) by XREAL_1: 8;

                              e2 Joins (v,(P . (n + 2)),G) by A51, A55, GLIB_001:def 3;

                              then

                               A60: (P . (n + 2)) = cv by A38, A57;

                              then cv = (P . 1) by A54, A56, A59, GLIB_001:def 28;

                              then

                               A61: cv = x by A46, GLIB_001: 17;

                              cv = (P . ( len P)) by A54, A56, A60, A59, GLIB_001:def 28;

                              hence contradiction by A44, A46, A61, GLIB_001: 17;

                            end;

                            then

                            reconsider P as Walk of G3 by GLIB_001: 171;

                            take P;

                            thus P is_Walk_from (x,y) by A46, GLIB_001: 19;

                          end;

                        end;

                        hence ex P be Walk of G3 st P is_Walk_from (x,y);

                      end;

                      then

                       A62: G3 is connected;

                      assume v is cut-vertex;

                      then 1 < (G3 .numComponents() ) by A3;

                      hence contradiction by A62, Lm18;

                    end;

                    hence not v is cut-vertex;

                  end;

                    suppose C is non _trivial;

                    then

                    reconsider C9 = C as non _trivial _Graph;

                    ((C .order() ) + 0 ) < ((G2 .order() ) + 1) by GLIB_000: 75, XREAL_1: 8;

                    then

                    consider v1,v2 be Vertex of C9 such that

                     A63: v1 <> v2 and

                     A64: not v1 is cut-vertex and

                     A65: not v2 is cut-vertex by A1, A11;

                    set C9R1 = the removeVertex of C9, v1;

                    

                     A66: C9R1 is connected by A64, Lm20;

                    set C9R2 = the removeVertex of C9, v2;

                    

                     A67: ( the_Vertices_of C9R1) = (( the_Vertices_of C9) \ {v1}) by GLIB_000: 47;

                    v2 in ( the_Vertices_of G2) by GLIB_000: 42;

                    then not v2 in {cv} by A9, XBOOLE_0:def 5;

                    then

                     A68: v2 <> cv by TARSKI:def 1;

                    

                     A69: ( the_Vertices_of C9R2) = (( the_Vertices_of C9) \ {v2}) by GLIB_000: 47;

                    v1 in ( the_Vertices_of G2) by GLIB_000: 42;

                    then not v1 in {cv} by A9, XBOOLE_0:def 5;

                    then

                     A70: v1 <> cv by TARSKI:def 1;

                    

                     A71: C9R2 is connected by A65, Lm20;

                    now

                      per cases ;

                        suppose

                         A72: not v1 in (cv .allNeighbors() );

                        reconsider v9 = v1 as Vertex of G2 by GLIB_000: 42;

                        reconsider v = v9 as Vertex of G by GLIB_000: 42;

                        take v;

                        thus v in ( the_Vertices_of C);

                        set G3 = the removeVertex of G, v;

                        

                         A73: ( the_Vertices_of G3) = (( the_Vertices_of G) \ {v}) by GLIB_000: 47;

                         not cv in {v} by A70, TARSKI:def 1;

                        then

                        reconsider cv9 = cv as Vertex of G3 by A73, XBOOLE_0:def 5;

                        

                         A74: v1 <> a by A33, A72, GLIB_000: 71;

                        

                         A75: ( the_Vertices_of C) = (G2 .reachableFrom v9) by Lm16;

                        now

                          let y be Vertex of G3;

                          now

                            per cases ;

                              suppose y = cv;

                              then (G3 .walkOf y) is_Walk_from (cv9,y) by GLIB_001: 13;

                              hence ex W be Walk of G3 st W is_Walk_from (cv9,y);

                            end;

                              suppose

                               A76: y <> cv;

                              now

                                per cases ;

                                  suppose

                                   A77: y in ( the_Vertices_of C);

                                   not a in {v1} by A74, TARSKI:def 1;

                                  then

                                   A78: a in ( the_Vertices_of C9R1) by A67, XBOOLE_0:def 5;

                                   not y in {v1} by A73, XBOOLE_0:def 5;

                                  then y in ( the_Vertices_of C9R1) by A67, A77, XBOOLE_0:def 5;

                                  then

                                  consider W be Walk of C9R1 such that

                                   A79: W is_Walk_from (y,a) by A66, A78;

                                  

                                   A80: (W . 1) = y & (W . ( len W)) = a by A79, GLIB_001: 17;

                                   A81:

                                  now

                                    assume v in (W .vertices() );

                                    then not v in {v1} by A67, XBOOLE_0:def 5;

                                    hence contradiction by TARSKI:def 1;

                                  end;

                                   not e in (v .edgesInOut() ) by A33, A70, A74, GLIB_000: 65;

                                  then e in (( the_Edges_of G) \ (v .edgesInOut() )) by A34, XBOOLE_0:def 5;

                                  then e in (( the_Edges_of G) \ (G .edgesInOut {v})) by GLIB_000:def 40;

                                  then e in (G .edgesBetween (( the_Vertices_of G) \ {v})) by GLIB_000: 35;

                                  then e in ( the_Edges_of G3) by GLIB_000: 47;

                                  then e Joins (cv,a,G3) by A33, GLIB_000: 73;

                                  then

                                   A82: e Joins (a,cv,G3) by GLIB_000: 14;

                                  reconsider W as Walk of C by GLIB_001: 167;

                                  reconsider W as Walk of G2 by GLIB_001: 167;

                                  reconsider W as Walk of G by GLIB_001: 167;

                                   not v in (W .vertices() ) by A81, GLIB_001: 98;

                                  then

                                  reconsider W as Walk of G3 by GLIB_001: 171;

                                  W is_Walk_from (y,a) by A80, GLIB_001: 17;

                                  then (W .addEdge e) is_Walk_from (y,cv) by A82, GLIB_001: 66;

                                  then ((W .addEdge e) .reverse() ) is_Walk_from (cv,y) by GLIB_001: 23;

                                  hence ex W be Walk of G3 st W is_Walk_from (cv9,y);

                                end;

                                  suppose

                                   A83: not y in ( the_Vertices_of C);

                                  reconsider y9 = y as Vertex of G by GLIB_000: 42;

                                  consider W be Walk of G such that

                                   A84: W is_Walk_from (cv,y9) by Def1;

                                  set P = the Path of W;

                                  

                                   A85: P is_Walk_from (cv,y9) by A84, GLIB_001: 160;

                                  then

                                   A86: (P . ( len P)) = y9 by GLIB_001: 17;

                                  

                                   A87: (P . 1) = cv by A85, GLIB_001: 17;

                                  now

                                    assume v in (P .vertices() );

                                    then

                                    consider n be odd Element of NAT such that

                                     A88: n <= ( len P) and

                                     A89: (P . n) = v by GLIB_001: 87;

                                    set P2 = (P .cut (n,( len P)));

                                    

                                     A90: P2 is_Walk_from (v,y9) by A86, A88, A89, GLIB_001: 37;

                                    1 <= n by ABIAN: 12;

                                    then

                                     A91: 1 < n by A70, A87, A89, XXREAL_0: 1;

                                    now

                                      assume cv in (P2 .vertices() );

                                      then

                                      consider m be odd Element of NAT such that

                                       A92: m <= ( len P2) and

                                       A93: (P2 . m) = cv by GLIB_001: 87;

                                      1 <= m by ABIAN: 12;

                                      then

                                       A94: m in ( dom P2) by A92, FINSEQ_3: 25;

                                      then

                                       A95: (P . ((n + m) - 1)) = cv by A88, A93, GLIB_001: 47;

                                      (1 + 1) < (n + m) by A91, ABIAN: 12, XREAL_1: 8;

                                      then ((1 + 1) - 1) < ((n + m) - 1) by XREAL_1: 14;

                                      then

                                       A96: ((2 * 0 ) + 1) < ((n + m) - 1);

                                      

                                       A97: ((n + m) - 1) in ( dom P) by A88, A94, GLIB_001: 47;

                                      then ((n + m) - 1) <= ( len P) by FINSEQ_3: 25;

                                      hence contradiction by A76, A87, A86, A95, A97, A96, GLIB_001:def 28;

                                    end;

                                    then

                                    reconsider P2 as Walk of G2 by GLIB_001: 171;

                                    P2 is_Walk_from (v,y9) by A90, GLIB_001: 19;

                                    hence contradiction by A75, A83, Def5;

                                  end;

                                  then

                                  reconsider P as Walk of G3 by GLIB_001: 171;

                                  take P;

                                  thus P is_Walk_from (cv9,y) by A85, GLIB_001: 19;

                                end;

                              end;

                              hence ex W be Walk of G3 st W is_Walk_from (cv9,y);

                            end;

                          end;

                          hence ex W be Walk of G3 st W is_Walk_from (cv9,y);

                        end;

                        then G3 is connected by Lm6;

                        then (G3 .numComponents() ) = 1 by Lm18;

                        hence not v is cut-vertex by A3;

                      end;

                        suppose

                         A98: v1 in (cv .allNeighbors() ) & not v2 in (cv .allNeighbors() );

                        reconsider v9 = v2 as Vertex of G2 by GLIB_000: 42;

                        reconsider v = v9 as Vertex of G by GLIB_000: 42;

                        take v;

                        thus v in ( the_Vertices_of C);

                        set G3 = the removeVertex of G, v;

                        

                         A99: ( the_Vertices_of G3) = (( the_Vertices_of G) \ {v}) by GLIB_000: 47;

                         not cv in {v} by A68, TARSKI:def 1;

                        then

                        reconsider cv9 = cv as Vertex of G3 by A99, XBOOLE_0:def 5;

                        

                         A100: v2 <> a by A33, A98, GLIB_000: 71;

                        

                         A101: ( the_Vertices_of C) = (G2 .reachableFrom v9) by Lm16;

                        now

                          let y be Vertex of G3;

                          now

                            per cases ;

                              suppose y = cv;

                              then (G3 .walkOf y) is_Walk_from (cv9,y) by GLIB_001: 13;

                              hence ex W be Walk of G3 st W is_Walk_from (cv9,y);

                            end;

                              suppose

                               A102: y <> cv;

                              now

                                per cases ;

                                  suppose

                                   A103: y in ( the_Vertices_of C);

                                   not a in {v2} by A100, TARSKI:def 1;

                                  then

                                   A104: a in ( the_Vertices_of C9R2) by A69, XBOOLE_0:def 5;

                                   not y in {v2} by A99, XBOOLE_0:def 5;

                                  then y in ( the_Vertices_of C9R2) by A69, A103, XBOOLE_0:def 5;

                                  then

                                  consider W be Walk of C9R2 such that

                                   A105: W is_Walk_from (y,a) by A71, A104;

                                  

                                   A106: (W . 1) = y & (W . ( len W)) = a by A105, GLIB_001: 17;

                                   A107:

                                  now

                                    assume v in (W .vertices() );

                                    then not v in {v2} by A69, XBOOLE_0:def 5;

                                    hence contradiction by TARSKI:def 1;

                                  end;

                                   not e in (v .edgesInOut() ) by A33, A68, A100, GLIB_000: 65;

                                  then e in (( the_Edges_of G) \ (v .edgesInOut() )) by A34, XBOOLE_0:def 5;

                                  then e in (( the_Edges_of G) \ (G .edgesInOut {v})) by GLIB_000:def 40;

                                  then e in (G .edgesBetween (( the_Vertices_of G) \ {v})) by GLIB_000: 35;

                                  then e in ( the_Edges_of G3) by GLIB_000: 47;

                                  then e Joins (cv,a,G3) by A33, GLIB_000: 73;

                                  then

                                   A108: e Joins (a,cv,G3) by GLIB_000: 14;

                                  reconsider W as Walk of C by GLIB_001: 167;

                                  reconsider W as Walk of G2 by GLIB_001: 167;

                                  reconsider W as Walk of G by GLIB_001: 167;

                                   not v in (W .vertices() ) by A107, GLIB_001: 98;

                                  then

                                  reconsider W as Walk of G3 by GLIB_001: 171;

                                  W is_Walk_from (y,a) by A106, GLIB_001: 17;

                                  then (W .addEdge e) is_Walk_from (y,cv) by A108, GLIB_001: 66;

                                  then ((W .addEdge e) .reverse() ) is_Walk_from (cv,y) by GLIB_001: 23;

                                  hence ex W be Walk of G3 st W is_Walk_from (cv9,y);

                                end;

                                  suppose

                                   A109: not y in ( the_Vertices_of C);

                                  reconsider y9 = y as Vertex of G by GLIB_000: 42;

                                  consider W be Walk of G such that

                                   A110: W is_Walk_from (cv,y9) by Def1;

                                  set P = the Path of W;

                                  

                                   A111: P is_Walk_from (cv,y9) by A110, GLIB_001: 160;

                                  then

                                   A112: (P . ( len P)) = y9 by GLIB_001: 17;

                                  

                                   A113: (P . 1) = cv by A111, GLIB_001: 17;

                                  now

                                    assume v in (P .vertices() );

                                    then

                                    consider n be odd Element of NAT such that

                                     A114: n <= ( len P) and

                                     A115: (P . n) = v by GLIB_001: 87;

                                    set P2 = (P .cut (n,( len P)));

                                    

                                     A116: P2 is_Walk_from (v,y9) by A112, A114, A115, GLIB_001: 37;

                                    1 <= n by ABIAN: 12;

                                    then

                                     A117: 1 < n by A68, A113, A115, XXREAL_0: 1;

                                    now

                                      assume cv in (P2 .vertices() );

                                      then

                                      consider m be odd Element of NAT such that

                                       A118: m <= ( len P2) and

                                       A119: (P2 . m) = cv by GLIB_001: 87;

                                      1 <= m by ABIAN: 12;

                                      then

                                       A120: m in ( dom P2) by A118, FINSEQ_3: 25;

                                      then

                                       A121: (P . ((n + m) - 1)) = cv by A114, A119, GLIB_001: 47;

                                      (1 + 1) < (n + m) by A117, ABIAN: 12, XREAL_1: 8;

                                      then ((1 + 1) - 1) < ((n + m) - 1) by XREAL_1: 14;

                                      then

                                       A122: ((2 * 0 ) + 1) < ((n + m) - 1);

                                      

                                       A123: ((n + m) - 1) in ( dom P) by A114, A120, GLIB_001: 47;

                                      then ((n + m) - 1) <= ( len P) by FINSEQ_3: 25;

                                      hence contradiction by A102, A113, A112, A121, A123, A122, GLIB_001:def 28;

                                    end;

                                    then

                                    reconsider P2 as Walk of G2 by GLIB_001: 171;

                                    P2 is_Walk_from (v,y9) by A116, GLIB_001: 19;

                                    hence contradiction by A101, A109, Def5;

                                  end;

                                  then

                                  reconsider P as Walk of G3 by GLIB_001: 171;

                                  take P;

                                  thus P is_Walk_from (cv9,y) by A111, GLIB_001: 19;

                                end;

                              end;

                              hence ex W be Walk of G3 st W is_Walk_from (cv9,y);

                            end;

                          end;

                          hence ex W be Walk of G3 st W is_Walk_from (cv9,y);

                        end;

                        then G3 is connected by Lm6;

                        then (G3 .numComponents() ) = 1 by Lm18;

                        hence not v is cut-vertex by A3;

                      end;

                        suppose v1 in (cv .allNeighbors() ) & v2 in (cv .allNeighbors() );

                        then

                        consider e be object such that

                         A124: e Joins (cv,v2,G) by GLIB_000: 71;

                        reconsider v9 = v1 as Vertex of G2 by GLIB_000: 42;

                        set a = v2;

                        reconsider v = v9 as Vertex of G by GLIB_000: 42;

                        take v;

                        thus v in ( the_Vertices_of C);

                        set G3 = the removeVertex of G, v;

                        

                         A125: ( the_Vertices_of G3) = (( the_Vertices_of G) \ {v}) by GLIB_000: 47;

                         not cv in {v} by A70, TARSKI:def 1;

                        then

                        reconsider cv9 = cv as Vertex of G3 by A125, XBOOLE_0:def 5;

                        

                         A126: ( the_Vertices_of C) = (G2 .reachableFrom v9) by Lm16;

                        

                         A127: e in ( the_Edges_of G) by A124, GLIB_000:def 13;

                        now

                          let y be Vertex of G3;

                          now

                            per cases ;

                              suppose y = cv;

                              then (G3 .walkOf y) is_Walk_from (cv9,y) by GLIB_001: 13;

                              hence ex W be Walk of G3 st W is_Walk_from (cv9,y);

                            end;

                              suppose

                               A128: y <> cv;

                              now

                                per cases ;

                                  suppose

                                   A129: y in ( the_Vertices_of C);

                                   not a in {v1} by A63, TARSKI:def 1;

                                  then

                                   A130: a in ( the_Vertices_of C9R1) by A67, XBOOLE_0:def 5;

                                   not y in {v1} by A125, XBOOLE_0:def 5;

                                  then y in ( the_Vertices_of C9R1) by A67, A129, XBOOLE_0:def 5;

                                  then

                                  consider W be Walk of C9R1 such that

                                   A131: W is_Walk_from (y,a) by A66, A130;

                                  

                                   A132: (W . 1) = y & (W . ( len W)) = a by A131, GLIB_001: 17;

                                   A133:

                                  now

                                    assume v in (W .vertices() );

                                    then not v in {v1} by A67, XBOOLE_0:def 5;

                                    hence contradiction by TARSKI:def 1;

                                  end;

                                   not e in (v .edgesInOut() ) by A63, A70, A124, GLIB_000: 65;

                                  then e in (( the_Edges_of G) \ (v .edgesInOut() )) by A127, XBOOLE_0:def 5;

                                  then e in (( the_Edges_of G) \ (G .edgesInOut {v})) by GLIB_000:def 40;

                                  then e in (G .edgesBetween (( the_Vertices_of G) \ {v})) by GLIB_000: 35;

                                  then e in ( the_Edges_of G3) by GLIB_000: 47;

                                  then e Joins (cv,a,G3) by A124, GLIB_000: 73;

                                  then

                                   A134: e Joins (a,cv,G3) by GLIB_000: 14;

                                  reconsider W as Walk of C by GLIB_001: 167;

                                  reconsider W as Walk of G2 by GLIB_001: 167;

                                  reconsider W as Walk of G by GLIB_001: 167;

                                   not v in (W .vertices() ) by A133, GLIB_001: 98;

                                  then

                                  reconsider W as Walk of G3 by GLIB_001: 171;

                                  W is_Walk_from (y,a) by A132, GLIB_001: 17;

                                  then (W .addEdge e) is_Walk_from (y,cv) by A134, GLIB_001: 66;

                                  then ((W .addEdge e) .reverse() ) is_Walk_from (cv,y) by GLIB_001: 23;

                                  hence ex W be Walk of G3 st W is_Walk_from (cv9,y);

                                end;

                                  suppose

                                   A135: not y in ( the_Vertices_of C);

                                  reconsider y9 = y as Vertex of G by GLIB_000: 42;

                                  consider W be Walk of G such that

                                   A136: W is_Walk_from (cv,y9) by Def1;

                                  set P = the Path of W;

                                  

                                   A137: P is_Walk_from (cv,y9) by A136, GLIB_001: 160;

                                  then

                                   A138: (P . ( len P)) = y9 by GLIB_001: 17;

                                  

                                   A139: (P . 1) = cv by A137, GLIB_001: 17;

                                  now

                                    assume v in (P .vertices() );

                                    then

                                    consider n be odd Element of NAT such that

                                     A140: n <= ( len P) and

                                     A141: (P . n) = v by GLIB_001: 87;

                                    set P2 = (P .cut (n,( len P)));

                                    

                                     A142: P2 is_Walk_from (v,y9) by A138, A140, A141, GLIB_001: 37;

                                    1 <= n by ABIAN: 12;

                                    then

                                     A143: 1 < n by A70, A139, A141, XXREAL_0: 1;

                                    now

                                      assume cv in (P2 .vertices() );

                                      then

                                      consider m be odd Element of NAT such that

                                       A144: m <= ( len P2) and

                                       A145: (P2 . m) = cv by GLIB_001: 87;

                                      1 <= m by ABIAN: 12;

                                      then

                                       A146: m in ( dom P2) by A144, FINSEQ_3: 25;

                                      then

                                       A147: (P . ((n + m) - 1)) = cv by A140, A145, GLIB_001: 47;

                                      (1 + 1) < (n + m) by A143, ABIAN: 12, XREAL_1: 8;

                                      then ((1 + 1) - 1) < ((n + m) - 1) by XREAL_1: 14;

                                      then

                                       A148: ((2 * 0 ) + 1) < ((n + m) - 1);

                                      

                                       A149: ((n + m) - 1) in ( dom P) by A140, A146, GLIB_001: 47;

                                      then ((n + m) - 1) <= ( len P) by FINSEQ_3: 25;

                                      hence contradiction by A128, A139, A138, A147, A149, A148, GLIB_001:def 28;

                                    end;

                                    then

                                    reconsider P2 as Walk of G2 by GLIB_001: 171;

                                    P2 is_Walk_from (v,y9) by A142, GLIB_001: 19;

                                    hence contradiction by A126, A135, Def5;

                                  end;

                                  then

                                  reconsider P as Walk of G3 by GLIB_001: 171;

                                  take P;

                                  thus P is_Walk_from (cv9,y) by A137, GLIB_001: 19;

                                end;

                              end;

                              hence ex W be Walk of G3 st W is_Walk_from (cv9,y);

                            end;

                          end;

                          hence ex W be Walk of G3 st W is_Walk_from (cv9,y);

                        end;

                        then G3 is connected by Lm6;

                        then (G3 .numComponents() ) = 1 by Lm18;

                        hence not v is cut-vertex by A3;

                      end;

                    end;

                    hence ex v be Vertex of G st v in ( the_Vertices_of C) & not v is cut-vertex;

                  end;

                end;

                hence ex v be Vertex of G st v in ( the_Vertices_of C) & not v is cut-vertex;

              end;

              then

              consider v1 be Vertex of G such that

               A150: v1 in ( the_Vertices_of CC1) and

               A151: not v1 is cut-vertex;

              consider v2 be Vertex of G such that

               A152: v2 in ( the_Vertices_of CC2) and

               A153: not v2 is cut-vertex by A12;

              take v1, v2;

              now

                C2 is non empty Subset of ( the_Vertices_of G2) by Lm13;

                then

                 A154: ( the_Vertices_of CC2) = C2 by GLIB_000:def 37;

                C1 is non empty Subset of ( the_Vertices_of G2) by Lm13;

                then

                 A155: ( the_Vertices_of CC1) = C1 by GLIB_000:def 37;

                assume v1 = v2;

                then CC1 == CC2 by A150, A152, Lm17;

                hence contradiction by A8, A155, A154, GLIB_000:def 34;

              end;

              hence v1 <> v2;

              thus not v1 is cut-vertex & not v2 is cut-vertex by A151, A153;

            end;

          end;

          hence ex v1,v2 be Vertex of G st v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex;

        end;

        hence P[k];

      end;

      then

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

      

       A157: for k be Nat holds P[k] from NAT_1:sch 4( A156);

      (G .order() ) = (G .order() );

      hence thesis by A157;

    end;

    registration

      let G be non _trivial _finite connected _Graph;

      cluster non cut-vertex for Vertex of G;

      existence

      proof

        ex v1,v2 be Vertex of G st v1 <> v2 & ( not v1 is cut-vertex) & not v2 is cut-vertex by Lm21;

        hence thesis;

      end;

    end

    

     Lm22: for G be acyclic _Graph, W be Path of G, e be set st not e in (W .edges() ) & e in ((W .last() ) .edgesInOut() ) holds (W .addEdge e) is Path-like

    proof

      let G be acyclic _Graph, W be Path of G, e be set;

      assume that

       A1: not e in (W .edges() ) and

       A2: e in ((W .last() ) .edgesInOut() );

      set v = ((W .last() ) .adj e), W2 = (W .addEdge e);

      

       A3: e Joins ((W .last() ),((W .last() ) .adj e),G) by A2, GLIB_000: 67;

      then

       A4: ( len W2) = (( len W) + 2) by GLIB_001: 64;

      

       A5: W2 is Trail-like by A1, A2, GLIB_001: 142;

      now

        per cases ;

          suppose

           A6: W is trivial;

          then for n be odd Element of NAT st 1 < n & n <= ( len W) holds (W . n) <> v by GLIB_001: 126;

          hence thesis by A1, A3, A6, GLIB_001: 150;

        end;

          suppose

           A7: W is non trivial;

           A8:

          now

            let n be odd Element of NAT ;

            assume that

             A9: 1 < n and

             A10: n <= ( len W);

            now

              set W3 = (W2 .cut (n,( len W2)));

              assume

               A11: (W . n) = v;

              

               A12: n <= ( len W2) by A4, A10, NAT_1: 12;

              then

               A13: (W3 .first() ) = (W2 . n) by GLIB_001: 37;

              now

                assume W3 is trivial;

                then ( len W3) = 1 by GLIB_001: 126;

                then (1 + n) = (( len W2) + 1) by A12, GLIB_001: 36;

                then ((2 + ( len W)) - ( len W)) <= (( len W) - ( len W)) by A4, A10, XREAL_1: 13;

                then 2 <= 0 ;

                hence contradiction;

              end;

              then

              consider W4 be Path of W3 such that

               A14: W4 is non trivial by A5, GLIB_001: 166;

              (W3 .last() ) = (W2 . ( len W2)) by A12, GLIB_001: 37;

              

              then

               A15: (W3 .last() ) = (W2 .last() ) by GLIB_001:def 7

              .= v by A3, GLIB_001: 63;

              n in ( dom W) by A9, A10, FINSEQ_3: 25;

              then (W3 .first() ) = v by A3, A11, A13, GLIB_001: 65;

              then W4 is_Walk_from (v,v) by A15, GLIB_001:def 32;

              then W4 is closed by GLIB_001: 119;

              then W4 is Cycle-like by A14, GLIB_001:def 31;

              hence contradiction by Def2;

            end;

            hence (W . n) <> v;

          end;

           not W is closed by A7, GLIB_001:def 31, Def2;

          hence thesis by A1, A3, A8, GLIB_001: 150;

        end;

      end;

      hence thesis;

    end;

    

     Lm23: for G be non _trivial _finite acyclic _Graph st ( the_Edges_of G) <> {} holds ex v1,v2 be Vertex of G st v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in (G .reachableFrom v1)

    proof

      let G be non _trivial _finite acyclic _Graph such that

       A1: ( the_Edges_of G) <> {} ;

      defpred P[ Nat] means ex W be Path of G st ( len W) = $1;

      set e = the Element of ( the_Edges_of G);

       A2:

      now

        let k be Nat;

        assume P[k];

        then

        consider P be Path of G such that

         A3: ( len P) = k;

        (2 * ( len (P .vertexSeq() ))) <= (2 * ((G .order() ) + 1)) by GLIB_001: 154, XREAL_1: 64;

        then (k + 1) <= (2 * ((G .order() ) + 1)) by A3, GLIB_001:def 14;

        then ((k + 1) - 1) <= ((2 * ((G .order() ) + 1)) - 0 ) by XREAL_1: 13;

        hence k <= (2 * ((G .order() ) + 1));

      end;

      set src = (( the_Source_of G) . e), tar = (( the_Target_of G) . e);

      e Joins (src,tar,G) by A1, GLIB_000:def 13;

      then

       A4: ( len (G .walkOf (src,e,tar))) = 3 by GLIB_001: 14;

      then

       A5: ex k be Nat st P[k];

      consider k be Nat such that

       A6: P[k] & for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A2, A5);

      consider W be Path of G such that

       A7: ( len W) = k and

       A8: for n be Nat st P[n] holds n <= k by A6;

      

       A9: ( len (W .reverse() )) = k by A7, GLIB_001: 21;

      

       A10: 3 <= ( len W) by A4, A7, A8;

      then

       A11: W is non trivial by GLIB_001: 125;

       A12:

      now

        assume (W .first() ) = (W .last() );

        then W is closed by GLIB_001:def 24;

        then W is Cycle-like by A11, GLIB_001:def 31;

        hence contradiction by Def2;

      end;

      then

       A13: W is open by GLIB_001:def 24;

       A14:

      now

        let W be Path of G;

        assume that

         A15: ( len W) = k and

         A16: W is open;

        (2 + 1) <= ( len W) by A4, A8, A15;

        then 2 < ( len W) by NAT_1: 13;

        then

        reconsider lenW2 = (( len W) - (2 * 1)) as odd Element of NAT by INT_1: 5;

        

         A17: (lenW2 + 2) = ( len W);

        

         A18: W is non trivial by A7, A10, A15, GLIB_001: 125;

        now

          (W .last() ) in (W .vertices() ) by GLIB_001: 88;

          then not (W .last() ) is isolated by A18, GLIB_001: 135;

          then ((W .last() ) .degree() ) <> 0 by GLIB_000:def 50;

          then ( card ((W .last() ) .edgesInOut() )) <> 0 by GLIB_000: 19;

          then 0 < ( card ((W .last() ) .edgesInOut() )) by NAT_1: 3;

          then

           A19: ( 0 + 1) <= ( card ((W .last() ) .edgesInOut() )) by NAT_1: 13;

          assume not (W .last() ) is endvertex;

          then ((W .last() ) .degree() ) <> 1 by GLIB_000:def 52;

          then ( card ((W .last() ) .edgesInOut() )) <> 1 by GLIB_000: 19;

          then 1 < ( card ((W .last() ) .edgesInOut() )) by A19, XXREAL_0: 1;

          then

          consider e1,e2 be set such that

           A20: e1 in ((W .last() ) .edgesInOut() ) and

           A21: e2 in ((W .last() ) .edgesInOut() ) & e1 <> e2 by NAT_1: 59;

          now

            per cases ;

              suppose

               A22: e1 = (W . (lenW2 + 1));

              take e2;

              thus e2 in ((W .last() ) .edgesInOut() ) & e2 <> (W . (lenW2 + 1)) by A21, A22;

            end;

              suppose

               A23: e1 <> (W . (lenW2 + 1));

              take e1;

              thus e1 in ((W .last() ) .edgesInOut() ) & e1 <> (W . (lenW2 + 1)) by A20, A23;

            end;

          end;

          then

          consider e be set such that

           A24: e in ((W .last() ) .edgesInOut() ) and

           A25: e <> (W . (lenW2 + 1));

          consider v be Vertex of G such that

           A26: e Joins ((W .last() ),v,G) by A24, GLIB_000: 64;

          now

            per cases ;

              suppose v in (W .vertices() );

              then

              consider n be odd Element of NAT such that

               A27: n <= ( len W) and

               A28: (W . n) = v by GLIB_001: 87;

              set m = (W .rfind n);

              set W2 = (W .cut (m,( len W)));

              

               A29: m <= ( len W) by A27, GLIB_001:def 22;

              then (W2 .last() ) = (W . ( len W)) by GLIB_001: 37;

              then

               A30: e Joins ((W2 .last() ),v,G) by A26, GLIB_001:def 7;

              (W . m) = v by A27, A28, GLIB_001:def 22;

              then

               A31: (W2 .first() ) = v by A29, GLIB_001: 37;

              

               A32: e in ((W2 .last() ) .edgesInOut() ) by A30, GLIB_000: 62;

              now

                per cases ;

                  suppose

                   A33: not e in (W2 .edges() );

                  

                   A34: (W2 .addEdge e) is non trivial by A30, GLIB_001: 132;

                  ((W2 .addEdge e) .first() ) = v & ((W2 .addEdge e) .last() ) = v by A31, A30, GLIB_001: 63;

                  then

                   A35: (W2 .addEdge e) is closed by GLIB_001:def 24;

                  (W2 .addEdge e) is Path-like by A32, A33, Lm22;

                  then (W2 .addEdge e) is Cycle-like by A35, A34, GLIB_001:def 31;

                  hence contradiction by Def2;

                end;

                  suppose

                   A36: e in (W2 .edges() );

                  (W2 .edges() ) c= (W .edges() ) by GLIB_001: 106;

                  then

                  consider a be even Element of NAT such that

                   A37: 1 <= a and

                   A38: a <= ( len W) and

                   A39: (W . a) = e by A36, GLIB_001: 99;

                  reconsider a1 = (a - 1) as odd Element of NAT by A37, INT_1: 5;

                  

                   A40: a1 < (( len W) - 0 ) by A38, XREAL_1: 15;

                  a < (lenW2 + 2) by A38, XXREAL_0: 1;

                  then (a + 1) <= ((lenW2 + 1) + 1) by NAT_1: 13;

                  then a <= (lenW2 + 1) by XREAL_1: 6;

                  then

                   A41: a < (lenW2 + 1) by A25, A39, XXREAL_0: 1;

                  (a1 + 1) = a;

                  then

                   A42: e Joins ((W . a1),(W . (a1 + 2)),G) by A39, A40, GLIB_001:def 3;

                  now

                    per cases by A26, A42, GLIB_000: 15;

                      suppose (W .last() ) = (W . a1) & v = (W . (a1 + 2));

                      then (W . ( len W)) = (W . a1) by GLIB_001:def 7;

                      hence contradiction by A16, A40, GLIB_001: 147;

                    end;

                      suppose

                       A43: (W .last() ) = (W . (a1 + 2)) & v = (W . a1);

                      a1 < ((lenW2 + 1) - 1) by A41, XREAL_1: 14;

                      then

                       A44: (a1 + 2) < ( len W) by A17, XREAL_1: 8;

                      (W . ( len W)) = (W . (a1 + 2)) by A43, GLIB_001:def 7;

                      hence contradiction by A16, A44, GLIB_001: 147;

                    end;

                  end;

                  hence contradiction;

                end;

              end;

              hence contradiction;

            end;

              suppose

               A45: not v in (W .vertices() );

              

               A46: ( len (W .addEdge e)) = (k + 2) by A15, A26, GLIB_001: 64;

              (W .addEdge e) is Path-like by A16, A26, A45, GLIB_001: 151;

              then (k + 2) <= (k + 0 ) by A8, A46;

              hence contradiction by XREAL_1: 6;

            end;

          end;

          hence contradiction;

        end;

        hence (W .last() ) is endvertex;

      end;

      W is_Walk_from ((W .first() ),(W .last() )) by GLIB_001:def 23;

      then

       A47: (W .last() ) in (G .reachableFrom (W .first() )) by Def5;

      (W .reverse() ) is open by A13, GLIB_001: 120;

      then ((W .reverse() ) .last() ) is endvertex by A14, A9;

      then

       A48: (W .first() ) is endvertex by GLIB_001: 22;

      (W .last() ) is endvertex by A7, A13, A14;

      hence thesis by A12, A48, A47;

    end;

    

     Lm24: for G be non _trivial _finite Tree-like _Graph holds ex v1,v2 be Vertex of G st v1 <> v2 & v1 is endvertex & v2 is endvertex

    proof

      let G be non _trivial _finite Tree-like _Graph;

      consider v1,v2 be Vertex of G such that

       A1: v1 <> v2 by GLIB_000: 21;

      consider W be Walk of G such that

       A2: W is_Walk_from (v1,v2) by Def1;

       A3:

      now

        assume ( len W) = 1;

        

        then

         A4: (W .last() ) = (W . 1) by GLIB_001:def 7

        .= (W .first() ) by GLIB_001:def 6;

        (W .first() ) = v1 by A2, GLIB_001:def 23;

        hence contradiction by A1, A2, A4, GLIB_001:def 23;

      end;

      1 <= ( len W) by ABIAN: 12;

      then 1 < ( len W) by A3, XXREAL_0: 1;

      then (1 + 1) <= ( len W) by NAT_1: 13;

      then (1 + 1) in ( dom W) by FINSEQ_3: 25;

      then (W . (2 * 1)) in ( the_Edges_of G) by GLIB_001: 8;

      then ex v1,v2 be Vertex of G st v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in (G .reachableFrom v1) by Lm23;

      hence thesis;

    end;

    registration

      let G be non _trivial _finite Tree-like _Graph;

      cluster endvertex for Vertex of G;

      existence

      proof

        consider v1,v2 be Vertex of G such that v1 <> v2 and

         A1: v1 is endvertex and v2 is endvertex by Lm24;

        take v1;

        thus thesis by A1;

      end;

    end

    registration

      let G be non _trivial _finite Tree-like _Graph, v be endvertex Vertex of G;

      cluster -> Tree-like for removeVertex of G, v;

      coherence by Lm5;

    end

    definition

      let GF be Graph-yielding Function;

      :: GLIB_002:def12

      attr GF is connected means for x be object st x in ( dom GF) holds ex G be _Graph st (GF . x) = G & G is connected;

      :: GLIB_002:def13

      attr GF is acyclic means for x be object st x in ( dom GF) holds ex G be _Graph st (GF . x) = G & G is acyclic;

      :: GLIB_002:def14

      attr GF is Tree-like means for x be object st x in ( dom GF) holds ex G be _Graph st (GF . x) = G & G is Tree-like;

    end

    definition

      let GF be non empty Graph-yielding Function;

      :: original: connected

      redefine

      :: GLIB_002:def15

      attr GF is connected means

      : Def12b: for x be Element of ( dom GF) holds (GF . x) is connected;

      compatibility

      proof

        hereby

          assume

           A1: GF is connected;

          let x be Element of ( dom GF);

          consider G be _Graph such that

           A2: (GF . x) = G & G is connected by A1;

          thus (GF . x) is connected by A2;

        end;

        assume

         A3: for x be Element of ( dom GF) holds (GF . x) is connected;

        let x be object;

        assume x in ( dom GF);

        then

        reconsider y = x as Element of ( dom GF);

        take (GF . y);

        thus thesis by A3;

      end;

      :: original: acyclic

      redefine

      :: GLIB_002:def16

      attr GF is acyclic means

      : Def13b: for x be Element of ( dom GF) holds (GF . x) is acyclic;

      compatibility

      proof

        hereby

          assume

           A1: GF is acyclic;

          let x be Element of ( dom GF);

          consider G be _Graph such that

           A2: (GF . x) = G & G is acyclic by A1;

          thus (GF . x) is acyclic by A2;

        end;

        assume

         A3: for x be Element of ( dom GF) holds (GF . x) is acyclic;

        let x be object;

        assume x in ( dom GF);

        then

        reconsider y = x as Element of ( dom GF);

        take (GF . y);

        thus thesis by A3;

      end;

      :: original: Tree-like

      redefine

      :: GLIB_002:def17

      attr GF is Tree-like means for x be Element of ( dom GF) holds (GF . x) is Tree-like;

      compatibility

      proof

        hereby

          assume

           A1: GF is Tree-like;

          let x be Element of ( dom GF);

          consider G be _Graph such that

           A2: (GF . x) = G & G is Tree-like by A1;

          thus (GF . x) is Tree-like by A2;

        end;

        assume

         A3: for x be Element of ( dom GF) holds (GF . x) is Tree-like;

        let x be object;

        assume x in ( dom GF);

        then

        reconsider y = x as Element of ( dom GF);

        take (GF . y);

        thus thesis by A3;

      end;

    end

    

     LmNat: for F be ManySortedSet of NAT , n be object holds n is Nat iff n in ( dom F)

    proof

      let F be ManySortedSet of NAT , n be object;

      hereby

        assume n is Nat;

        then n in NAT by ORDINAL1:def 12;

        hence n in ( dom F) by PARTFUN1:def 2;

      end;

      assume n in ( dom F);

      then n in NAT by PARTFUN1:def 2;

      hence n is Nat;

    end;

    definition

      let GSq be GraphSeq;

      :: original: connected

      redefine

      :: GLIB_002:def18

      attr GSq is connected means

      : Def12: for n be Nat holds (GSq . n) is connected;

      compatibility

      proof

        hereby

          assume

           A1: GSq is connected;

          let x be Nat;

          x in ( dom GSq) by LmNat;

          then x is Element of ( dom GSq);

          hence (GSq . x) is connected by A1;

        end;

        assume

         A2: for x be Nat holds (GSq . x) is connected;

        let x be Element of ( dom GSq);

        x is Nat by LmNat;

        hence thesis by A2;

      end;

      :: original: acyclic

      redefine

      :: GLIB_002:def19

      attr GSq is acyclic means

      : Def13: for n be Nat holds (GSq . n) is acyclic;

      compatibility

      proof

        hereby

          assume

           A1: GSq is acyclic;

          let x be Nat;

          x in ( dom GSq) by LmNat;

          then x is Element of ( dom GSq);

          hence (GSq . x) is acyclic by A1;

        end;

        assume

         A2: for x be Nat holds (GSq . x) is acyclic;

        let x be Element of ( dom GSq);

        x is Nat by LmNat;

        hence thesis by A2;

      end;

      :: original: Tree-like

      redefine

      :: GLIB_002:def20

      attr GSq is Tree-like means for n be Nat holds (GSq . n) is Tree-like;

      compatibility

      proof

        hereby

          assume

           A1: GSq is Tree-like;

          let x be Nat;

          x in ( dom GSq) by LmNat;

          then x is Element of ( dom GSq);

          hence (GSq . x) is Tree-like by A1;

        end;

        assume

         A2: for x be Nat holds (GSq . x) is Tree-like;

        let x be Element of ( dom GSq);

        x is Nat by LmNat;

        hence thesis by A2;

      end;

    end

    registration

      cluster connected acyclic Tree-like non empty for Graph-yielding Function;

      existence

      proof

        reconsider GSq = ( NAT --> the Tree-like _Graph) as GraphSeq;

        take GSq;

        thus thesis;

      end;

    end

    registration

      cluster _trivial -> connected for Graph-yielding Function;

      coherence

      proof

        let GF be Graph-yielding Function;

        assume

         A1: GF is _trivial;

        let x be object;

        assume x in ( dom GF);

        then

        consider G be _Graph such that

         A2: (GF . x) = G & G is _trivial by A1, GLIB_000:def 60;

        take G;

        thus thesis by A2;

      end;

      cluster _trivial loopless -> Tree-like for Graph-yielding Function;

      coherence

      proof

        let GF be Graph-yielding Function;

        assume

         A1: GF is _trivial loopless;

        let x be object;

        assume

         A2: x in ( dom GF);

        then

        consider G be _Graph such that

         A3: (GF . x) = G & G is _trivial by A1, GLIB_000:def 60;

        consider G0 be _Graph such that

         A4: (GF . x) = G0 & G0 is loopless by A1, A2, GLIB_000:def 59;

        take G;

        thus thesis by A3, A4;

      end;

      cluster acyclic -> simple for Graph-yielding Function;

      coherence

      proof

        let GF be Graph-yielding Function;

        assume

         A1: GF is acyclic;

        now

          let x be object;

          assume x in ( dom GF);

          then

          consider G be _Graph such that

           A2: (GF . x) = G & G is acyclic by A1;

          take G;

          thus (GF . x) = G & G is simple by A2;

        end;

        hence thesis by GLIB_000:def 64;

      end;

      cluster Tree-like -> acyclic connected for Graph-yielding Function;

      coherence

      proof

        let GF be Graph-yielding Function;

        assume

         A1: GF is Tree-like;

        for x be object st x in ( dom GF) holds ex G be _Graph st (GF . x) = G & G is acyclic

        proof

          let x be object;

          assume x in ( dom GF);

          then

          consider G be _Graph such that

           A2: (GF . x) = G & G is Tree-like by A1;

          take G;

          thus thesis by A2;

        end;

        hence GF is acyclic;

        for x be object st x in ( dom GF) holds ex G be _Graph st (GF . x) = G & G is connected

        proof

          let x be object;

          assume x in ( dom GF);

          then

          consider G be _Graph such that

           A2: (GF . x) = G & G is Tree-like by A1;

          take G;

          thus thesis by A2;

        end;

        hence thesis;

      end;

      cluster acyclic connected -> Tree-like for Graph-yielding Function;

      coherence

      proof

        let GF be Graph-yielding Function;

        assume

         A1: GF is acyclic connected;

        let x be object;

        assume

         A2: x in ( dom GF);

        then

        consider G be _Graph such that

         A3: (GF . x) = G & G is acyclic by A1;

        consider G0 be _Graph such that

         A4: (GF . x) = G0 & G0 is connected by A1, A2;

        take G;

        thus thesis by A3, A4;

      end;

    end

    registration

      cluster halting _finite Tree-like for GraphSeq;

      existence

      proof

        set G = the _finite Tree-like _Graph;

        set F = ( NAT --> G);

        

         A1: ( dom F) = NAT ;

        reconsider F as ManySortedSet of NAT ;

        reconsider F as GraphSeq;

        

         A2: (F . (1 + 1)) = G;

        take F;

        (F . 1) = G;

        hence F is halting by A2, GLIB_000:def 55;

        now

          let x be Nat;

          x in NAT by ORDINAL1:def 12;

          then (F . x) in ( rng F) by A1, FUNCT_1: 3;

          then (F . x) in {G} by FUNCOP_1: 8;

          hence (F . x) is _finite & (F . x) is Tree-like by TARSKI:def 1;

        end;

        hence thesis by GLIB_000:def 74;

      end;

    end

    registration

      let GF be connected non empty Graph-yielding Function;

      let x be Element of ( dom GF);

      cluster (GF . x) -> connected;

      coherence by Def12b;

    end

    registration

      let GF be acyclic non empty Graph-yielding Function;

      let x be Element of ( dom GF);

      cluster (GF . x) -> acyclic;

      coherence by Def13b;

    end

    registration

      let GF be Tree-like non empty Graph-yielding Function;

      let x be Element of ( dom GF);

      cluster (GF . x) -> Tree-like;

      coherence ;

    end

    registration

      let GSq be connected GraphSeq, n be Nat;

      cluster (GSq . n) -> connected;

      coherence by Def12;

    end

    registration

      let GSq be acyclic GraphSeq, n be Nat;

      cluster (GSq . n) -> acyclic;

      coherence by Def13;

    end

    registration

      let GSq be Tree-like GraphSeq, n be Nat;

      cluster (GSq . n) -> Tree-like;

      coherence ;

    end

    begin

    reserve G,G1,G2 for _Graph;

    reserve e,x,y for set;

    reserve v,v1,v2 for Vertex of G;

    reserve W for Walk of G;

    ::$Canceled

    theorem :: GLIB_002:2

    

     Th1: for G be non _trivial connected _Graph, v be Vertex of G holds not v is isolated

    proof

      let G be non _trivial connected _Graph, v be Vertex of G;

      consider v1,v2 be Vertex of G such that

       A1: v1 <> v2 by GLIB_000: 21;

      now

        per cases ;

          suppose v1 = v;

          hence ex u be Vertex of G st u <> v by A1;

        end;

          suppose v1 <> v;

          hence ex u be Vertex of G st u <> v;

        end;

      end;

      then

      consider u be Vertex of G such that

       A2: u <> v;

      consider W be Walk of G such that

       A3: W is_Walk_from (u,v) by Def1;

      

       A4: (W .first() ) = u by A3, GLIB_001:def 23;

      

       A5: (W .last() ) = v by A3, GLIB_001:def 23;

      then v in (W .vertices() ) by GLIB_001: 88;

      hence thesis by A2, A4, A5, GLIB_001: 127, GLIB_001: 135;

    end;

    theorem :: GLIB_002:3

    

     Th2: for G1 be non _trivial _Graph, v be Vertex of G1, G2 be removeVertex of G1, v st G2 is connected & ex e be set st e in (v .edgesInOut() ) & not e Joins (v,v,G1) holds G1 is connected

    proof

      let G1 be non _trivial _Graph, v be Vertex of G1, G2 be removeVertex of G1, v;

      assume that

       A1: G2 is connected and

       A2: ex e be set st e in (v .edgesInOut() ) & not e Joins (v,v,G1);

       A3:

      now

        let x be Vertex of G1;

        assume x <> v;

        then not x in {v} by TARSKI:def 1;

        then x in (( the_Vertices_of G1) \ {v}) by XBOOLE_0:def 5;

        hence x in ( the_Vertices_of G2) by GLIB_000: 47;

      end;

      consider e be set such that

       A4: e in (v .edgesInOut() ) and

       A5: not e Joins (v,v,G1) by A2;

      set v3 = (v .adj e);

      v <> v3 by A4, A5, GLIB_000: 67;

      then

      reconsider v39 = v3 as Vertex of G2 by A3;

      

       A6: e Joins (v,v3,G1) by A4, GLIB_000: 67;

      then

       A7: e Joins (v3,v,G1) by GLIB_000: 14;

      now

        let v1,v2 be Vertex of G1;

        now

          per cases ;

            suppose v1 <> v;

            then

            reconsider v19 = v1 as Vertex of G2 by A3;

            now

              per cases ;

                suppose v2 <> v;

                then

                reconsider v29 = v2 as Vertex of G2 by A3;

                consider W9 be Walk of G2 such that

                 A8: W9 is_Walk_from (v19,v29) by A1;

                reconsider W = W9 as Walk of G1 by GLIB_001: 167;

                W is_Walk_from (v1,v2) by A8, GLIB_001: 19;

                hence ex W be Walk of G1 st W is_Walk_from (v1,v2);

              end;

                suppose

                 A9: v2 = v;

                consider W9 be Walk of G2 such that

                 A10: W9 is_Walk_from (v19,v39) by A1;

                reconsider W = W9 as Walk of G1 by GLIB_001: 167;

                W is_Walk_from (v1,v3) by A10, GLIB_001: 19;

                then (W .first() ) = v1 & (W .last() ) = v3 by GLIB_001:def 23;

                then (W .addEdge e) is_Walk_from (v1,v2) by A7, A9, GLIB_001: 63;

                hence ex W be Walk of G1 st W is_Walk_from (v1,v2);

              end;

            end;

            hence ex W be Walk of G1 st W is_Walk_from (v1,v2);

          end;

            suppose

             A11: v1 = v;

            now

              per cases ;

                suppose v2 <> v;

                then

                reconsider v29 = v2 as Vertex of G2 by A3;

                set W1 = (G1 .walkOf (v1,e,v3));

                consider W29 be Walk of G2 such that

                 A12: W29 is_Walk_from (v39,v29) by A1;

                reconsider W2 = W29 as Walk of G1 by GLIB_001: 167;

                

                 A13: W2 is_Walk_from (v3,v2) by A12, GLIB_001: 19;

                take W = (W1 .append W2);

                W1 is_Walk_from (v1,v3) by A6, A11, GLIB_001: 15;

                hence W is_Walk_from (v1,v2) by A13, GLIB_001: 31;

              end;

                suppose

                 A14: v2 = v;

                take W = (G1 .walkOf v);

                thus W is_Walk_from (v1,v2) by A11, A14, GLIB_001: 13;

              end;

            end;

            hence ex W be Walk of G1 st W is_Walk_from (v1,v2);

          end;

        end;

        hence ex W be Walk of G1 st W is_Walk_from (v1,v2);

      end;

      hence thesis;

    end;

    theorem :: GLIB_002:4

    for G1 be non _trivial connected _Graph, v be Vertex of G1, G2 be removeVertex of G1, v st v is endvertex holds G2 is connected by Lm5;

    theorem :: GLIB_002:5

    

     Th4: for G1 be connected _Graph, W be Walk of G1, e be set, G2 be removeEdge of G1, e st W is Cycle-like & e in (W .edges() ) holds G2 is connected

    proof

      let G1 be connected _Graph, W be Walk of G1, e be set, G2 be removeEdge of G1, e;

      assume that

       A1: W is Cycle-like and

       A2: e in (W .edges() );

      reconsider v1 = (( the_Source_of G1) . e), v2 = (( the_Target_of G1) . e) as Vertex of G1 by A2, FUNCT_2: 5;

      e Joins (v1,v2,G1) by A2, GLIB_000:def 13;

      then

      consider X be Walk of G1 such that

       A3: X is_Walk_from (v1,v2) and

       A4: not e in (X .edges() ) by A1, A2, GLIB_001: 157;

      reconsider X2 = X as Walk of G2 by A4, GLIB_001: 172;

      

       A5: X2 is_Walk_from (v1,v2) by A3, GLIB_001: 19;

      then

       A6: (X2 .reverse() ) is_Walk_from (v2,v1) by GLIB_001: 23;

      now

        let u,v be Vertex of G2;

        ( the_Vertices_of G2) c= ( the_Vertices_of G1);

        then

        reconsider u9 = u, v9 = v as Vertex of G1;

        consider C be Walk of G1 such that

         A7: C is_Walk_from (u9,v9) by Def1;

        set P = the Path of C;

        

         A8: P is_Walk_from (u9,v9) by A7, GLIB_001: 160;

        then

         A9: (P . ( len P)) = v by GLIB_001: 17;

        

         A10: (P . 1) = u by A8, GLIB_001: 17;

        now

          per cases ;

            suppose e in (P .edges() );

            then

            consider a,b be Vertex of G1, m be odd Element of NAT such that

             A11: (m + 2) <= ( len P) and

             A12: a = (P . m) and

             A13: e = (P . (m + 1)) and

             A14: b = (P . (m + 2)) and

             A15: e Joins (a,b,G1) by GLIB_001: 103;

            set P1 = (P .cut (1,m)), P2 = (P .cut ((m + 2),( len P)));

            

             A16: ((m + 2) - 2) < (( len P) - 0 ) by A11, XREAL_1: 15;

            then

             A17: (m + 1) <= ( len P) by NAT_1: 13;

            now

              assume e in (P1 .edges() );

              then

              consider x be even Element of NAT such that

               A18: 1 <= x and

               A19: x <= ( len P1) and

               A20: (P1 . x) = e by GLIB_001: 99;

              x <= m by A16, A19, GLIB_001: 45;

              then

               A21: x < (m + 1) by NAT_1: 13;

              x in ( dom P1) by A18, A19, FINSEQ_3: 25;

              then (P . x) = e by A16, A20, GLIB_001: 46;

              hence contradiction by A13, A17, A18, A21, GLIB_001: 138;

            end;

            then

            reconsider P19 = P1 as Walk of G2 by GLIB_001: 172;

            now

              assume e in (P2 .edges() );

              then

              consider x be even Element of NAT such that

               A22: 1 <= x and

               A23: x <= ( len P2) and

               A24: (P2 . x) = e by GLIB_001: 99;

              reconsider x1 = (x - 1) as odd Element of NAT by A22, INT_1: 5;

              

               A25: x1 < (( len P2) - 0 ) by A23, XREAL_1: 15;

              then ((m + 2) + x1) in ( dom P) by A11, GLIB_001: 36;

              then

               A26: ((m + 2) + x1) <= ( len P) by FINSEQ_3: 25;

              (x1 + 1) = x;

              then

               A27: e = (P . ((m + 2) + x1)) by A11, A24, A25, GLIB_001: 36;

              (m + 1) < ((m + 1) + 1) by NAT_1: 13;

              then

               A28: ((m + 1) + 0 ) < ((m + 2) + x1) by NAT_1: 2, XREAL_1: 8;

              1 <= (m + 1) by NAT_1: 12;

              hence contradiction by A13, A27, A26, A28, GLIB_001: 138;

            end;

            then

            reconsider P29 = P2 as Walk of G2 by GLIB_001: 172;

            reconsider a, b as Vertex of G2 by GLIB_000: 51;

            1 <= m by ABIAN: 12;

            then P1 is_Walk_from (u,a) by A10, A12, A16, GLIB_001: 37, JORDAN12: 2;

            then

             A29: P19 is_Walk_from (u,a) by GLIB_001: 19;

            P2 is_Walk_from (b,v) by A9, A11, A14, GLIB_001: 37;

            then

             A30: P29 is_Walk_from (b,v) by GLIB_001: 19;

            now

              per cases by A15, GLIB_000:def 13;

                suppose a = v1 & b = v2;

                then (P19 .append X2) is_Walk_from (u,b) by A5, A29, GLIB_001: 31;

                then ((P19 .append X2) .append P29) is_Walk_from (u,v) by A30, GLIB_001: 31;

                hence ex W be Walk of G2 st W is_Walk_from (u,v);

              end;

                suppose b = v1 & a = v2;

                then (P19 .append (X2 .reverse() )) is_Walk_from (u,b) by A6, A29, GLIB_001: 31;

                then ((P19 .append (X2 .reverse() )) .append P29) is_Walk_from (u,v) by A30, GLIB_001: 31;

                hence ex W be Walk of G2 st W is_Walk_from (u,v);

              end;

            end;

            hence ex W be Walk of G2 st W is_Walk_from (u,v);

          end;

            suppose not e in (P .edges() );

            then

            reconsider P as Walk of G2 by GLIB_001: 172;

            take P;

            thus P is_Walk_from (u,v) by A8, GLIB_001: 19;

          end;

        end;

        hence ex W be Walk of G2 st W is_Walk_from (u,v);

      end;

      hence thesis;

    end;

    theorem :: GLIB_002:6

    (ex v1 be Vertex of G st for v2 be Vertex of G holds ex W be Walk of G st W is_Walk_from (v1,v2)) implies G is connected by Lm6;

    theorem :: GLIB_002:7

    for G be _trivial _Graph holds G is connected;

    theorem :: GLIB_002:8

    

     Th7: G1 == G2 & G1 is connected implies G2 is connected

    proof

      assume that

       A1: G1 == G2 and

       A2: G1 is connected;

      now

        let u,v be Vertex of G2;

        reconsider u9 = u, v9 = v as Vertex of G1 by A1, GLIB_000:def 34;

        consider W9 be Walk of G1 such that

         A3: W9 is_Walk_from (u9,v9) by A2;

        reconsider W = W9 as Walk of G2 by A1, GLIB_001: 179;

        take W;

        thus W is_Walk_from (u,v) by A3, GLIB_001: 19;

      end;

      hence thesis;

    end;

    theorem :: GLIB_002:9

    v in (G .reachableFrom v) by Lm1;

    theorem :: GLIB_002:10

    for e,x,y be object holds x in (G .reachableFrom v1) & e Joins (x,y,G) implies y in (G .reachableFrom v1) by Lm2;

    theorem :: GLIB_002:11

    (G .edgesBetween (G .reachableFrom v)) = (G .edgesInOut (G .reachableFrom v))

    proof

      set R = (G .reachableFrom v);

      now

        let x be object;

        set Sx = (( the_Source_of G) . x), Tx = (( the_Target_of G) . x);

        assume

         A1: x in (G .edgesInOut R);

        then

        reconsider Sx, Tx as Vertex of G by FUNCT_2: 5;

        now

          per cases by A1, GLIB_000: 28;

            suppose

             A2: Sx in R;

            then

            consider W be Walk of G such that

             A3: W is_Walk_from (v,Sx) by Def5;

            now

              (W .last() ) = Sx by A3, GLIB_001:def 23;

              then

               A4: x Joins ((W .last() ),Tx,G) by A1, GLIB_000:def 13;

              assume

               A5: not Tx in R;

              (W .first() ) = v by A3, GLIB_001:def 23;

              then (W .addEdge x) is_Walk_from (v,Tx) by A4, GLIB_001: 63;

              hence contradiction by A5, Def5;

            end;

            then

             A6: x in (G .edgesInto R) by A1, GLIB_000:def 26;

            x in (G .edgesOutOf R) by A1, A2, GLIB_000:def 27;

            then x in ((G .edgesInto R) /\ (G .edgesOutOf R)) by A6, XBOOLE_0:def 4;

            hence x in (G .edgesBetween R) by GLIB_000:def 29;

          end;

            suppose

             A7: Tx in R;

            then

            consider W be Walk of G such that

             A8: W is_Walk_from (v,Tx) by Def5;

            now

              (W .last() ) = Tx by A8, GLIB_001:def 23;

              then

               A9: x Joins ((W .last() ),Sx,G) by A1, GLIB_000:def 13;

              assume

               A10: not Sx in R;

              (W .first() ) = v by A8, GLIB_001:def 23;

              then (W .addEdge x) is_Walk_from (v,Sx) by A9, GLIB_001: 63;

              hence contradiction by A10, Def5;

            end;

            then

             A11: x in (G .edgesOutOf R) by A1, GLIB_000:def 27;

            x in (G .edgesInto R) by A1, A7, GLIB_000:def 26;

            then x in ((G .edgesInto R) /\ (G .edgesOutOf R)) by A11, XBOOLE_0:def 4;

            hence x in (G .edgesBetween R) by GLIB_000:def 29;

          end;

        end;

        hence x in (G .edgesBetween R);

      end;

      then (G .edgesBetween R) c= (G .edgesInOut R) & (G .edgesInOut R) c= (G .edgesBetween R) by GLIB_000: 33;

      hence thesis by XBOOLE_0:def 10;

    end;

    theorem :: GLIB_002:12

    v1 in (G .reachableFrom v2) implies (G .reachableFrom v1) = (G .reachableFrom v2) by Lm3;

    theorem :: GLIB_002:13

    v in (W .vertices() ) implies (W .vertices() ) c= (G .reachableFrom v) by Lm4;

    theorem :: GLIB_002:14

    for G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2 st v1 = v2 holds (G2 .reachableFrom v2) c= (G1 .reachableFrom v1)

    proof

      let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2;

      assume

       A1: v1 = v2;

      let v be object;

      assume v in (G2 .reachableFrom v2);

      then

      consider W be Walk of G2 such that

       A2: W is_Walk_from (v2,v) by Def5;

      reconsider W2 = W as Walk of G1 by GLIB_001: 167;

      W2 is_Walk_from (v1,v) by A1, A2, GLIB_001: 19;

      hence thesis by Def5;

    end;

    theorem :: GLIB_002:15

    (ex v be Vertex of G st (G .reachableFrom v) = ( the_Vertices_of G)) implies G is connected by Lm7;

    theorem :: GLIB_002:16

    G is connected implies for v be Vertex of G holds (G .reachableFrom v) = ( the_Vertices_of G) by Lm8;

    theorem :: GLIB_002:17

    for v1 be Vertex of G1, v2 be Vertex of G2 st G1 == G2 & v1 = v2 holds (G1 .reachableFrom v1) = (G2 .reachableFrom v2) by Lm9;

    theorem :: GLIB_002:18

    v in (G .reachableDFrom v)

    proof

      (G .walkOf v) is_Walk_from (v,v) by GLIB_001: 13;

      hence thesis by Def6;

    end;

    theorem :: GLIB_002:19

    x in (G .reachableDFrom v1) & e DJoins (x,y,G) implies y in (G .reachableDFrom v1)

    proof

      set RFV = (G .reachableDFrom v1);

      assume that

       A1: x in RFV and

       A2: e DJoins (x,y,G);

      consider W be directed Walk of G such that

       A3: W is_Walk_from (v1,x) by A1, Def6;

      (W .addEdge e) is directed & (W .addEdge e) is_Walk_from (v1,y) by A2, A3, GLIB_001: 123;

      hence thesis by Def6;

    end;

    theorem :: GLIB_002:20

    (G .reachableDFrom v) c= (G .reachableFrom v)

    proof

      set RFD = (G .reachableDFrom v);

      let x be object;

      assume

       A1: x in RFD;

      then

      reconsider x9 = x as Vertex of G;

      ex W be directed Walk of G st W is_Walk_from (v,x9) by A1, Def6;

      hence thesis by Def5;

    end;

    theorem :: GLIB_002:21

    for G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2 st v1 = v2 holds (G2 .reachableDFrom v2) c= (G1 .reachableDFrom v1)

    proof

      let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2;

      assume

       A1: v1 = v2;

      let v be object;

      assume v in (G2 .reachableDFrom v2);

      then

      consider W be DWalk of G2 such that

       A2: W is_Walk_from (v2,v) by Def6;

      reconsider W as DWalk of G1 by GLIB_001: 175;

      W is_Walk_from (v1,v) by A1, A2, GLIB_001: 19;

      hence v in (G1 .reachableDFrom v1) by Def6;

    end;

    theorem :: GLIB_002:22

    for v1 be Vertex of G1, v2 be Vertex of G2 st G1 == G2 & v1 = v2 holds (G1 .reachableDFrom v1) = (G2 .reachableDFrom v2)

    proof

      let v1 be Vertex of G1, v2 be Vertex of G2;

      assume that

       A1: G1 == G2 and

       A2: v1 = v2;

      now

        let x be object;

        hereby

          assume x in (G1 .reachableDFrom v1);

          then

          consider W be DWalk of G1 such that

           A3: W is_Walk_from (v2,x) by A2, Def6;

          reconsider W2 = W as DWalk of G2 by A1, GLIB_001: 179, GLIB_001: 181;

          W2 is_Walk_from (v2,x) by A3, GLIB_001: 19;

          hence x in (G2 .reachableDFrom v2) by Def6;

        end;

        assume x in (G2 .reachableDFrom v2);

        then

        consider W be DWalk of G2 such that

         A4: W is_Walk_from (v1,x) by A2, Def6;

        reconsider W2 = W as DWalk of G1 by A1, GLIB_001: 179, GLIB_001: 181;

        W2 is_Walk_from (v1,x) by A4, GLIB_001: 19;

        hence x in (G1 .reachableDFrom v1) by Def6;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLIB_002:23

    for G1 be _Graph, G2 be connected Subgraph of G1 holds G2 is spanning implies G1 is connected by Lm10;

    theorem :: GLIB_002:24

    ( union (G .componentSet() )) = ( the_Vertices_of G)

    proof

      now

        let x be object;

        thus x in ( union (G .componentSet() )) implies x in ( the_Vertices_of G);

        assume x in ( the_Vertices_of G);

        then

        reconsider x9 = x as Vertex of G;

        set Y = (G .reachableFrom x9);

        x in Y & Y in (G .componentSet() ) by Def8, Lm1;

        hence x in ( union (G .componentSet() )) by TARSKI:def 4;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLIB_002:25

    G is connected iff (G .componentSet() ) = {( the_Vertices_of G)} by Lm11;

    theorem :: GLIB_002:26

    G1 == G2 implies (G1 .componentSet() ) = (G2 .componentSet() ) by Lm12;

    theorem :: GLIB_002:27

    x in (G .componentSet() ) implies x is non empty Subset of ( the_Vertices_of G) by Lm13;

    theorem :: GLIB_002:28

    G is connected iff (G .numComponents() ) = 1 by Lm18;

    theorem :: GLIB_002:29

    G1 == G2 implies (G1 .numComponents() ) = (G2 .numComponents() ) by Lm12;

    theorem :: GLIB_002:30

    G is Component of G iff G is connected

    proof

      thus G is Component of G implies G is connected;

      

       A1: G is Subgraph of G by GLIB_000: 40;

       A2:

      now

        given G2 be connected Subgraph of G such that

         A3: G c< G2;

        now

          per cases by A1, A3, GLIB_000: 98;

            suppose ( the_Vertices_of G) c< ( the_Vertices_of G2);

            hence contradiction by XBOOLE_0:def 8;

          end;

            suppose ( the_Edges_of G) c< ( the_Edges_of G2);

            hence contradiction by XBOOLE_0:def 8;

          end;

        end;

        hence contradiction;

      end;

      assume G is connected;

      hence thesis by A2, Def7, GLIB_000: 40;

    end;

    theorem :: GLIB_002:31

    for C be Component of G holds ( the_Edges_of C) = (G .edgesBetween ( the_Vertices_of C)) by Lm14;

    theorem :: GLIB_002:32

    for C1,C2 be Component of G holds ( the_Vertices_of C1) = ( the_Vertices_of C2) iff C1 == C2 by Lm15;

    theorem :: GLIB_002:33

    for C be Component of G, v be Vertex of G holds v in ( the_Vertices_of C) iff ( the_Vertices_of C) = (G .reachableFrom v) by Lm16;

    theorem :: GLIB_002:34

    for C1,C2 be Component of G, v be set st v in ( the_Vertices_of C1) & v in ( the_Vertices_of C2) holds C1 == C2 by Lm17;

    theorem :: GLIB_002:35

    for G be connected _Graph, v be Vertex of G holds v is non cut-vertex iff for G2 be removeVertex of G, v holds (G2 .numComponents() ) c= (G .numComponents() ) by Lm19;

    theorem :: GLIB_002:36

    for G be connected _Graph, v be Vertex of G, G2 be removeVertex of G, v st not v is cut-vertex holds G2 is connected by Lm20;

    theorem :: GLIB_002:37

    for G be non _trivial _finite connected _Graph holds ex v1,v2 be Vertex of G st v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex by Lm21;

    theorem :: GLIB_002:38

    

     Th37: v is cut-vertex implies G is non _trivial

    proof

      assume

       A1: v is cut-vertex;

      now

        assume G is _trivial;

        then

        reconsider G9 = G as _trivial _Graph;

        set G2 = the removeVertex of G9, v;

        (G9 .numComponents() ) = 1 & (G2 .numComponents() ) = 1 by Lm18;

        then 1 in 1 by A1;

        hence contradiction;

      end;

      hence thesis;

    end;

    theorem :: GLIB_002:39

    for v1 be Vertex of G1, v2 be Vertex of G2 st G1 == G2 & v1 = v2 holds v1 is cut-vertex implies v2 is cut-vertex

    proof

      let v1 be Vertex of G1, v2 be Vertex of G2;

      assume that

       A1: G1 == G2 and

       A2: v1 = v2 and

       A3: v1 is cut-vertex;

      

       A4: G1 is non _trivial by A3, Th37;

      then

       A5: G2 is non _trivial by A1, GLIB_000: 89;

      let G2A be removeVertex of G2, v2;

      set G1A = the removeVertex of G1, v1;

      (G1 .numComponents() ) = (G2 .numComponents() ) by A1, Lm12;

      then

       A6: (G2 .numComponents() ) in (G1A .numComponents() ) by A3;

      ( the_Vertices_of G1A) = (( the_Vertices_of G1) \ {v2}) by A2, A4, GLIB_000: 47

      .= (( the_Vertices_of G2) \ {v2}) by A1, GLIB_000:def 34;

      then

       A7: ( the_Vertices_of G2A) = ( the_Vertices_of G1A) by A5, GLIB_000: 47;

      G2 is Subgraph of G1 by A1, GLIB_000: 87;

      then

       A8: G2A is Subgraph of G1 by GLIB_000: 43;

      ( the_Edges_of G1A) = (G1 .edgesBetween (( the_Vertices_of G1) \ {v1})) by A4, GLIB_000: 47

      .= (G1 .edgesBetween (( the_Vertices_of G2) \ {v2})) by A1, A2, GLIB_000:def 34

      .= (G2 .edgesBetween (( the_Vertices_of G2) \ {v2})) by A1, GLIB_000: 90;

      then ( the_Edges_of G2A) = ( the_Edges_of G1A) by A5, GLIB_000: 47;

      hence thesis by A6, A7, A8, Lm12, GLIB_000: 86;

    end;

    theorem :: GLIB_002:40

    

     Th39: for G be _finite connected _Graph holds (G .order() ) <= ((G .size() ) + 1)

    proof

      let G be _finite connected _Graph;

      defpred P[ _finite _Graph] means $1 is connected implies ($1 .order() ) <= (($1 .size() ) + 1);

       A1:

      now

        let k be non zero Nat;

        assume

         A2: for Gk be _finite _Graph st (Gk .order() ) = k holds P[Gk];

        let Gk1 be _finite _Graph;

        assume

         A3: (Gk1 .order() ) = (k + 1);

        now

           A4:

          now

            assume (Gk1 .order() ) = 1;

            then (k + 1) = ( 0 + 1) by A3;

            hence contradiction;

          end;

          assume Gk1 is connected;

          then

          reconsider Gk19 = Gk1 as non _trivial _finite connected _Graph by A4, GLIB_000: 26;

          consider v1,v2 be Vertex of Gk19 such that v1 <> v2 and

           A5: not v1 is cut-vertex and not v2 is cut-vertex by Lm21;

          set Gkb = the removeVertex of Gk19, v1;

          

           A6: ((Gkb .order() ) + 1) = (k + 1) & ((Gkb .size() ) + ( card (v1 .edgesInOut() ))) = (Gk1 .size() ) by A3, GLIB_000: 48;

           not v1 is isolated by Th1;

          then (v1 .edgesInOut() ) <> {} by GLIB_000:def 49;

          then 0 < ( card (v1 .edgesInOut() )) by NAT_1: 3;

          then

           A7: ( 0 + 1) <= ( card (v1 .edgesInOut() )) by NAT_1: 13;

          Gkb is connected by A5, Lm20;

          then k <= (((Gk1 .size() ) - ( card (v1 .edgesInOut() ))) + 1) by A2, A6;

          then (k + 1) <= ((((Gk1 .size() ) + 1) - ( card (v1 .edgesInOut() ))) + ( card (v1 .edgesInOut() ))) by A7, XREAL_1: 7;

          hence (Gk1 .order() ) <= ((Gk1 .size() ) + 1) by A3;

        end;

        hence P[Gk1];

      end;

      

       A8: for G be _finite _Graph st (G .order() ) = 1 holds P[G] by NAT_1: 12;

      for G be _finite _Graph holds P[G] from GLIB_000:sch 1( A8, A1);

      hence thesis;

    end;

    theorem :: GLIB_002:41

    for G be acyclic _Graph holds G is simple;

    theorem :: GLIB_002:42

    for G be acyclic _Graph, W be Path of G, e be set st not e in (W .edges() ) & e in ((W .last() ) .edgesInOut() ) holds (W .addEdge e) is Path-like by Lm22;

    theorem :: GLIB_002:43

    for G be non _trivial _finite acyclic _Graph st ( the_Edges_of G) <> {} holds ex v1,v2 be Vertex of G st v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in (G .reachableFrom v1) by Lm23;

    theorem :: GLIB_002:44

    

     Th43: G1 == G2 & G1 is acyclic implies G2 is acyclic

    proof

      assume that

       A1: G1 == G2 and

       A2: G1 is acyclic;

      reconsider G19 = G1 as acyclic _Graph by A2;

      G2 is Subgraph of G19 by A1, GLIB_000: 87;

      hence thesis;

    end;

    theorem :: GLIB_002:45

    for G be non _trivial _finite Tree-like _Graph holds ex v1,v2 be Vertex of G st v1 <> v2 & v1 is endvertex & v2 is endvertex by Lm24;

    theorem :: GLIB_002:46

    

     Th45: for G be _finite _Graph holds G is Tree-like iff G is acyclic & (G .order() ) = ((G .size() ) + 1)

    proof

      defpred P[ Nat] means for G be _finite acyclic _Graph st (G .order() ) = $1 & (G .order() ) = ((G .size() ) + 1) holds G is connected;

      let G be _finite _Graph;

      hereby

        defpred P[ Nat] means for T be _finite Tree-like _Graph st (T .order() ) = $1 holds $1 = ((T .size() ) + 1);

        assume

         A1: G is Tree-like;

        hence G is acyclic;

        now

          let T be _finite Tree-like _Graph;

          set VT = ( the_Vertices_of T), ET = ( the_Edges_of T);

          assume (T .order() ) = 1;

          then ( card VT) = 1 by GLIB_000:def 24;

          then

          consider v be object such that

           A2: VT = {v} by CARD_2: 42;

          reconsider v as Vertex of T by A2, TARSKI:def 1;

          now

            given e be object such that

             A3: e in ET;

            (( the_Target_of T) . e) in {v} by A2, A3, FUNCT_2: 5;

            then

             A4: (( the_Target_of T) . e) = v by TARSKI:def 1;

            (( the_Source_of T) . e) in {v} by A2, A3, FUNCT_2: 5;

            then (( the_Source_of T) . e) = v by TARSKI:def 1;

            then e Joins (v,v,T) by A3, A4, GLIB_000:def 13;

            then (T .walkOf (v,e,v)) is Cycle-like by GLIB_001: 156;

            hence contradiction by Def2;

          end;

          then ( card ET) = 0 by CARD_1: 27, XBOOLE_0:def 1;

          then (T .size() ) = 0 by GLIB_000:def 25;

          hence 1 = ((T .size() ) + 1);

        end;

        then

         A5: P[1];

        now

          let k be non zero Nat;

          assume

           A6: for T be _finite Tree-like _Graph st (T .order() ) = k holds k = ((T .size() ) + 1);

          let T be _finite Tree-like _Graph;

          assume

           A7: (T .order() ) = (k + 1);

          then (T .order() ) <> 1 by XCMPLX_1: 3;

          then

          reconsider aT = T as non _trivial _finite Tree-like _Graph by GLIB_000: 26;

          set v = the endvertex Vertex of aT;

          set T2 = the removeVertex of aT, v;

          (((T2 .order() ) + 1) - 1) = ((k + 1) - 1) by A7, GLIB_000: 48;

          then

           A8: k = ((T2 .size() ) + 1) by A6;

          ( card (v .edgesInOut() )) = (v .degree() ) by GLIB_000: 19

          .= 1 by GLIB_000:def 52;

          hence (k + 1) = ((T .size() ) + 1) by A8, GLIB_000: 48;

        end;

        then

         A9: for k be non zero Nat st P[k] holds P[(k + 1)];

        for k be non zero Nat holds P[k] from NAT_1:sch 10( A5, A9);

        hence (G .order() ) = ((G .size() ) + 1) by A1;

      end;

      assume that

       A10: G is acyclic and

       A11: (G .order() ) = ((G .size() ) + 1);

      now

        let k be non zero Element of NAT ;

        assume

         A12: for G be _finite acyclic _Graph st (G .order() ) = k & (G .order() ) = ((G .size() ) + 1) holds G is connected;

        let G be _finite acyclic _Graph;

        assume that

         A13: (G .order() ) = (k + 1) and

         A14: (G .order() ) = ((G .size() ) + 1);

        now

          assume (G .order() ) = 1;

          then ( 0 + 1) = (k + 1) by A13;

          hence contradiction;

        end;

        then

        reconsider aG = G as non _trivial _finite acyclic _Graph by GLIB_000: 26;

        ( the_Edges_of G) <> {} by A13, A14, CARD_1: 27, GLIB_000:def 25;

        then

        consider v,v2 be Vertex of aG such that v <> v2 and

         A15: v is endvertex and v2 is endvertex and v2 in (aG .reachableFrom v) by Lm23;

        set G2 = the removeVertex of G, v;

        

         A16: ((G2 .order() ) + 1) = (aG .order() ) & ((G2 .size() ) + ( card (v .edgesInOut() ))) = (aG .size() ) by GLIB_000: 48;

        ( card (v .edgesInOut() )) = (v .degree() ) by GLIB_000: 19

        .= 1 by A15, GLIB_000:def 52;

        then

         A17: G2 is connected by A12, A13, A14, A16;

        consider e be object such that

         A18: (v .edgesInOut() ) = {e} and

         A19: not e Joins (v,v,G) by A15, GLIB_000:def 51;

        e in (v .edgesInOut() ) by A18, TARSKI:def 1;

        hence G is connected by A17, A19, Th2;

      end;

      then

       A20: for k be non zero Nat st P[k] holds P[(k + 1)];

      now

        let G be _finite acyclic _Graph;

        assume that

         A21: (G .order() ) = 1 and (G .order() ) = ((G .size() ) + 1);

        consider v be Vertex of G such that

         A22: ( the_Vertices_of G) = {v} by A21, GLIB_000: 27;

        now

          let v1,v2 be Vertex of G;

          v1 = v & v2 = v by A22, TARSKI:def 1;

          then (G .walkOf v) is_Walk_from (v1,v2) by GLIB_001: 13;

          hence ex W be Walk of G st W is_Walk_from (v1,v2);

        end;

        hence G is connected;

      end;

      then

       A23: P[1];

      for k be non zero Nat holds P[k] from NAT_1:sch 10( A23, A20);

      then G is connected by A10, A11;

      hence thesis by A10;

    end;

    theorem :: GLIB_002:47

    for G be _finite _Graph holds G is Tree-like iff G is connected & (G .order() ) = ((G .size() ) + 1)

    proof

      let G be _finite _Graph;

      thus G is Tree-like implies G is connected & (G .order() ) = ((G .size() ) + 1) by Th45;

      assume that

       A1: G is connected and

       A2: (G .order() ) = ((G .size() ) + 1);

      now

        assume not G is acyclic;

        then

        consider W be Walk of G such that

         A3: W is Cycle-like;

        set e = the Element of (W .edges() );

        set G2 = the removeEdge of G, e;

        

         A4: (W .edges() ) <> {} by A3, GLIB_001: 136;

        then e in (W .edges() );

        then

         A5: (G2 .order() ) = (G .order() ) & ((G2 .size() ) + 1) = (G .size() ) by GLIB_000: 52;

        G2 is connected by A1, A3, A4, Th4;

        then (((G2 .size() ) + 1) + 1) <= (((G2 .size() ) + 1) + 0 ) by A2, A5, Th39;

        hence contradiction by XREAL_1: 6;

      end;

      hence thesis by A1;

    end;

    theorem :: GLIB_002:48

    

     Th47: G1 == G2 & G1 is Tree-like implies G2 is Tree-like by Th7, Th43;

    theorem :: GLIB_002:49

    G is_DTree_rooted_at x implies x is Vertex of G

    proof

      set v = the Vertex of G;

      assume G is_DTree_rooted_at x;

      then ex W be DWalk of G st W is_Walk_from (x,v);

      hence thesis by GLIB_001: 18;

    end;

    theorem :: GLIB_002:50

    G1 == G2 & G1 is_DTree_rooted_at x implies G2 is_DTree_rooted_at x

    proof

      assume that

       A1: G1 == G2 and

       A2: G1 is_DTree_rooted_at x;

       A3:

      now

        let y be Vertex of G2;

        reconsider y9 = y as Vertex of G1 by A1, GLIB_000:def 34;

        consider W be DWalk of G1 such that

         A4: W is_Walk_from (x,y9) by A2;

        reconsider W9 = W as DWalk of G2 by A1, GLIB_001: 179, GLIB_001: 181;

        take W9;

        thus W9 is_Walk_from (x,y) by A4, GLIB_001: 19;

      end;

      G1 is Tree-like by A2;

      then G2 is Tree-like by A1, Th47;

      hence thesis by A3;

    end;