graph_3a.miz



    begin

    definition

      :: GRAPH_3A:def1

      func KVertices -> set equals { 0 , 1, 2, 3};

      correctness ;

      :: GRAPH_3A:def2

      func KEdges -> set equals {10, 20, 30, 40, 50, 60, 70};

      correctness ;

    end

    definition

      :: GRAPH_3A:def3

      func KSource -> Function of KEdges , KVertices equals { [10, 0 ], [20, 0 ], [30, 0 ], [40, 1], [50, 1], [60, 2], [70, 2]};

      correctness

      proof

        set K = { [10, 0 ], [20, 0 ], [30, 0 ], [40, 1], [50, 1], [60, 2], [70, 2]};

        K c= [: KEdges , KVertices :]

        proof

          let x be object;

          assume x in K;

          then

           x: x = [10, 0 ] or x = [20, 0 ] or x = [30, 0 ] or x = [40, 1] or x = [50, 1] or x = [60, 2] or x = [70, 2] by ENUMSET1:def 5;

          10 in KEdges & 20 in KEdges & 30 in KEdges & 40 in KEdges & 50 in KEdges & 60 in KEdges & 70 in KEdges & 0 in KVertices & 1 in KVertices & 2 in KVertices & 3 in KVertices by ENUMSET1:def 2, ENUMSET1:def 5;

          hence x in [: KEdges , KVertices :] by x, ZFMISC_1: 87;

        end;

        then

        reconsider K as Relation of KEdges , KVertices ;

        K is Function-like

        proof

          let x,y1,y2 be object;

          assume [x, y1] in K & [x, y2] in K;

          then ( [x, y1] = [10, 0 ] or [x, y1] = [20, 0 ] or [x, y1] = [30, 0 ] or [x, y1] = [40, 1] or [x, y1] = [50, 1] or [x, y1] = [60, 2] or [x, y1] = [70, 2]) & ( [x, y2] = [10, 0 ] or [x, y2] = [20, 0 ] or [x, y2] = [30, 0 ] or [x, y2] = [40, 1] or [x, y2] = [50, 1] or [x, y2] = [60, 2] or [x, y2] = [70, 2]) by ENUMSET1:def 5;

          then (x = 10 & y1 = 0 or x = 20 & y1 = 0 or x = 30 & y1 = 0 or x = 40 & y1 = 1 or x = 50 & y1 = 1 or x = 60 & y1 = 2 or x = 70 & y1 = 2) & (x = 10 & y2 = 0 or x = 20 & y2 = 0 or x = 30 & y2 = 0 or x = 40 & y2 = 1 or x = 50 & y2 = 1 or x = 60 & y2 = 2 or x = 70 & y2 = 2) by XTUPLE_0: 1;

          hence y1 = y2;

        end;

        then

        reconsider K as PartFunc of KEdges , KVertices ;

        ( dom K) = KEdges

        proof

          thus ( dom K) c= KEdges ;

          let o be object;

          assume o in KEdges ;

          then

           o: o = 10 or o = 20 or o = 30 or o = 40 or o = 50 or o = 60 or o = 70 by ENUMSET1:def 5;

           [10, 0 ] in K & [20, 0 ] in K & [30, 0 ] in K & [40, 1] in K & [50, 1] in K & [60, 2] in K & [70, 2] in K by ENUMSET1:def 5;

          hence o in ( dom K) by o, XTUPLE_0:def 12;

        end;

        then K is quasi_total by FUNCT_2:def 1;

        hence thesis;

      end;

      :: GRAPH_3A:def4

      func KTarget -> Function of KEdges , KVertices equals { [10, 1], [20, 2], [30, 3], [40, 2], [50, 2], [60, 3], [70, 3]};

      correctness

      proof

        set K = { [10, 1], [20, 2], [30, 3], [40, 2], [50, 2], [60, 3], [70, 3]};

        K c= [: KEdges , KVertices :]

        proof

          let x be object;

          assume x in K;

          then

           x: x = [10, 1] or x = [20, 2] or x = [30, 3] or x = [40, 2] or x = [50, 2] or x = [60, 3] or x = [70, 3] by ENUMSET1:def 5;

          10 in KEdges & 20 in KEdges & 30 in KEdges & 40 in KEdges & 50 in KEdges & 60 in KEdges & 70 in KEdges & 0 in KVertices & 1 in KVertices & 2 in KVertices & 3 in KVertices by ENUMSET1:def 2, ENUMSET1:def 5;

          hence x in [: KEdges , KVertices :] by x, ZFMISC_1: 87;

        end;

        then

        reconsider K as Relation of KEdges , KVertices ;

        K is Function-like

        proof

          let x,y1,y2 be object;

          assume [x, y1] in K & [x, y2] in K;

          then ( [x, y1] = [10, 1] or [x, y1] = [20, 2] or [x, y1] = [30, 3] or [x, y1] = [40, 2] or [x, y1] = [50, 2] or [x, y1] = [60, 3] or [x, y1] = [70, 3]) & ( [x, y2] = [10, 1] or [x, y2] = [20, 2] or [x, y2] = [30, 3] or [x, y2] = [40, 2] or [x, y2] = [50, 2] or [x, y2] = [60, 3] or [x, y2] = [70, 3]) by ENUMSET1:def 5;

          then (x = 10 & y1 = 1 or x = 20 & y1 = 2 or x = 30 & y1 = 3 or x = 40 & y1 = 2 or x = 50 & y1 = 2 or x = 60 & y1 = 3 or x = 70 & y1 = 3) & (x = 10 & y2 = 1 or x = 20 & y2 = 2 or x = 30 & y2 = 3 or x = 40 & y2 = 2 or x = 50 & y2 = 2 or x = 60 & y2 = 3 or x = 70 & y2 = 3) by XTUPLE_0: 1;

          hence y1 = y2;

        end;

        then

        reconsider K as PartFunc of KEdges , KVertices ;

        ( dom K) = KEdges

        proof

          thus ( dom K) c= KEdges ;

          let o be object;

          assume o in KEdges ;

          then

           o: o = 10 or o = 20 or o = 30 or o = 40 or o = 50 or o = 60 or o = 70 by ENUMSET1:def 5;

           [10, 1] in K & [20, 2] in K & [30, 3] in K & [40, 2] in K & [50, 2] in K & [60, 3] in K & [70, 3] in K by ENUMSET1:def 5;

          hence o in ( dom K) by o, XTUPLE_0:def 12;

        end;

        then K is quasi_total by FUNCT_2:def 1;

        hence thesis;

      end;

    end

    definition

      :: GRAPH_3A:def5

      func KoenigsbergBridges -> Graph equals MultiGraphStruct (# KVertices , KEdges , KSource , KTarget #);

      correctness ;

    end

    registration

      cluster KoenigsbergBridges -> finite connected;

      correctness

      proof

        for g1,g2 be Vertex of KoenigsbergBridges st g1 <> g2 holds ex c be Chain of KoenigsbergBridges , vs be FinSequence of the carrier of KoenigsbergBridges st c is non empty & vs is_vertex_seq_of c & (vs . 1) = g1 & (vs . ( len vs)) = g2

        proof

          let g1,g2 be Vertex of KoenigsbergBridges ;

          assume

           g: g1 <> g2;

          per cases by ENUMSET1:def 2;

            suppose g1 = 0 & g2 = 0 ;

            hence thesis by g;

          end;

            suppose

             gg: g1 = 0 & g2 = 1;

            10 in KEdges by ENUMSET1:def 5;

            then

            reconsider c = <*10*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            take c;

            reconsider vs = <*g1, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            take vs;

            thus c is non empty;

            

             l: ( len c) = 1 & (c . 1) = 10 by FINSEQ_1: 40;

            

             lv: ( len vs) = 2 by FINSEQ_1: 44;

            thus vs is_vertex_seq_of c

            proof

              thus ( len vs) = (( len c) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len c);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (c . n) = 10 by l;

              ( dom vs) = ( Seg 2) by lv, FINSEQ_1:def 3;

              then ( dom vs) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs) & 2 in ( dom vs) by TARSKI:def 2;

              

               v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

              .= g1 by n, FINSEQ_1: 44;

              

               v2: (vs /. (n + 1)) = (vs . 2) by d, n, PARTFUN1:def 6

              .= g2 by FINSEQ_1: 44;

               [10, 0 ] in KSource & [10, 1] in KTarget by ENUMSET1:def 5;

              then ( KSource . (c . n)) = g1 & ( KTarget . (c . n)) = g2 by cn, gg, FUNCT_1: 1;

              hence (c . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

            end;

            thus (vs . 1) = g1 & (vs . ( len vs)) = g2 by lv, FINSEQ_1: 44;

          end;

            suppose

             gg: g1 = 0 & g2 = 2;

            20 in KEdges by ENUMSET1:def 5;

            then

            reconsider c = <*20*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            take c;

            reconsider vs = <*g1, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            take vs;

            thus c is non empty;

            

             l: ( len c) = 1 & (c . 1) = 20 by FINSEQ_1: 40;

            

             lv: ( len vs) = 2 by FINSEQ_1: 44;

            thus vs is_vertex_seq_of c

            proof

              thus ( len vs) = (( len c) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len c);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (c . n) = 20 by l;

              ( dom vs) = ( Seg 2) by lv, FINSEQ_1:def 3;

              then ( dom vs) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs) & 2 in ( dom vs) by TARSKI:def 2;

              

               v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

              .= g1 by n, FINSEQ_1: 44;

              

               v2: (vs /. (n + 1)) = (vs . 2) by d, n, PARTFUN1:def 6

              .= g2 by FINSEQ_1: 44;

               [20, 0 ] in KSource & [20, 2] in KTarget by ENUMSET1:def 5;

              then ( KSource . (c . n)) = g1 & ( KTarget . (c . n)) = g2 by cn, gg, FUNCT_1: 1;

              hence (c . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

            end;

            thus (vs . 1) = g1 & (vs . ( len vs)) = g2 by lv, FINSEQ_1: 44;

          end;

            suppose

             gg: g1 = 0 & g2 = 3;

            30 in KEdges by ENUMSET1:def 5;

            then

            reconsider c = <*30*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            take c;

            reconsider vs = <*g1, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            take vs;

            thus c is non empty;

            

             l: ( len c) = 1 & (c . 1) = 30 by FINSEQ_1: 40;

            

             lv: ( len vs) = 2 by FINSEQ_1: 44;

            thus vs is_vertex_seq_of c

            proof

              thus ( len vs) = (( len c) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len c);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (c . n) = 30 by l;

              ( dom vs) = ( Seg 2) by lv, FINSEQ_1:def 3;

              then ( dom vs) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs) & 2 in ( dom vs) by TARSKI:def 2;

              

               v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

              .= g1 by n, FINSEQ_1: 44;

              

               v2: (vs /. (n + 1)) = (vs . 2) by d, n, PARTFUN1:def 6

              .= g2 by FINSEQ_1: 44;

               [30, 0 ] in KSource & [30, 3] in KTarget by ENUMSET1:def 5;

              then ( KSource . (c . n)) = g1 & ( KTarget . (c . n)) = g2 by cn, gg, FUNCT_1: 1;

              hence (c . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

            end;

            thus (vs . 1) = g1 & (vs . ( len vs)) = g2 by lv, FINSEQ_1: 44;

          end;

            suppose

             gg: g1 = 1 & g2 = 0 ;

            10 in KEdges by ENUMSET1:def 5;

            then

            reconsider c = <*10*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            take c;

            reconsider vs = <*g1, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            take vs;

            thus c is non empty;

            

             l: ( len c) = 1 & (c . 1) = 10 by FINSEQ_1: 40;

            

             lv: ( len vs) = 2 by FINSEQ_1: 44;

            thus vs is_vertex_seq_of c

            proof

              thus ( len vs) = (( len c) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len c);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (c . n) = 10 by l;

              ( dom vs) = ( Seg 2) by lv, FINSEQ_1:def 3;

              then ( dom vs) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs) & 2 in ( dom vs) by TARSKI:def 2;

              

               v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

              .= g1 by n, FINSEQ_1: 44;

              

               v2: (vs /. (n + 1)) = (vs . 2) by d, n, PARTFUN1:def 6

              .= g2 by FINSEQ_1: 44;

               [10, 0 ] in KSource & [10, 1] in KTarget by ENUMSET1:def 5;

              then ( KSource . (c . n)) = g2 & ( KTarget . (c . n)) = g1 by cn, gg, FUNCT_1: 1;

              hence (c . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

            end;

            thus (vs . 1) = g1 & (vs . ( len vs)) = g2 by lv, FINSEQ_1: 44;

          end;

            suppose g1 = 1 & g2 = 1;

            hence thesis by g;

          end;

            suppose

             gg: g1 = 1 & g2 = 2;

            40 in KEdges by ENUMSET1:def 5;

            then

            reconsider c = <*40*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            take c;

            reconsider vs = <*g1, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            take vs;

            thus c is non empty;

            

             l: ( len c) = 1 & (c . 1) = 40 by FINSEQ_1: 40;

            

             lv: ( len vs) = 2 by FINSEQ_1: 44;

            thus vs is_vertex_seq_of c

            proof

              thus ( len vs) = (( len c) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len c);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (c . n) = 40 by l;

              ( dom vs) = ( Seg 2) by lv, FINSEQ_1:def 3;

              then ( dom vs) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs) & 2 in ( dom vs) by TARSKI:def 2;

              

               v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

              .= g1 by n, FINSEQ_1: 44;

              

               v2: (vs /. (n + 1)) = (vs . 2) by d, n, PARTFUN1:def 6

              .= g2 by FINSEQ_1: 44;

               [40, 1] in KSource & [40, 2] in KTarget by ENUMSET1:def 5;

              then ( KSource . (c . n)) = g1 & ( KTarget . (c . n)) = g2 by cn, gg, FUNCT_1: 1;

              hence (c . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

            end;

            thus (vs . 1) = g1 & (vs . ( len vs)) = g2 by lv, FINSEQ_1: 44;

          end;

            suppose

             gg: g1 = 1 & g2 = 3;

            reconsider g3 = 2 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;

            40 in KEdges by ENUMSET1:def 5;

            then

            reconsider c = <*40*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            60 in KEdges by ENUMSET1:def 5;

            then

            reconsider d = <*60*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            reconsider vs1 = <*g1, g3*> as FinSequence of the carrier of KoenigsbergBridges ;

            

             l: ( len c) = 1 & (c . 1) = 40 by FINSEQ_1: 40;

            

             lv1: ( len vs1) = 2 by FINSEQ_1: 44;

            

             vs1: vs1 is_vertex_seq_of c

            proof

              thus ( len vs1) = (( len c) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len c);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (c . n) = 40 by l;

              ( dom vs1) = ( Seg 2) by lv1, FINSEQ_1:def 3;

              then ( dom vs1) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs1) & 2 in ( dom vs1) by TARSKI:def 2;

              

               v1: (vs1 /. n) = (vs1 . n) by d, n, PARTFUN1:def 6

              .= g1 by n, FINSEQ_1: 44;

              

               v2: (vs1 /. (n + 1)) = (vs1 . 2) by d, n, PARTFUN1:def 6

              .= g3 by FINSEQ_1: 44;

               [40, 1] in KSource & [40, 2] in KTarget by ENUMSET1:def 5;

              then ( KSource . (c . n)) = g1 & ( KTarget . (c . n)) = g3 by cn, gg, FUNCT_1: 1;

              hence (c . n) joins ((vs1 /. n),(vs1 /. (n + 1))) by v1, v2;

            end;

            reconsider vs2 = <*g3, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            

             l: ( len d) = 1 & (d . 1) = 60 by FINSEQ_1: 40;

            

             lv: ( len vs2) = 2 by FINSEQ_1: 44;

            

             vs2: vs2 is_vertex_seq_of d

            proof

              thus ( len vs2) = (( len d) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len d);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (d . n) = 60 by l;

              ( dom vs2) = ( Seg 2) by lv, FINSEQ_1:def 3;

              then ( dom vs2) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs2) & 2 in ( dom vs2) by TARSKI:def 2;

              

               v1: (vs2 /. n) = (vs2 . n) by d, n, PARTFUN1:def 6

              .= g3 by n, FINSEQ_1: 44;

              

               v2: (vs2 /. (n + 1)) = (vs2 . 2) by d, n, PARTFUN1:def 6

              .= g2 by FINSEQ_1: 44;

               [60, 2] in KSource & [60, 3] in KTarget by ENUMSET1:def 5;

              then ( KSource . (d . n)) = g3 & ( KTarget . (d . n)) = g2 by cn, gg, FUNCT_1: 1;

              hence (d . n) joins ((vs2 /. n),(vs2 /. (n + 1))) by v1, v2;

            end;

            ( rng c) = {40} & ( rng d) = {60} by FINSEQ_1: 38;

            then

             r: ( rng c) misses ( rng d) by ZFMISC_1: 11;

            (vs1 . ( len vs1)) = g3 by lv1, FINSEQ_1: 44

            .= (vs2 . 1) by FINSEQ_1: 44;

            then

            reconsider cd = (c ^ d) as Path of KoenigsbergBridges by vs1, vs2, r, GRAPH_3: 6;

            take cd;

            reconsider vs = <*g1, g3, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            take vs;

            thus cd is non empty;

            cd = <*40, 60*>;

            then

             l: ( len cd) = 2 & (cd . 1) = 40 & (cd . 2) = 60 by FINSEQ_1: 44;

            

             lv: ( len vs) = 3 by FINSEQ_1: 45;

            thus vs is_vertex_seq_of cd

            proof

              thus ( len vs) = (( len cd) + 1) by l, FINSEQ_1: 45;

              let n be Nat;

              assume 1 <= n & n <= ( len cd);

              then 1 <= n & n <= (1 + 1) by l;

              then n = (1 + 0 ) or ... or n = (1 + 1) by NAT_1: 62;

              then n = 1 or n = 2;

              per cases ;

                suppose

                 n: n = 1;

                then

                 cn: (cd . n) = 40 by l;

                ( dom vs) = ( Seg 3) by lv, FINSEQ_1:def 3;

                then ( dom vs) = {1, 2, 3} by FINSEQ_3: 1;

                then

                 d: 1 in ( dom vs) & 2 in ( dom vs) by ENUMSET1:def 1;

                

                 v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

                .= g1 by n, FINSEQ_1: 45;

                

                 v2: (vs /. (n + 1)) = (vs . 2) by d, n, PARTFUN1:def 6

                .= g3 by FINSEQ_1: 45;

                 [40, 1] in KSource & [40, 2] in KTarget by ENUMSET1:def 5;

                then ( KSource . (cd . n)) = g1 & ( KTarget . (cd . n)) = g3 by cn, gg, FUNCT_1: 1;

                hence (cd . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

              end;

                suppose

                 n: n = 2;

                then

                 cn: (cd . n) = 60 by l;

                ( dom vs) = ( Seg 3) by lv, FINSEQ_1:def 3;

                then ( dom vs) = {1, 2, 3} by FINSEQ_3: 1;

                then

                 d: 2 in ( dom vs) & 3 in ( dom vs) by ENUMSET1:def 1;

                

                 v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

                .= g3 by n, FINSEQ_1: 45;

                

                 v2: (vs /. (n + 1)) = (vs . 3) by d, n, PARTFUN1:def 6

                .= g2 by FINSEQ_1: 45;

                 [60, 2] in KSource & [60, 3] in KTarget by ENUMSET1:def 5;

                then ( KSource . (cd . n)) = g3 & ( KTarget . (cd . n)) = g2 by cn, gg, FUNCT_1: 1;

                hence (cd . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

              end;

            end;

            thus (vs . 1) = g1 & (vs . ( len vs)) = g2 by lv, FINSEQ_1: 45;

          end;

            suppose

             gg: g1 = 2 & g2 = 0 ;

            20 in KEdges by ENUMSET1:def 5;

            then

            reconsider c = <*20*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            take c;

            reconsider vs = <*g1, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            take vs;

            thus c is non empty;

            

             l: ( len c) = 1 & (c . 1) = 20 by FINSEQ_1: 40;

            

             lv: ( len vs) = 2 by FINSEQ_1: 44;

            thus vs is_vertex_seq_of c

            proof

              thus ( len vs) = (( len c) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len c);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (c . n) = 20 by l;

              ( dom vs) = ( Seg 2) by lv, FINSEQ_1:def 3;

              then ( dom vs) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs) & 2 in ( dom vs) by TARSKI:def 2;

              

               v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

              .= g1 by n, FINSEQ_1: 44;

              

               v2: (vs /. (n + 1)) = (vs . 2) by d, n, PARTFUN1:def 6

              .= g2 by FINSEQ_1: 44;

               [20, 0 ] in KSource & [20, 2] in KTarget by ENUMSET1:def 5;

              then ( KTarget . (c . n)) = g1 & ( KSource . (c . n)) = g2 by cn, gg, FUNCT_1: 1;

              hence (c . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

            end;

            thus (vs . 1) = g1 & (vs . ( len vs)) = g2 by lv, FINSEQ_1: 44;

          end;

            suppose

             gg: g1 = 2 & g2 = 1;

            40 in KEdges by ENUMSET1:def 5;

            then

            reconsider c = <*40*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            take c;

            reconsider vs = <*g1, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            take vs;

            thus c is non empty;

            

             l: ( len c) = 1 & (c . 1) = 40 by FINSEQ_1: 40;

            

             lv: ( len vs) = 2 by FINSEQ_1: 44;

            thus vs is_vertex_seq_of c

            proof

              thus ( len vs) = (( len c) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len c);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (c . n) = 40 by l;

              ( dom vs) = ( Seg 2) by lv, FINSEQ_1:def 3;

              then ( dom vs) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs) & 2 in ( dom vs) by TARSKI:def 2;

              

               v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

              .= g1 by n, FINSEQ_1: 44;

              

               v2: (vs /. (n + 1)) = (vs . 2) by d, n, PARTFUN1:def 6

              .= g2 by FINSEQ_1: 44;

               [40, 1] in KSource & [40, 2] in KTarget by ENUMSET1:def 5;

              then ( KTarget . (c . n)) = g1 & ( KSource . (c . n)) = g2 by cn, gg, FUNCT_1: 1;

              hence (c . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

            end;

            thus (vs . 1) = g1 & (vs . ( len vs)) = g2 by lv, FINSEQ_1: 44;

          end;

            suppose g1 = 2 & g2 = 2;

            hence thesis by g;

          end;

            suppose

             gg: g1 = 2 & g2 = 3;

            60 in KEdges by ENUMSET1:def 5;

            then

            reconsider c = <*60*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            take c;

            reconsider vs = <*g1, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            take vs;

            thus c is non empty;

            

             l: ( len c) = 1 & (c . 1) = 60 by FINSEQ_1: 40;

            

             lv: ( len vs) = 2 by FINSEQ_1: 44;

            thus vs is_vertex_seq_of c

            proof

              thus ( len vs) = (( len c) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len c);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (c . n) = 60 by l;

              ( dom vs) = ( Seg 2) by lv, FINSEQ_1:def 3;

              then ( dom vs) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs) & 2 in ( dom vs) by TARSKI:def 2;

              

               v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

              .= g1 by n, FINSEQ_1: 44;

              

               v2: (vs /. (n + 1)) = (vs . 2) by d, n, PARTFUN1:def 6

              .= g2 by FINSEQ_1: 44;

               [60, 2] in KSource & [60, 3] in KTarget by ENUMSET1:def 5;

              then ( KSource . (c . n)) = g1 & ( KTarget . (c . n)) = g2 by cn, gg, FUNCT_1: 1;

              hence (c . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

            end;

            thus (vs . 1) = g1 & (vs . ( len vs)) = g2 by lv, FINSEQ_1: 44;

          end;

            suppose

             gg: g1 = 3 & g2 = 0 ;

            30 in KEdges by ENUMSET1:def 5;

            then

            reconsider c = <*30*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            take c;

            reconsider vs = <*g1, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            take vs;

            thus c is non empty;

            

             l: ( len c) = 1 & (c . 1) = 30 by FINSEQ_1: 40;

            

             lv: ( len vs) = 2 by FINSEQ_1: 44;

            thus vs is_vertex_seq_of c

            proof

              thus ( len vs) = (( len c) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len c);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (c . n) = 30 by l;

              ( dom vs) = ( Seg 2) by lv, FINSEQ_1:def 3;

              then ( dom vs) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs) & 2 in ( dom vs) by TARSKI:def 2;

              

               v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

              .= g1 by n, FINSEQ_1: 44;

              

               v2: (vs /. (n + 1)) = (vs . 2) by d, n, PARTFUN1:def 6

              .= g2 by FINSEQ_1: 44;

               [30, 0 ] in KSource & [30, 3] in KTarget by ENUMSET1:def 5;

              then ( KTarget . (c . n)) = g1 & ( KSource . (c . n)) = g2 by cn, gg, FUNCT_1: 1;

              hence (c . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

            end;

            thus (vs . 1) = g1 & (vs . ( len vs)) = g2 by lv, FINSEQ_1: 44;

          end;

            suppose

             gg: g1 = 3 & g2 = 1;

            reconsider g3 = 2 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;

            60 in KEdges by ENUMSET1:def 5;

            then

            reconsider c = <*60*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            40 in KEdges by ENUMSET1:def 5;

            then

            reconsider d = <*40*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            reconsider vs1 = <*g1, g3*> as FinSequence of the carrier of KoenigsbergBridges ;

            

             l: ( len c) = 1 & (c . 1) = 60 by FINSEQ_1: 40;

            

             lv1: ( len vs1) = 2 by FINSEQ_1: 44;

            

             vs1: vs1 is_vertex_seq_of c

            proof

              thus ( len vs1) = (( len c) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len c);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (c . n) = 60 by l;

              ( dom vs1) = ( Seg 2) by lv1, FINSEQ_1:def 3;

              then ( dom vs1) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs1) & 2 in ( dom vs1) by TARSKI:def 2;

              

               v1: (vs1 /. n) = (vs1 . n) by d, n, PARTFUN1:def 6

              .= g1 by n, FINSEQ_1: 44;

              

               v2: (vs1 /. (n + 1)) = (vs1 . 2) by d, n, PARTFUN1:def 6

              .= g3 by FINSEQ_1: 44;

               [60, 2] in KSource & [60, 3] in KTarget by ENUMSET1:def 5;

              then ( KTarget . (c . n)) = g1 & ( KSource . (c . n)) = g3 by cn, gg, FUNCT_1: 1;

              hence (c . n) joins ((vs1 /. n),(vs1 /. (n + 1))) by v1, v2;

            end;

            reconsider vs2 = <*g3, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            

             l: ( len d) = 1 & (d . 1) = 40 by FINSEQ_1: 40;

            

             lv: ( len vs2) = 2 by FINSEQ_1: 44;

            

             vs2: vs2 is_vertex_seq_of d

            proof

              thus ( len vs2) = (( len d) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len d);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (d . n) = 40 by l;

              ( dom vs2) = ( Seg 2) by lv, FINSEQ_1:def 3;

              then ( dom vs2) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs2) & 2 in ( dom vs2) by TARSKI:def 2;

              

               v1: (vs2 /. n) = (vs2 . n) by d, n, PARTFUN1:def 6

              .= g3 by n, FINSEQ_1: 44;

              

               v2: (vs2 /. (n + 1)) = (vs2 . 2) by d, n, PARTFUN1:def 6

              .= g2 by FINSEQ_1: 44;

               [40, 1] in KSource & [40, 2] in KTarget by ENUMSET1:def 5;

              then ( KTarget . (d . n)) = g3 & ( KSource . (d . n)) = g2 by cn, gg, FUNCT_1: 1;

              hence (d . n) joins ((vs2 /. n),(vs2 /. (n + 1))) by v1, v2;

            end;

            ( rng c) = {60} & ( rng d) = {40} by FINSEQ_1: 38;

            then

             r: ( rng c) misses ( rng d) by ZFMISC_1: 11;

            (vs1 . ( len vs1)) = g3 by lv1, FINSEQ_1: 44

            .= (vs2 . 1) by FINSEQ_1: 44;

            then

            reconsider cd = (c ^ d) as Path of KoenigsbergBridges by vs1, vs2, r, GRAPH_3: 6;

            take cd;

            reconsider vs = <*g1, g3, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            take vs;

            thus cd is non empty;

            cd = <*60, 40*>;

            then

             l: ( len cd) = 2 & (cd . 1) = 60 & (cd . 2) = 40 by FINSEQ_1: 44;

            

             lv: ( len vs) = 3 by FINSEQ_1: 45;

            thus vs is_vertex_seq_of cd

            proof

              thus ( len vs) = (( len cd) + 1) by l, FINSEQ_1: 45;

              let n be Nat;

              assume 1 <= n & n <= ( len cd);

              then 1 <= n & n <= (1 + 1) by l;

              then n = (1 + 0 ) or ... or n = (1 + 1) by NAT_1: 62;

              then n = 1 or n = 2;

              per cases ;

                suppose

                 n: n = 1;

                then

                 cn: (cd . n) = 60 by l;

                ( dom vs) = ( Seg 3) by lv, FINSEQ_1:def 3;

                then ( dom vs) = {1, 2, 3} by FINSEQ_3: 1;

                then

                 d: 1 in ( dom vs) & 2 in ( dom vs) by ENUMSET1:def 1;

                

                 v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

                .= g1 by n, FINSEQ_1: 45;

                

                 v2: (vs /. (n + 1)) = (vs . 2) by d, n, PARTFUN1:def 6

                .= g3 by FINSEQ_1: 45;

                 [60, 2] in KSource & [60, 3] in KTarget by ENUMSET1:def 5;

                then ( KTarget . (cd . n)) = g1 & ( KSource . (cd . n)) = g3 by cn, gg, FUNCT_1: 1;

                hence (cd . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

              end;

                suppose

                 n: n = 2;

                then

                 cn: (cd . n) = 40 by l;

                ( dom vs) = ( Seg 3) by lv, FINSEQ_1:def 3;

                then ( dom vs) = {1, 2, 3} by FINSEQ_3: 1;

                then

                 d: 2 in ( dom vs) & 3 in ( dom vs) by ENUMSET1:def 1;

                

                 v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

                .= g3 by n, FINSEQ_1: 45;

                

                 v2: (vs /. (n + 1)) = (vs . 3) by d, n, PARTFUN1:def 6

                .= g2 by FINSEQ_1: 45;

                 [40, 1] in KSource & [40, 2] in KTarget by ENUMSET1:def 5;

                then ( KTarget . (cd . n)) = g3 & ( KSource . (cd . n)) = g2 by cn, gg, FUNCT_1: 1;

                hence (cd . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

              end;

            end;

            thus (vs . 1) = g1 & (vs . ( len vs)) = g2 by lv, FINSEQ_1: 45;

          end;

            suppose

             gg: g1 = 3 & g2 = 2;

            60 in KEdges by ENUMSET1:def 5;

            then

            reconsider c = <*60*> as Path of KoenigsbergBridges by GRAPH_3: 4;

            take c;

            reconsider vs = <*g1, g2*> as FinSequence of the carrier of KoenigsbergBridges ;

            take vs;

            thus c is non empty;

            

             l: ( len c) = 1 & (c . 1) = 60 by FINSEQ_1: 40;

            

             lv: ( len vs) = 2 by FINSEQ_1: 44;

            thus vs is_vertex_seq_of c

            proof

              thus ( len vs) = (( len c) + 1) by l, FINSEQ_1: 44;

              let n be Nat;

              assume 1 <= n & n <= ( len c);

              then

               n: n = 1 by l, XXREAL_0: 1;

              then

               cn: (c . n) = 60 by l;

              ( dom vs) = ( Seg 2) by lv, FINSEQ_1:def 3;

              then ( dom vs) = {1, 2} by FINSEQ_1: 2;

              then

               d: 1 in ( dom vs) & 2 in ( dom vs) by TARSKI:def 2;

              

               v1: (vs /. n) = (vs . n) by d, n, PARTFUN1:def 6

              .= g1 by n, FINSEQ_1: 44;

              

               v2: (vs /. (n + 1)) = (vs . 2) by d, n, PARTFUN1:def 6

              .= g2 by FINSEQ_1: 44;

               [60, 2] in KSource & [60, 3] in KTarget by ENUMSET1:def 5;

              then ( KTarget . (c . n)) = g1 & ( KSource . (c . n)) = g2 by cn, gg, FUNCT_1: 1;

              hence (c . n) joins ((vs /. n),(vs /. (n + 1))) by v1, v2;

            end;

            thus (vs . 1) = g1 & (vs . ( len vs)) = g2 by lv, FINSEQ_1: 44;

          end;

            suppose g1 = 3 & g2 = 3;

            hence thesis by g;

          end;

        end;

        hence KoenigsbergBridges is finite connected by GRAPH_3: 18;

      end;

    end

    theorem :: GRAPH_3A:1

    

     d0: for v be Vertex of KoenigsbergBridges st v = 0 holds ( Degree v) = 3

    proof

      let v be Vertex of KoenigsbergBridges such that

       v: v = 0 ;

      now

        let a be object;

        reconsider s = a as set by TARSKI: 1;

        assume a in ( Edges_In v);

        then

         s: s in KEdges & ( KTarget . s) = v by GRAPH_3:def 1;

        ( dom KTarget ) = KEdges by FUNCT_2:def 1;

        then s in ( dom KTarget ) by s;

        then [s, v] in KTarget by s, FUNCT_1: 1;

        then [s, v] = [10, 1] or [s, v] = [20, 2] or [s, v] = [30, 3] or [s, v] = [40, 2] or [s, v] = [50, 2] or [s, v] = [60, 3] or [s, v] = [70, 3] by ENUMSET1:def 5;

        hence contradiction by v, XTUPLE_0: 1;

      end;

      then

       c1: ( Edges_In v) = {} by XBOOLE_0:def 1;

      

       c2: ( Edges_Out v) = {10, 20, 30}

      proof

        thus ( Edges_Out v) c= {10, 20, 30}

        proof

          let a be object;

          reconsider s = a as set by TARSKI: 1;

          assume a in ( Edges_Out v);

          then

           s: s in KEdges & ( KSource . s) = v by GRAPH_3:def 2;

          ( dom KSource ) = KEdges by FUNCT_2:def 1;

          then s in ( dom KSource ) by s;

          then [s, v] in KSource by s, FUNCT_1: 1;

          then [s, v] = [10, 0 ] or [s, v] = [20, 0 ] or [s, v] = [30, 0 ] or [s, v] = [40, 1] or [s, v] = [50, 1] or [s, v] = [60, 2] or [s, v] = [70, 2] by ENUMSET1:def 5;

          then s = 10 or s = 20 or s = 30 by v, XTUPLE_0: 1;

          hence a in {10, 20, 30} by ENUMSET1:def 1;

        end;

        let a be object;

        reconsider s = a as set by TARSKI: 1;

        assume a in {10, 20, 30};

        then

         a: a = 10 or a = 20 or a = 30 by ENUMSET1:def 1;

        then

         s: s in KEdges by ENUMSET1:def 5;

         [s, v] in KSource by v, a, ENUMSET1:def 5;

        then ( KSource . s) = v by FUNCT_1: 1;

        hence a in ( Edges_Out v) by s, GRAPH_3:def 2;

      end;

      ( Degree (v,the carrier' of KoenigsbergBridges )) = ( 0 + 3) by c1, c2, CARD_2: 58;

      hence ( Degree v) = 3 by GRAPH_3: 24;

    end;

    theorem :: GRAPH_3A:2

    

     d1: for v be Vertex of KoenigsbergBridges st v = 1 holds ( Degree v) = 3

    proof

      let v be Vertex of KoenigsbergBridges such that

       v: v = 1;

      

       c1: ( Edges_In v) = {10}

      proof

        thus ( Edges_In v) c= {10}

        proof

          let a be object;

          reconsider s = a as set by TARSKI: 1;

          assume a in ( Edges_In v);

          then

           s: s in KEdges & ( KTarget . s) = v by GRAPH_3:def 1;

          ( dom KTarget ) = KEdges by FUNCT_2:def 1;

          then s in ( dom KTarget ) by s;

          then [s, v] in KTarget by s, FUNCT_1: 1;

          then [s, v] = [10, 1] or [s, v] = [20, 2] or [s, v] = [30, 3] or [s, v] = [40, 2] or [s, v] = [50, 2] or [s, v] = [60, 3] or [s, v] = [70, 3] by ENUMSET1:def 5;

          then s = 10 by v, XTUPLE_0: 1;

          hence a in {10} by TARSKI:def 1;

        end;

        let a be object;

        reconsider s = a as set by TARSKI: 1;

        assume a in {10};

        then

         a: a = 10 by TARSKI:def 1;

        then

         s: s in KEdges by ENUMSET1:def 5;

         [s, v] in KTarget by v, a, ENUMSET1:def 5;

        then ( KTarget . s) = v by FUNCT_1: 1;

        hence a in ( Edges_In v) by s, GRAPH_3:def 1;

      end;

      

       c2: ( Edges_Out v) = {40, 50}

      proof

        thus ( Edges_Out v) c= {40, 50}

        proof

          let a be object;

          reconsider s = a as set by TARSKI: 1;

          assume a in ( Edges_Out v);

          then

           s: s in KEdges & ( KSource . s) = v by GRAPH_3:def 2;

          ( dom KSource ) = KEdges by FUNCT_2:def 1;

          then s in ( dom KSource ) by s;

          then [s, v] in KSource by s, FUNCT_1: 1;

          then [s, v] = [10, 0 ] or [s, v] = [20, 0 ] or [s, v] = [30, 0 ] or [s, v] = [40, 1] or [s, v] = [50, 1] or [s, v] = [60, 2] or [s, v] = [70, 2] by ENUMSET1:def 5;

          then s = 40 or s = 50 by v, XTUPLE_0: 1;

          hence a in {40, 50} by TARSKI:def 2;

        end;

        let a be object;

        reconsider s = a as set by TARSKI: 1;

        assume a in {40, 50};

        then

         a: a = 40 or a = 50 by TARSKI:def 2;

        then

         s: s in KEdges by ENUMSET1:def 5;

         [s, v] in KSource by v, a, ENUMSET1:def 5;

        then ( KSource . s) = v by FUNCT_1: 1;

        hence a in ( Edges_Out v) by s, GRAPH_3:def 2;

      end;

      ( card ( Edges_In v)) = 1 & ( card ( Edges_Out v)) = 2 by c1, c2, CARD_1: 30, CARD_2: 57;

      then ( Degree (v,the carrier' of KoenigsbergBridges )) = (1 + 2);

      hence ( Degree v) = 3 by GRAPH_3: 24;

    end;

    theorem :: GRAPH_3A:3

    for v be Vertex of KoenigsbergBridges st v = 2 holds ( Degree v) = 5

    proof

      let v be Vertex of KoenigsbergBridges such that

       v: v = 2;

      

       c1: ( Edges_In v) = {20, 40, 50}

      proof

        thus ( Edges_In v) c= {20, 40, 50}

        proof

          let a be object;

          reconsider s = a as set by TARSKI: 1;

          assume a in ( Edges_In v);

          then

           s: s in KEdges & ( KTarget . s) = v by GRAPH_3:def 1;

          ( dom KTarget ) = KEdges by FUNCT_2:def 1;

          then s in ( dom KTarget ) by s;

          then [s, v] in KTarget by s, FUNCT_1: 1;

          then [s, v] = [10, 1] or [s, v] = [20, 2] or [s, v] = [30, 3] or [s, v] = [40, 2] or [s, v] = [50, 2] or [s, v] = [60, 3] or [s, v] = [70, 3] by ENUMSET1:def 5;

          then s = 20 or s = 40 or s = 50 by v, XTUPLE_0: 1;

          hence a in {20, 40, 50} by ENUMSET1:def 1;

        end;

        let a be object;

        reconsider s = a as set by TARSKI: 1;

        assume a in {20, 40, 50};

        then

         a: a = 20 or a = 40 or a = 50 by ENUMSET1:def 1;

        then

         s: s in KEdges by ENUMSET1:def 5;

         [s, v] in KTarget by v, a, ENUMSET1:def 5;

        then ( KTarget . s) = v by FUNCT_1: 1;

        hence a in ( Edges_In v) by s, GRAPH_3:def 1;

      end;

      

       c2: ( Edges_Out v) = {60, 70}

      proof

        thus ( Edges_Out v) c= {60, 70}

        proof

          let a be object;

          reconsider s = a as set by TARSKI: 1;

          assume a in ( Edges_Out v);

          then

           s: s in KEdges & ( KSource . s) = v by GRAPH_3:def 2;

          ( dom KSource ) = KEdges by FUNCT_2:def 1;

          then s in ( dom KSource ) by s;

          then [s, v] in KSource by s, FUNCT_1: 1;

          then [s, v] = [10, 0 ] or [s, v] = [20, 0 ] or [s, v] = [30, 0 ] or [s, v] = [40, 1] or [s, v] = [50, 1] or [s, v] = [60, 2] or [s, v] = [70, 2] by ENUMSET1:def 5;

          then s = 60 or s = 70 by v, XTUPLE_0: 1;

          hence a in {60, 70} by TARSKI:def 2;

        end;

        let a be object;

        reconsider s = a as set by TARSKI: 1;

        assume a in {60, 70};

        then

         a: a = 60 or a = 70 by TARSKI:def 2;

        then

         s: s in KEdges by ENUMSET1:def 5;

         [s, v] in KSource by v, a, ENUMSET1:def 5;

        then ( KSource . s) = v by FUNCT_1: 1;

        hence a in ( Edges_Out v) by s, GRAPH_3:def 2;

      end;

      ( card ( Edges_In v)) = 3 & ( card ( Edges_Out v)) = 2 by c1, c2, CARD_2: 57, CARD_2: 58;

      then ( Degree (v,the carrier' of KoenigsbergBridges )) = (3 + 2);

      hence ( Degree v) = 5 by GRAPH_3: 24;

    end;

    theorem :: GRAPH_3A:4

    

     d3: for v be Vertex of KoenigsbergBridges st v = 3 holds ( Degree v) = 3

    proof

      let v be Vertex of KoenigsbergBridges such that

       v: v = 3;

      

       c1: ( Edges_In v) = {30, 60, 70}

      proof

        thus ( Edges_In v) c= {30, 60, 70}

        proof

          let a be object;

          reconsider s = a as set by TARSKI: 1;

          assume a in ( Edges_In v);

          then

           s: s in KEdges & ( KTarget . s) = v by GRAPH_3:def 1;

          ( dom KTarget ) = KEdges by FUNCT_2:def 1;

          then s in ( dom KTarget ) by s;

          then [s, v] in KTarget by s, FUNCT_1: 1;

          then [s, v] = [10, 1] or [s, v] = [20, 2] or [s, v] = [30, 3] or [s, v] = [40, 2] or [s, v] = [50, 2] or [s, v] = [60, 3] or [s, v] = [70, 3] by ENUMSET1:def 5;

          then s = 30 or s = 60 or s = 70 by v, XTUPLE_0: 1;

          hence a in {30, 60, 70} by ENUMSET1:def 1;

        end;

        let a be object;

        reconsider s = a as set by TARSKI: 1;

        assume a in {30, 60, 70};

        then

         a: a = 30 or a = 60 or a = 70 by ENUMSET1:def 1;

        then

         s: s in KEdges by ENUMSET1:def 5;

         [s, v] in KTarget by v, a, ENUMSET1:def 5;

        then ( KTarget . s) = v by FUNCT_1: 1;

        hence a in ( Edges_In v) by s, GRAPH_3:def 1;

      end;

      

       c2: ( Edges_Out v) = {}

      proof

        thus ( Edges_Out v) c= {}

        proof

          let a be object;

          reconsider s = a as set by TARSKI: 1;

          assume a in ( Edges_Out v);

          then

           s: s in KEdges & ( KSource . s) = v by GRAPH_3:def 2;

          ( dom KSource ) = KEdges by FUNCT_2:def 1;

          then s in ( dom KSource ) by s;

          then [s, v] in KSource by s, FUNCT_1: 1;

          then [s, v] = [10, 0 ] or [s, v] = [20, 0 ] or [s, v] = [30, 0 ] or [s, v] = [40, 1] or [s, v] = [50, 1] or [s, v] = [60, 2] or [s, v] = [70, 2] by ENUMSET1:def 5;

          hence a in {} by v, XTUPLE_0: 1;

        end;

        let a be object;

        assume a in {} ;

        hence a in ( Edges_Out v);

      end;

      ( card ( Edges_In v)) = 3 & ( card ( Edges_Out v)) = 0 by c1, c2, CARD_2: 58;

      then ( Degree (v,the carrier' of KoenigsbergBridges )) = (3 + 0 );

      hence ( Degree v) = 3 by GRAPH_3: 24;

    end;

    ::$Notion-Name

    theorem :: GRAPH_3A:5

     not ex p be Path of KoenigsbergBridges st p is cyclic Eulerian

    proof

      reconsider v = 0 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;

      ( Degree v) = 3 by d0;

      then not ( Degree v) is even by POLYFORM: 6;

      hence thesis by GRAPH_3: 59;

    end;

    theorem :: GRAPH_3A:6

     not ex p be Path of KoenigsbergBridges st p is non cyclic Eulerian

    proof

      given p be Path of KoenigsbergBridges such that

       p: p is non cyclic Eulerian;

      consider v1,v2 be Vertex of KoenigsbergBridges such that

       v: v1 <> v2 & for v be Vertex of KoenigsbergBridges holds ( Degree v) is even iff v <> v1 & v <> v2 by p, GRAPH_3: 60;

      (v1 = 0 or v1 = 1 or v1 = 2 or v1 = 3) & (v2 = 0 or v2 = 1 or v2 = 2 or v2 = 3) & v1 <> v2 by v, ENUMSET1:def 2;

      per cases ;

        suppose

         s: v1 = 0 & v2 = 1 or v1 = 0 & v2 = 2 or v1 = 1 & v2 = 0 or v1 = 1 & v2 = 2 or v1 = 2 & v2 = 0 or v1 = 2 & v2 = 1;

        reconsider v = 3 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;

        ( Degree v) = 3 by d3;

        then not ( Degree v) is even by POLYFORM: 6;

        hence contradiction by s, v;

      end;

        suppose

         s: v1 = 1 & v2 = 3 or v1 = 2 & v2 = 3 or v1 = 3 & v2 = 1 or v1 = 3 & v2 = 2;

        reconsider v = 0 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;

        ( Degree v) = 3 by d0;

        then not ( Degree v) is even by POLYFORM: 6;

        hence contradiction by s, v;

      end;

        suppose

         s: v1 = 0 & v2 = 3 or v1 = 3 & v2 = 0 ;

        reconsider v = 1 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;

        ( Degree v) = 3 by d1;

        then not ( Degree v) is even by POLYFORM: 6;

        hence contradiction by s, v;

      end;

    end;