graph_3.miz



    begin

    definition

      let D be set, T be non empty FinSequenceSet of D, S be non empty Subset of T;

      :: original: Element

      redefine

      mode Element of S -> FinSequence of D ;

      coherence

      proof

        let x be Element of S;

        x is Element of T;

        hence thesis;

      end;

    end

    registration

      let i,j be even Integer;

      cluster (i - j) -> even;

      coherence

      proof

        2 divides j by ABIAN:def 1;

        then

        consider l be Integer such that

         A1: j = (2 * l) by INT_1:def 3;

        2 divides i by ABIAN:def 1;

        then

        consider k be Integer such that

         A2: i = (2 * k) by INT_1:def 3;

        (i - j) = (2 * (k - l)) by A2, A1;

        hence thesis;

      end;

    end

    theorem :: GRAPH_3:1

    for i,j be Integer holds (i is even iff j is even) iff (i - j) is even;

    

     Lm1: for p be FinSequence, m,n be Nat st 1 <= m & m <= (n + 1) & n <= ( len p) holds (( len ((m,n) -cut p)) + m) = (n + 1) & for i be Nat st i < ( len ((m,n) -cut p)) holds (((m,n) -cut p) . (i + 1)) = (p . (m + i))

    proof

      let p be FinSequence, m,n be Nat such that

       A1: 1 <= m and

       A2: m <= (n + 1) and

       A3: n <= ( len p);

      

       A4: m = (n + 1) or m < (n + 1) by A2, XXREAL_0: 1;

      per cases by A4, NAT_1: 13;

        suppose

         A5: m = (n + 1);

        then n < m by XREAL_1: 29;

        then ((m,n) -cut p) = {} by FINSEQ_6:def 4;

        hence (( len ((m,n) -cut p)) + m) = (n + 1) by A5;

         not (1 <= m & m <= n & n <= ( len p)) by A5, XREAL_1: 29;

        hence thesis by CARD_1: 27, FINSEQ_6:def 4;

      end;

        suppose m <= n;

        hence thesis by A1, A3, FINSEQ_6:def 4;

      end;

    end;

    theorem :: GRAPH_3:2

    

     Th2: for p be FinSequence, m,n,a be Nat st a in ( dom ((m,n) -cut p)) holds ex k be Nat st k in ( dom p) & (p . k) = (((m,n) -cut p) . a) & (k + 1) = (m + a) & m <= k & k <= n

    proof

      let p be FinSequence, m,n,a be Nat such that

       A1: a in ( dom ((m,n) -cut p));

      set cp = ((m,n) -cut p);

      

       A2: a <= ( len cp) by A1, FINSEQ_3: 25;

      per cases ;

        suppose

         A3: 1 <= m & m <= n & n <= ( len p);

        ( 0 + 1) <= a by A1, FINSEQ_3: 25;

        then

        consider i1 be Nat such that 0 <= i1 and

         A4: i1 < ( len cp) and

         A5: a = (i1 + 1) by A2, FINSEQ_6: 127;

        take k = (m + i1);

        m <= k by NAT_1: 11;

        then

         A6: 1 <= k by A3, XXREAL_0: 2;

        

         A7: (( len cp) + m) = (n + 1) by A3, FINSEQ_6:def 4;

        

         A8: (m + i1) < (m + ( len cp)) by A4, XREAL_1: 6;

        then (m + i1) <= n by A7, NAT_1: 13;

        then k <= ( len p) by A3, XXREAL_0: 2;

        hence k in ( dom p) by A6, FINSEQ_3: 25;

        thus (p . k) = (cp . a) by A3, A4, A5, FINSEQ_6:def 4;

        thus (k + 1) = (m + a) by A5;

        thus thesis by A7, A8, NAT_1: 11, NAT_1: 13;

      end;

        suppose not (1 <= m & m <= n & n <= ( len p));

        hence thesis by A1, FINSEQ_6:def 4, RELAT_1: 38;

      end;

    end;

    definition

      let G be Graph;

      mode Vertex of G is Element of the carrier of G;

    end

    reserve G for Graph,

v,v1,v2 for Vertex of G,

c for Chain of G,

p,p1,p2 for Path of G,

vs,vs1,vs2 for FinSequence of the carrier of G,

e,X for set,

n,m for Nat;

    theorem :: GRAPH_3:3

    vs is_vertex_seq_of c implies vs is non empty;

    

     Lm2: 1 <= n & n <= ( len p) & 1 <= m & m <= ( len p) & n <> m implies (p . n) <> (p . m)

    proof

      assume that

       A1: 1 <= n & n <= ( len p) & 1 <= m & m <= ( len p) and

       A2: n <> m;

      n in ( dom p) & m in ( dom p) by A1, FINSEQ_3: 25;

      hence thesis by A2, FUNCT_1:def 4;

    end;

    theorem :: GRAPH_3:4

    

     Th4: e in the carrier' of G implies <*e*> is Path of G

    proof

      assume e in the carrier' of G;

      then

      reconsider c = <*e*> as Chain of G by MSSCYC_1: 5;

      now

        let n,m be Nat;

        

         A1: ( len c) = 1 by FINSEQ_1: 39;

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

        hence (c . n) <> (c . m) by A1, XXREAL_0: 2;

      end;

      hence thesis by GRAPH_1:def 16;

    end;

    theorem :: GRAPH_3:5

    

     Th5: ((m,n) -cut p) is Path of G

    proof

      per cases ;

        suppose not 1 <= m or not n <= ( len p) or m > n;

        then ((m,n) -cut p) = {} by FINSEQ_6:def 4;

        hence thesis by GRAPH_1: 14;

      end;

        suppose 1 <= m & m <= n & n <= ( len p);

        then

        reconsider q = ((m,n) -cut p) as Chain of G by GRAPH_2: 41;

        assume not ((m,n) -cut p) is Path of G;

        then

        consider a,b be Nat such that

         A1: 1 <= a and

         A2: a < b and

         A3: b <= ( len q) and

         A4: (q . a) = (q . b) by GRAPH_1:def 16;

        1 <= b by A1, A2, XXREAL_0: 2;

        then b in ( dom q) by A3, FINSEQ_3: 25;

        then

        consider kb be Nat such that

         A5: kb in ( dom p) & (p . kb) = (q . b) and

         A6: (kb + 1) = (m + b) and m <= kb and kb <= n by Th2;

        a <= ( len q) by A2, A3, XXREAL_0: 2;

        then a in ( dom q) by A1, FINSEQ_3: 25;

        then

        consider ka be Nat such that

         A7: ka in ( dom p) & (p . ka) = (q . a) and

         A8: (ka + 1) = (m + a) and m <= ka and ka <= n by Th2;

        ka = kb by A4, A7, A5, FUNCT_1:def 4;

        hence contradiction by A2, A8, A6;

      end;

    end;

    theorem :: GRAPH_3:6

    

     Th6: ( rng p1) misses ( rng p2) & vs1 is_vertex_seq_of p1 & vs2 is_vertex_seq_of p2 & (vs1 . ( len vs1)) = (vs2 . 1) implies (p1 ^ p2) is Path of G

    proof

      set c1 = p1, c2 = p2;

      assume that

       A1: ( rng c1) misses ( rng c2) and

       A2: vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & (vs1 . ( len vs1)) = (vs2 . 1);

      reconsider c = (c1 ^ c2) as Chain of G by A2, GRAPH_2: 43;

      now

        let n,m be Nat such that

         A3: 1 <= n and

         A4: n < m and

         A5: m <= ( len c) and

         A6: (c . n) = (c . m);

        1 <= m by A3, A4, XXREAL_0: 2;

        then

         A7: m in ( dom c) by A5, FINSEQ_3: 25;

        n <= ( len c) by A4, A5, XXREAL_0: 2;

        then

         A8: n in ( dom c) by A3, FINSEQ_3: 25;

        per cases by A8, A7, FINSEQ_1: 25;

          suppose

           A9: n in ( dom c1) & m in ( dom c1);

          

          then (c1 . n) = (c . n) by FINSEQ_1:def 7

          .= (c1 . m) by A6, A9, FINSEQ_1:def 7;

          hence contradiction by A4, A9, FUNCT_1:def 4;

        end;

          suppose

           A10: n in ( dom c1) & ex m2 be Nat st m2 in ( dom c2) & m = (( len c1) + m2);

          then

           A11: (c1 . n) in ( rng c1) by FUNCT_1:def 3;

          consider m2 be Nat such that

           A12: m2 in ( dom c2) and

           A13: m = (( len c1) + m2) by A10;

          

           A14: (c2 . m2) in ( rng c2) by A12, FUNCT_1:def 3;

          (c1 . n) = (c . n) by A10, FINSEQ_1:def 7

          .= (c2 . m2) by A6, A12, A13, FINSEQ_1:def 7;

          hence contradiction by A1, A11, A14, XBOOLE_0: 3;

        end;

          suppose

           A15: m in ( dom c1) & ex n2 be Nat st n2 in ( dom c2) & n = (( len c1) + n2);

          then

          consider n2 be Nat such that n2 in ( dom c2) and

           A16: n = (( len c1) + n2);

          m <= ( len c1) by A15, FINSEQ_3: 25;

          then (( len c1) + n2) < ( len c1) by A4, A16, XXREAL_0: 2;

          hence contradiction by NAT_1: 11;

        end;

          suppose

           A17: (ex n2 be Nat st n2 in ( dom c2) & n = (( len c1) + n2)) & ex m2 be Nat st m2 in ( dom c2) & m = (( len c1) + m2);

          then

          consider n2 be Nat such that

           A18: n2 in ( dom c2) & n = (( len c1) + n2);

          consider m2 be Nat such that

           A19: m2 in ( dom c2) & m = (( len c1) + m2) by A17;

          (c2 . n2) = (c . n) by A18, FINSEQ_1:def 7

          .= (c2 . m2) by A6, A19, FINSEQ_1:def 7;

          hence contradiction by A4, A19, A18, FUNCT_1:def 4;

        end;

      end;

      hence thesis by GRAPH_1:def 16;

    end;

    theorem :: GRAPH_3:7

    

     Th7: c = {} implies c is cyclic

    proof

      set v = the Vertex of G;

      assume c = {} ;

      then

       A1: <*v*> is_vertex_seq_of c by GRAPH_2: 32;

      ( <*v*> . 1) = ( <*v*> . ( len <*v*>)) by FINSEQ_1: 40;

      hence thesis by A1;

    end;

    registration

      let G be Graph;

      cluster cyclic for Path of G;

      existence

      proof

        reconsider p = {} as Path of G by GRAPH_1: 14;

        take p;

        thus thesis by Th7;

      end;

    end

    theorem :: GRAPH_3:8

    

     Th8: for p be cyclic Path of G holds ((((m + 1),( len p)) -cut p) ^ ((1,m) -cut p)) is cyclic Path of G

    proof

      let p be cyclic Path of G;

      per cases by NAT_1: 14, XXREAL_0: 1;

        suppose

         A1: m = 0 ;

         0 <= ( len p);

        then (( len ((1,m) -cut p)) + 1) = ( 0 + 1) by A1, Lm1;

        then

         A2: ((1,m) -cut p) = {} ;

        (((m + 1),( len p)) -cut p) = p by A1, FINSEQ_6: 133;

        hence thesis by A2, FINSEQ_1: 34;

      end;

        suppose

         A3: 1 <= m & ( len p) = m;

        1 <= (m + 1) by NAT_1: 12;

        then (( len (((m + 1),( len p)) -cut p)) + (m + 1)) = (( len p) + 1) by A3, Lm1;

        then (((m + 1),( len p)) -cut p) = {} by A3;

        

        then ((((m + 1),( len p)) -cut p) ^ ((1,m) -cut p)) = ((1,m) -cut p) by FINSEQ_1: 34

        .= p by A3, FINSEQ_6: 133;

        hence thesis;

      end;

        suppose

         A4: 1 <= m & ( len p) < m;

        m <= (m + 1) by NAT_1: 11;

        then ( len p) < (m + 1) by A4, XXREAL_0: 2;

        then

         A5: (((m + 1),( len p)) -cut p) = {} by FINSEQ_6:def 4;

        ((1,m) -cut p) = {} by A4, FINSEQ_6:def 4;

        then ((((m + 1),( len p)) -cut p) ^ ((1,m) -cut p)) = {} by A5, FINSEQ_1: 34;

        hence thesis by Th7, GRAPH_1: 14;

      end;

        suppose

         A6: 1 <= m & m < ( len p);

        set n1 = m, n = (m + 1);

        

         A7: 1 <= n by A6, NAT_1: 13;

        reconsider r1 = ((1,n1) -cut p), r2 = ((n,( len p)) -cut p) as Path of G by Th5;

        consider vs be FinSequence of the carrier of G such that

         A8: vs is_vertex_seq_of p by GRAPH_2: 33;

        reconsider vs1 = ((1,n) -cut vs), vs2 = ((n,( len vs)) -cut vs) as FinSequence of the carrier of G;

        

         A9: n <= ( len p) by A6, NAT_1: 13;

        

         A10: ( len vs) = (( len p) + 1) by A8;

        

         A11: vs2 is_vertex_seq_of r2 by A7, A9, A8, GRAPH_2: 42;

        ( len p) <= (( len p) + 1) by NAT_1: 11;

        then

         A12: n <= ( len vs) by A9, A10, XXREAL_0: 2;

        then

         A13: n < (( len vs) + 1) by NAT_1: 13;

        (( len vs1) + 1) = (n + 1) by A7, A12, FINSEQ_6:def 4;

        then

         A14: 1 < ( len vs1) by A6, NAT_1: 13;

        

         A15: vs1 is_vertex_seq_of r1 by A6, A8, GRAPH_2: 42;

        ( len vs) <= (( len vs) + 1) by NAT_1: 11;

        then n <= (( len vs) + 1) by A12, XXREAL_0: 2;

        then (( len vs2) + n) = (( len vs) + 1) by A7, Lm1;

        then (1 + n) <= (( len vs2) + n) by A13, NAT_1: 13;

        then

         A16: 1 <= ( len vs2) by XREAL_1: 6;

        reconsider vs9 = (vs2 ^' vs1) as FinSequence of the carrier of G;

        set r = (r2 ^ r1);

        

         A17: (vs . ( len vs)) = (vs . 1) by A8, MSSCYC_1: 6;

        

         A18: (vs1 . 1) = (vs . 1) & (vs2 . ( len vs2)) = (vs . ( len vs)) by A7, A12, FINSEQ_6: 138;

        then

        reconsider r as Chain of G by A17, A15, A11, GRAPH_2: 43;

        

         A19: vs9 is_vertex_seq_of r by A17, A15, A11, A18, GRAPH_2: 44;

        p = (r1 ^ r2) by A6, FINSEQ_6: 135;

        then ( rng r1) misses ( rng r2) by FINSEQ_3: 91;

        then

        reconsider r as Path of G by A17, A15, A11, A18, Th6;

        (vs1 . ( len vs1)) = (vs . n) & (vs2 . 1) = (vs . n) by A7, A12, FINSEQ_6: 138;

        

        then (vs9 . 1) = (vs1 . ( len vs1)) by A16, FINSEQ_6: 140

        .= (vs9 . ( len vs9)) by A14, FINSEQ_6: 142;

        then r is cyclic Path of G by A19, MSSCYC_1:def 2;

        hence thesis;

      end;

    end;

    theorem :: GRAPH_3:9

    

     Th9: (m + 1) in ( dom p) implies ( len ((((m + 1),( len p)) -cut p) ^ ((1,m) -cut p))) = ( len p) & ( rng ((((m + 1),( len p)) -cut p) ^ ((1,m) -cut p))) = ( rng p) & (((((m + 1),( len p)) -cut p) ^ ((1,m) -cut p)) . 1) = (p . (m + 1))

    proof

      set r2 = (((m + 1),( len p)) -cut p);

      set r1 = ((1,m) -cut p);

      set r = (r2 ^ r1);

      set n = (m + 1);

      assume

       A1: (m + 1) in ( dom p);

      then

       A2: (m + 1) <= ( len p) by FINSEQ_3: 25;

      then

       A3: n < (( len p) + 1) by NAT_1: 13;

      m <= (m + 1) by NAT_1: 11;

      then

       A4: p = (r1 ^ r2) by A2, FINSEQ_6: 135, XXREAL_0: 2;

      

      thus ( len r) = (( len r1) + ( len r2)) by FINSEQ_1: 22

      .= ( len p) by A4, FINSEQ_1: 22;

      

      thus ( rng r) = (( rng r1) \/ ( rng r2)) by FINSEQ_1: 31

      .= ( rng p) by A4, FINSEQ_1: 31;

      

       A5: 1 <= (m + 1) by A1, FINSEQ_3: 25;

      then (( len r2) + n) = (( len p) + 1) by A2, FINSEQ_6:def 4;

      then (1 + n) <= (( len r2) + n) by A3, NAT_1: 13;

      then

       A6: 1 <= ( len r2) by XREAL_1: 6;

      then 1 in ( dom r2) by FINSEQ_3: 25;

      

      hence (r . 1) = (r2 . ( 0 + 1)) by FINSEQ_1:def 7

      .= (p . (n + 0 )) by A5, A2, A6, FINSEQ_6:def 4

      .= (p . n);

    end;

    theorem :: GRAPH_3:10

    

     Th10: for p be cyclic Path of G st n in ( dom p) holds ex p9 be cyclic Path of G st (p9 . 1) = (p . n) & ( len p9) = ( len p) & ( rng p9) = ( rng p)

    proof

      let p be cyclic Path of G;

      assume

       A1: n in ( dom p);

      then

       A2: 1 <= n by FINSEQ_3: 25;

      per cases by A2, XXREAL_0: 1;

        suppose

         A3: n = 1;

        take p;

        thus thesis by A3;

      end;

        suppose 1 < n;

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

        then

        consider n1 be Nat such that 1 <= n1 and n1 < n and

         A4: n = (n1 + 1) by FINSEQ_6: 127;

        reconsider r = (((n,( len p)) -cut p) ^ ((1,n1) -cut p)) as cyclic Path of G by A4, Th8;

        take r;

        thus thesis by A1, A4, Th9;

      end;

    end;

    theorem :: GRAPH_3:11

    

     Th11: for s,t be Vertex of G st s = (the Source of G . e) & t = (the Target of G . e) holds <*t, s*> is_vertex_seq_of <*e*>

    proof

      let s,t be Element of the carrier of G;

      assume

       A1: s = (the Source of G . e) & t = (the Target of G . e);

      set c = <*e*>;

      set vs = <*t, s*>;

      

       A2: (vs /. (1 + 1)) = s by FINSEQ_4: 17;

      

       A3: ( len c) = 1 by FINSEQ_1: 39;

      hence ( len vs) = (( len c) + 1) by FINSEQ_1: 44;

      let n be Nat;

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

      then

       A4: n = 1 by A3, XXREAL_0: 1;

      (c . 1) = e & (vs /. 1) = t by FINSEQ_1: 40, FINSEQ_4: 17;

      hence thesis by A1, A4, A2;

    end;

    theorem :: GRAPH_3:12

    

     Th12: e in the carrier' of G & vs is_vertex_seq_of c & (vs . ( len vs)) = (the Source of G . e) implies (c ^ <*e*>) is Chain of G & ex vs9 be FinSequence of the carrier of G st vs9 = (vs ^' <*(the Source of G . e), (the Target of G . e)*>) & vs9 is_vertex_seq_of (c ^ <*e*>) & (vs9 . 1) = (vs . 1) & (vs9 . ( len vs9)) = (the Target of G . e)

    proof

      assume that

       A1: e in the carrier' of G and

       A2: vs is_vertex_seq_of c;

      reconsider ec = <*e*> as Chain of G by A1, MSSCYC_1: 5;

      reconsider s = (the Source of G . e), t = (the Target of G . e) as Vertex of G by A1, FUNCT_2: 5;

      reconsider vse = <*s, t*> as FinSequence of the carrier of G;

      

       A3: vse is_vertex_seq_of ec & (vse . 1) = s by FINSEQ_1: 44, MSSCYC_1: 4;

      assume

       A4: (vs . ( len vs)) = (the Source of G . e);

      hence (c ^ <*e*>) is Chain of G by A2, A3, GRAPH_2: 43;

      reconsider ce = (c ^ ec) as Chain of G by A2, A4, A3, GRAPH_2: 43;

      take vs9 = (vs ^' vse);

      thus vs9 = (vs ^' <*(the Source of G . e), (the Target of G . e)*>);

      vs9 is_vertex_seq_of ce by A2, A4, A3, GRAPH_2: 44;

      hence vs9 is_vertex_seq_of (c ^ <*e*>);

      ( len vs) = (( len c) + 1) by A2;

      then 1 <= ( len vs) by NAT_1: 11;

      hence (vs9 . 1) = (vs . 1) by FINSEQ_6: 140;

      

       A5: ( len vse) = 2 by FINSEQ_1: 44;

      then (vse . ( len vse)) = t by FINSEQ_1: 44;

      hence thesis by A5, FINSEQ_6: 142;

    end;

    theorem :: GRAPH_3:13

    

     Th13: e in the carrier' of G & vs is_vertex_seq_of c & (vs . ( len vs)) = (the Target of G . e) implies (c ^ <*e*>) is Chain of G & ex vs9 be FinSequence of the carrier of G st vs9 = (vs ^' <*(the Target of G . e), (the Source of G . e)*>) & vs9 is_vertex_seq_of (c ^ <*e*>) & (vs9 . 1) = (vs . 1) & (vs9 . ( len vs9)) = (the Source of G . e)

    proof

      assume that

       A1: e in the carrier' of G and

       A2: vs is_vertex_seq_of c;

      reconsider ec = <*e*> as Chain of G by A1, MSSCYC_1: 5;

      reconsider s = (the Source of G . e), t = (the Target of G . e) as Vertex of G by A1, FUNCT_2: 5;

      assume

       A3: (vs . ( len vs)) = (the Target of G . e);

      reconsider vse = <*t, s*> as FinSequence of the carrier of G;

      

       A4: vse is_vertex_seq_of ec & (vse . 1) = t by Th11, FINSEQ_1: 44;

      hence (c ^ <*e*>) is Chain of G by A2, A3, GRAPH_2: 43;

      reconsider ce = (c ^ ec) as Chain of G by A2, A3, A4, GRAPH_2: 43;

      take vs9 = (vs ^' vse);

      thus vs9 = (vs ^' <*(the Target of G . e), (the Source of G . e)*>);

      vs9 is_vertex_seq_of ce by A2, A3, A4, GRAPH_2: 44;

      hence vs9 is_vertex_seq_of (c ^ <*e*>);

      ( len vs) = (( len c) + 1) by A2;

      then 1 <= ( len vs) by NAT_1: 11;

      hence (vs9 . 1) = (vs . 1) by FINSEQ_6: 140;

      

       A5: ( len vse) = 2 by FINSEQ_1: 44;

      then (vse . ( len vse)) = s by FINSEQ_1: 44;

      hence thesis by A5, FINSEQ_6: 142;

    end;

    

     Lm3: for G be Graph, c be Chain of G, vs be FinSequence of the carrier of G st vs is_vertex_seq_of c holds for n be Nat st 1 <= n & n <= ( len c) holds 1 <= n & n <= ( len vs) & 1 <= (n + 1) & (n + 1) <= ( len vs) & ((vs . n) = (the Target of G . (c . n)) & (vs . (n + 1)) = (the Source of G . (c . n)) or (vs . n) = (the Source of G . (c . n)) & (vs . (n + 1)) = (the Target of G . (c . n)))

    proof

      let G be Graph, c be Chain of G, vs be FinSequence of the carrier of G;

      assume

       A1: vs is_vertex_seq_of c;

      then

       A2: ( len vs) = (( len c) + 1);

      let n be Nat such that

       A3: 1 <= n and

       A4: n <= ( len c);

      thus 1 <= n by A3;

      ( len c) <= (( len c) + 1) by NAT_1: 11;

      hence

       A5: n <= ( len vs) by A4, A2, XXREAL_0: 2;

      thus 1 <= (n + 1) by NAT_1: 11;

      thus

       A6: (n + 1) <= ( len vs) by A4, A2, XREAL_1: 6;

      reconsider n as Element of NAT by ORDINAL1:def 12;

      

       A7: (vs . n) = (vs /. n) by A3, A5, FINSEQ_4: 15;

      

       A8: (vs . (n + 1)) = (vs /. (n + 1)) by A6, FINSEQ_4: 15, NAT_1: 11;

      (c . n) joins ((vs /. n),(vs /. (n + 1))) by A1, A3, A4;

      hence thesis by A7, A8;

    end;

    theorem :: GRAPH_3:14

    vs is_vertex_seq_of c implies for n be Element of NAT st n in ( dom c) holds ((vs . n) = (the Target of G . (c . n)) & (vs . (n + 1)) = (the Source of G . (c . n)) or (vs . n) = (the Source of G . (c . n)) & (vs . (n + 1)) = (the Target of G . (c . n)))

    proof

      assume

       A1: vs is_vertex_seq_of c;

      let n be Element of NAT ;

      assume n in ( dom c);

      then 1 <= n & n <= ( len c) by FINSEQ_3: 25;

      hence thesis by A1, Lm3;

    end;

    theorem :: GRAPH_3:15

    

     Th15: vs is_vertex_seq_of c & e in ( rng c) implies (the Target of G . e) in ( rng vs) & (the Source of G . e) in ( rng vs)

    proof

      assume that

       A1: vs is_vertex_seq_of c and

       A2: e in ( rng c);

      c is FinSequence of the carrier' of G by MSSCYC_1:def 1;

      then

       A3: ( rng c) c= the carrier' of G by FINSEQ_1:def 4;

      then

      reconsider e9 = e as Element of the carrier' of G by A2;

      reconsider t = (the Target of G . e), s = (the Source of G . e) as Vertex of G by A2, A3, FUNCT_2: 5;

      e9 in ( rng c) by A2;

      then t in (G -VSet ( rng c)) & s in (G -VSet ( rng c));

      hence thesis by A1, A2, GRAPH_2: 31, RELAT_1: 38;

    end;

    definition

      let G be Graph, X be set;

      :: original: -VSet

      redefine

      func G -VSet X -> Subset of the carrier of G ;

      coherence

      proof

        defpred P[ set] means ex e be Element of the carrier' of G st e in X & ($1 = (the Source of G . e) or $1 = (the Target of G . e));

        { v where v be Vertex of G : P[v] } is Subset of the carrier of G from DOMAIN_1:sch 7;

        hence thesis;

      end;

    end

    theorem :: GRAPH_3:16

    

     Th16: (G -VSet {} ) = {}

    proof

      assume not thesis;

      then

      consider x be object such that

       A1: x in (G -VSet {} ) by XBOOLE_0:def 1;

      ex v be Vertex of G st x = v & ex e be Element of the carrier' of G st e in {} & (v = (the Source of G . e) or v = (the Target of G . e)) by A1;

      hence contradiction;

    end;

    theorem :: GRAPH_3:17

    

     Th17: e in the carrier' of G & e in X implies (G -VSet X) is non empty

    proof

      assume that

       A1: e in the carrier' of G and

       A2: e in X;

      reconsider v = (the Source of G . e) as Vertex of G by A1, FUNCT_2: 5;

      v in (G -VSet X) by A1, A2;

      hence thesis;

    end;

    theorem :: GRAPH_3:18

    

     Th18: G is connected iff for v1, v2 st v1 <> v2 holds ex c, vs st c is non empty & vs is_vertex_seq_of c & (vs . 1) = v1 & (vs . ( len vs)) = v2

    proof

      set E = the carrier' of G;

      set S = the Source of G;

      set T = the Target of G;

      thus G is connected implies for v1,v2 be Vertex of G st v1 <> v2 holds ex c be Chain of G, vs be FinSequence of the carrier of G st c is non empty & vs is_vertex_seq_of c & (vs . 1) = v1 & (vs . ( len vs)) = v2

      proof

        reconsider V = the carrier of G as non empty set;

        assume

         A1: G is connected;

        let v1,v2 be Vertex of G;

        set V1 = { v where v be Element of V : v = v1 or ex c be Chain of G, vs be FinSequence of the carrier of G st c is non empty & vs is_vertex_seq_of c & (vs . 1) = v1 & (vs . ( len vs)) = v };

        set V2 = (V \ V1);

        v1 in V1;

        then

        reconsider V1 as non empty set;

        assume

         A2: v1 <> v2;

        assume

         A3: not thesis;

        now

          assume v2 in V1;

          then ex v be Vertex of G st v = v2 & (v = v1 or ex c be Chain of G, vs be FinSequence of the carrier of G st c is non empty & vs is_vertex_seq_of c & (vs . 1) = v1 & (vs . ( len vs)) = v);

          hence contradiction by A2, A3;

        end;

        then

        reconsider V2 as non empty set by XBOOLE_0:def 5;

        defpred P[ set] means $1 = v1 or ex c be Chain of G, vs be FinSequence of the carrier of G st c is non empty & vs is_vertex_seq_of c & (vs . 1) = v1 & (vs . ( len vs)) = $1;

        

         A4: { v where v be Element of V : P[v] } is Subset of V from DOMAIN_1:sch 7;

        defpred P[ object] means (the Source of G . $1) in V1 & (the Target of G . $1) in V1;

        consider E1 be set such that

         A5: for e be object holds e in E1 iff e in E & P[e] from XBOOLE_0:sch 1;

        

         A6: ( dom S) = E by FUNCT_2:def 1;

        set E2 = (E \ E1);

        

         A7: ( dom (S | E2)) = (( dom S) /\ E2) by RELAT_1: 61

        .= E2 by A6, XBOOLE_1: 28;

        

         A8: ( rng S) c= V by RELAT_1:def 19;

        ( rng (S | E2)) c= V2

        proof

          let v be object;

          assume v in ( rng (S | E2));

          then

          consider e be object such that

           A9: e in ( dom (S | E2)) and

           A10: ((S | E2) . e) = v by FUNCT_1:def 3;

          reconsider e as Element of the carrier' of G by A7, A9;

          

           A11: ((S | E2) . e) = (S . e) by A9, FUNCT_1: 47;

          

           A12: not e in E1 by A7, A9, XBOOLE_0:def 5;

          per cases by A5, A12;

            suppose not e in E;

            hence thesis by A7, A9;

          end;

            suppose

             A13: not (the Source of G . e) in V1;

            (S . e) in V by A7, A9, FUNCT_2: 5;

            hence thesis by A10, A11, A13, XBOOLE_0:def 5;

          end;

            suppose

             A14: not (the Target of G . e) in V1;

            reconsider Te = (T . e) as Vertex of G by A7, A9, FUNCT_2: 5;

            v in ( rng (S | E2)) & ( rng (S | E2)) c= ( rng S) by A9, A10, FUNCT_1:def 3, RELAT_1: 70;

            then

             A15: v in ( rng S);

            assume not v in V2;

            then v in V1 by A8, A15, XBOOLE_0:def 5;

            then

            consider v9 be Vertex of G such that

             A16: v9 = v and

             A17: v9 = v1 or ex c be Chain of G, vs be FinSequence of the carrier of G st c is non empty & vs is_vertex_seq_of c & (vs . 1) = v1 & (vs . ( len vs)) = v9;

            thus contradiction

            proof

              per cases by A17;

                suppose

                 A18: v9 = v1;

                reconsider ec = <*e*> as Chain of G by A7, A9, MSSCYC_1: 5;

                reconsider vs = <*v1, Te*> as FinSequence of the carrier of G;

                ( len vs) = 2 by FINSEQ_1: 44;

                then

                 A19: (vs . 1) = v1 & (vs . ( len vs)) = Te by FINSEQ_1: 44;

                vs is_vertex_seq_of ec by A10, A11, A16, A18, MSSCYC_1: 4;

                hence contradiction by A14, A19;

              end;

                suppose ex c be Chain of G, vs be FinSequence of the carrier of G st c is non empty & vs is_vertex_seq_of c & (vs . 1) = v1 & (vs . ( len vs)) = v9;

                then

                consider c be Chain of G, vs be FinSequence of the carrier of G such that c is non empty and

                 A20: vs is_vertex_seq_of c and

                 A21: (vs . 1) = v1 and

                 A22: (vs . ( len vs)) = v9;

                reconsider c9 = (c ^ <*e*>) as Chain of G by A7, A9, A10, A11, A16, A20, A22, Th12;

                ex vs9 be FinSequence of the carrier of G st vs9 = (vs ^' <*(S . e), (T . e)*>) & vs9 is_vertex_seq_of c9 & (vs9 . 1) = (vs . 1) & (vs9 . ( len vs9)) = Te by A7, A9, A10, A11, A16, A20, A22, Th12;

                hence contradiction by A14, A21;

              end;

            end;

          end;

        end;

        then

        reconsider S2 = (S | E2) as Function of E2, V2 by A7, FUNCT_2:def 1, RELSET_1: 4;

        

         A23: ( dom T) = E by FUNCT_2:def 1;

        

         A24: ( dom (T | E2)) = (( dom T) /\ E2) by RELAT_1: 61

        .= E2 by A23, XBOOLE_1: 28;

        

         A25: ( rng T) c= V by RELAT_1:def 19;

        ( rng (T | E2)) c= V2

        proof

          let v be object;

          assume v in ( rng (T | E2));

          then

          consider e be object such that

           A26: e in ( dom (T | E2)) and

           A27: ((T | E2) . e) = v by FUNCT_1:def 3;

          reconsider e as Element of the carrier' of G by A24, A26;

          

           A28: ((T | E2) . e) = (T . e) by A26, FUNCT_1: 47;

          

           A29: not e in E1 by A24, A26, XBOOLE_0:def 5;

          per cases by A5, A29;

            suppose not e in E;

            hence thesis by A24, A26;

          end;

            suppose

             A30: not (the Target of G . e) in V1;

            (T . e) in V by A24, A26, FUNCT_2: 5;

            hence thesis by A27, A28, A30, XBOOLE_0:def 5;

          end;

            suppose

             A31: not (the Source of G . e) in V1;

            reconsider Se = (S . e) as Vertex of G by A24, A26, FUNCT_2: 5;

            v in ( rng (T | E2)) & ( rng (T | E2)) c= ( rng T) by A26, A27, FUNCT_1:def 3, RELAT_1: 70;

            then

             A32: v in ( rng T);

            assume not v in V2;

            then v in V1 by A25, A32, XBOOLE_0:def 5;

            then

            consider v9 be Vertex of G such that

             A33: v9 = v and

             A34: v9 = v1 or ex c be Chain of G, vs be FinSequence of the carrier of G st c is non empty & vs is_vertex_seq_of c & (vs . 1) = v1 & (vs . ( len vs)) = v9;

            thus contradiction

            proof

              per cases by A34;

                suppose

                 A35: v9 = v1;

                reconsider ec = <*e*> as Chain of G by A24, A26, MSSCYC_1: 5;

                reconsider vs = <*v1, Se*> as FinSequence of the carrier of G;

                ( len vs) = 2 by FINSEQ_1: 44;

                then

                 A36: (vs . 1) = v1 & (vs . ( len vs)) = Se by FINSEQ_1: 44;

                vs is_vertex_seq_of ec by A27, A28, A33, A35, Th11;

                hence contradiction by A31, A36;

              end;

                suppose ex c be Chain of G, vs be FinSequence of the carrier of G st c is non empty & vs is_vertex_seq_of c & (vs . 1) = v1 & (vs . ( len vs)) = v9;

                then

                consider c be Chain of G, vs be FinSequence of the carrier of G such that c is non empty and

                 A37: vs is_vertex_seq_of c and

                 A38: (vs . 1) = v1 and

                 A39: (vs . ( len vs)) = v9;

                reconsider c9 = (c ^ <*e*>) as Chain of G by A24, A26, A27, A28, A33, A37, A39, Th13;

                ex vs9 be FinSequence of the carrier of G st vs9 = (vs ^' <*(T . e), (S . e)*>) & vs9 is_vertex_seq_of c9 & (vs9 . 1) = (vs . 1) & (vs9 . ( len vs9)) = Se by A24, A26, A27, A28, A33, A37, A39, Th13;

                hence contradiction by A31, A38;

              end;

            end;

          end;

        end;

        then

        reconsider T2 = (T | E2) as Function of E2, V2 by A24, FUNCT_2:def 1, RELSET_1: 4;

        

         A40: E1 c= E by A5;

        

         A41: ( dom (T | E1)) = (( dom T) /\ E1) by RELAT_1: 61

        .= (E /\ E1) by FUNCT_2:def 1

        .= E1 by A40, XBOOLE_1: 28;

        ( rng (T | E1)) c= V1

        proof

          let v be object;

          assume v in ( rng (T | E1));

          then

          consider e be object such that

           A42: e in ( dom (T | E1)) and

           A43: ((T | E1) . e) = v by FUNCT_1:def 3;

          ((T | E1) . e) = (T . e) by A42, FUNCT_1: 47;

          hence thesis by A5, A41, A42, A43;

        end;

        then

        reconsider T1 = (T | E1) as Function of E1, V1 by A41, FUNCT_2:def 1, RELSET_1: 4;

        

         A44: ( dom (S | E1)) = (( dom S) /\ E1) by RELAT_1: 61

        .= (E /\ E1) by FUNCT_2:def 1

        .= E1 by A40, XBOOLE_1: 28;

        ( rng (S | E1)) c= V1

        proof

          let v be object;

          assume v in ( rng (S | E1));

          then

          consider e be object such that

           A45: e in ( dom (S | E1)) and

           A46: ((S | E1) . e) = v by FUNCT_1:def 3;

          ((S | E1) . e) = (S . e) by A45, FUNCT_1: 47;

          hence thesis by A5, A44, A45, A46;

        end;

        then

        reconsider S1 = (S | E1) as Function of E1, V1 by A44, FUNCT_2:def 1, RELSET_1: 4;

        reconsider G1 = MultiGraphStruct (# V1, E1, S1, T1 #), G2 = MultiGraphStruct (# V2, E2, S2, T2 #) as Graph;

        

         A47: G is_sum_of (G1,G2)

        proof

          reconsider MG = the MultiGraphStruct of G as strict Graph;

          thus

           A48: the Target of G1 tolerates the Target of G2

          proof

            let x be object;

            assume

             A49: x in (( dom the Target of G1) /\ ( dom the Target of G2));

            then x in ( dom the Target of G2) by XBOOLE_0:def 4;

            then

             A50: x in E2 by FUNCT_2:def 1;

            x in ( dom the Target of G1) by A49, XBOOLE_0:def 4;

            then x in E1 by FUNCT_2:def 1;

            hence thesis by A50, XBOOLE_0:def 5;

          end;

          thus

           A51: the Source of G1 tolerates the Source of G2

          proof

            let x be object;

            assume

             A52: x in (( dom the Source of G1) /\ ( dom the Source of G2));

            then x in ( dom the Source of G2) by XBOOLE_0:def 4;

            then

             A53: x in E2 by FUNCT_2:def 1;

            x in ( dom the Source of G1) by A52, XBOOLE_0:def 4;

            then x in E1 by FUNCT_2:def 1;

            hence thesis by A53, XBOOLE_0:def 5;

          end;

          

           A54: (for v be set st v in the carrier' of G1 holds (the Source of MG . v) = (the Source of G1 . v) & (the Target of MG . v) = (the Target of G1 . v)) & for v be set st v in the carrier' of G2 holds (the Source of MG . v) = (the Source of G2 . v) & (the Target of MG . v) = (the Target of G2 . v) by FUNCT_1: 49;

          the carrier of MG = (the carrier of G1 \/ the carrier of G2) & the carrier' of MG = (the carrier' of G1 \/ the carrier' of G2) by A4, A40, XBOOLE_1: 45;

          hence thesis by A48, A51, A54, GRAPH_1:def 5;

        end;

        V1 misses V2 by XBOOLE_1: 79;

        hence contradiction by A1, A47;

      end;

      assume

       A55: for v1,v2 be Vertex of G st v1 <> v2 holds ex c be Chain of G, vs be FinSequence of the carrier of G st c is non empty & vs is_vertex_seq_of c & (vs . 1) = v1 & (vs . ( len vs)) = v2;

      thus G is connected

      proof

        given G1,G2 be Graph such that

         A56: the carrier of G1 misses the carrier of G2 and

         A57: G is_sum_of (G1,G2);

        set v2 = the Vertex of G2;

        set v1 = the Vertex of G1;

        set V2 = the carrier of G2;

        set V1 = the carrier of G1;

        set T2 = the Target of G2;

        set T1 = the Target of G1;

        set S2 = the Source of G2;

        set S1 = the Source of G1;

        set E1 = the carrier' of G1;

        

         A58: the MultiGraphStruct of G = (G1 \/ G2) by A57;

        

         A59: T1 tolerates T2 & S1 tolerates S2 by A57;

        then

         A60: E = (E1 \/ the carrier' of G2) by A58, GRAPH_1:def 5;

        the carrier of the MultiGraphStruct of G = (V1 \/ V2) by A59, A58, GRAPH_1:def 5;

        then

        reconsider v19 = v1, v29 = v2 as Vertex of G by XBOOLE_0:def 3;

        

         A61: (the carrier of G1 /\ the carrier of G2) = {} by A56;

        then v1 <> v2 by XBOOLE_0:def 4;

        then

        consider c be Chain of G, vs be FinSequence of the carrier of G such that c is non empty and

         A62: vs is_vertex_seq_of c and

         A63: (vs . 1) = v19 and

         A64: (vs . ( len vs)) = v29 by A55;

        defpred P[ Nat] means $1 in ( dom vs) & (vs . $1) is Vertex of G2;

        

         A65: ( len vs) = (( len c) + 1) by A62;

        c is FinSequence of E by MSSCYC_1:def 1;

        then

         A66: ( rng c) c= E by FINSEQ_1:def 4;

        1 <= (( len c) + 1) by NAT_1: 11;

        then ( len vs) in ( dom vs) by A65, FINSEQ_3: 25;

        then

         A67: ex k be Nat st P[k] by A64;

        consider k be Nat such that

         A68: P[k] and

         A69: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A67);

        

         A70: 1 <= k by A68, FINSEQ_3: 25;

        k <> 1 by A61, A63, A68, XBOOLE_0:def 4;

        then 1 < k by A70, XXREAL_0: 1;

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

        then

        consider i be Nat such that

         A71: 1 <= i and

         A72: i < k and

         A73: k = (i + 1) by FINSEQ_6: 127;

        set e = (c . i);

        

         A74: k <= ( len vs) by A68, FINSEQ_3: 25;

        then

         A75: i <= ( len c) by A65, A73, XREAL_1: 6;

        then i in ( dom c) by A71, FINSEQ_3: 25;

        then

         A76: e in ( rng c) by FUNCT_1:def 3;

        i <= ( len vs) by A72, A74, XXREAL_0: 2;

        then

         A77: i in ( dom vs) by A71, FINSEQ_3: 25;

        per cases by A60, A66, A76, XBOOLE_0:def 3;

          suppose

           A78: e in E1;

          then

           A79: (T1 . e) in V1 by FUNCT_2: 5;

          

           A80: (S1 . e) in V1 by A78, FUNCT_2: 5;

          thus contradiction

          proof

            per cases by A62, A71, A75, Lm3;

              suppose (vs . i) = (T . e) & (vs . (i + 1)) = (S . e);

              then (vs . k) in V1 by A59, A58, A73, A78, A80, GRAPH_1:def 5;

              hence contradiction by A61, A68, XBOOLE_0:def 4;

            end;

              suppose (vs . i) = (S . e) & (vs . (i + 1)) = (T . e);

              then (vs . k) in V1 by A59, A58, A73, A78, A79, GRAPH_1:def 5;

              hence contradiction by A61, A68, XBOOLE_0:def 4;

            end;

          end;

        end;

          suppose

           A81: e in the carrier' of G2;

          then

           A82: (T2 . e) in V2 by FUNCT_2: 5;

          

           A83: (S2 . e) in V2 by A81, FUNCT_2: 5;

          thus contradiction

          proof

            per cases by A62, A71, A75, Lm3;

              suppose (vs . i) = (T . e) & (vs . (i + 1)) = (S . e);

              then (vs . i) in V2 by A59, A58, A81, A82, GRAPH_1:def 5;

              hence contradiction by A69, A72, A77;

            end;

              suppose (vs . i) = (S . e) & (vs . (i + 1)) = (T . e);

              then (vs . i) in V2 by A59, A58, A81, A83, GRAPH_1:def 5;

              hence contradiction by A69, A72, A77;

            end;

          end;

        end;

      end;

    end;

    theorem :: GRAPH_3:19

    

     Th19: for G be connected Graph, X be set, v be Vertex of G st X meets the carrier' of G & not v in (G -VSet X) holds ex v9 be Vertex of G, e be Element of the carrier' of G st v9 in (G -VSet X) & not e in X & (v9 = (the Target of G . e) or v9 = (the Source of G . e))

    proof

      let G be connected Graph, X be set, v be Vertex of G;

      assume that

       A1: X meets the carrier' of G and

       A2: not v in (G -VSet X);

      ex e be object st e in X & e in the carrier' of G by A1, XBOOLE_0: 3;

      then (G -VSet X) is non empty by Th17;

      then

      consider vv be object such that

       A3: vv in (G -VSet X);

      reconsider vv as Vertex of G by A3;

      consider c be Chain of G, vs be FinSequence of the carrier of G such that

       A4: c is non empty and

       A5: vs is_vertex_seq_of c and

       A6: (vs . 1) = vv and

       A7: (vs . ( len vs)) = v by A2, A3, Th18;

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len c) & not (vs . ($1 + 1)) in (G -VSet X);

      

       A8: ( len vs) = (( len c) + 1) by A5;

      (1 + 0 ) <= ( len c) by A4, NAT_1: 13;

      then

       A9: ex n be Nat st P[n] by A2, A7, A8;

      consider k be Nat such that

       A10: P[k] and

       A11: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A9);

      ( len c) <= (( len c) + 1) by NAT_1: 11;

      then k <= ( len vs) by A8, A10, XXREAL_0: 2;

      then k in ( dom vs) by A10, FINSEQ_3: 25;

      then

      reconsider v9 = (vs . k) as Vertex of G by FINSEQ_2: 11;

      reconsider c as FinSequence of the carrier' of G by MSSCYC_1:def 1;

      

       A12: ( rng c) c= the carrier' of G by FINSEQ_1:def 4;

      k in ( dom c) by A10, FINSEQ_3: 25;

      then (c . k) in ( rng c) by FUNCT_1:def 3;

      then

      reconsider e = (c . k) as Element of the carrier' of G by A12;

      take v9;

      take e;

      hereby

        per cases by A10, XXREAL_0: 1;

          suppose k = 1;

          hence v9 in (G -VSet X) by A3, A6;

        end;

          suppose

           A13: 1 < k;

          assume

           A14: not v9 in (G -VSet X);

          consider p be Element of NAT such that

           A15: k = (1 + p) and

           A16: 1 <= p by A13, FINSEQ_4: 84;

          p <= k by A15, NAT_1: 11;

          then p <= ( len c) by A10, XXREAL_0: 2;

          then k <= p by A11, A15, A16, A14;

          hence contradiction by A15, NAT_1: 13;

        end;

      end;

      hereby

        1 <= (k + 1) & (k + 1) <= ( len vs) by A8, A10, NAT_1: 11, XREAL_1: 6;

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

        then

        reconsider v99 = (vs . (k + 1)) as Vertex of G by FINSEQ_2: 11;

        assume

         A17: e in X;

        v99 = (the Target of G . e) or v99 = (the Source of G . e) by A5, A10, Lm3;

        hence contradiction by A10, A17;

      end;

      thus thesis by A5, A10, Lm3;

    end;

    begin

    definition

      let G be Graph, v be Vertex of G, X be set;

      :: GRAPH_3:def1

      func Edges_In (v,X) -> Subset of the carrier' of G means

      : Def1: for e be set holds e in it iff e in the carrier' of G & e in X & (the Target of G . e) = v;

      existence

      proof

        defpred P[ object] means $1 in X & (the Target of G . $1) = v;

        consider IT be set such that

         A1: for x be object holds x in IT iff x in the carrier' of G & P[x] from XBOOLE_0:sch 1;

        take IT;

        for x be object st x in IT holds x in the carrier' of G by A1;

        hence IT is Subset of the carrier' of G by TARSKI:def 3;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be Subset of the carrier' of G such that

         A2: for e be set holds e in it1 iff e in the carrier' of G & e in X & (the Target of G . e) = v and

         A3: for e be set holds e in it2 iff e in the carrier' of G & e in X & (the Target of G . e) = v;

        now

          let e be object;

          e in it1 iff e in the carrier' of G & e in X & (the Target of G . e) = v by A2;

          hence e in it1 iff e in it2 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

      :: GRAPH_3:def2

      func Edges_Out (v,X) -> Subset of the carrier' of G means

      : Def2: for e be set holds e in it iff e in the carrier' of G & e in X & (the Source of G . e) = v;

      existence

      proof

        defpred P[ object] means $1 in X & (the Source of G . $1) = v;

        consider IT be set such that

         A4: for x be object holds x in IT iff x in the carrier' of G & P[x] from XBOOLE_0:sch 1;

        take IT;

        for x be object st x in IT holds x in the carrier' of G by A4;

        hence IT is Subset of the carrier' of G by TARSKI:def 3;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let it1,it2 be Subset of the carrier' of G such that

         A5: for e be set holds e in it1 iff e in the carrier' of G & e in X & (the Source of G . e) = v and

         A6: for e be set holds e in it2 iff e in the carrier' of G & e in X & (the Source of G . e) = v;

        now

          let e be object;

          e in it1 iff e in the carrier' of G & e in X & (the Source of G . e) = v by A5;

          hence e in it1 iff e in it2 by A6;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let G be Graph, v be Vertex of G, X be set;

      :: GRAPH_3:def3

      func Edges_At (v,X) -> Subset of the carrier' of G equals (( Edges_In (v,X)) \/ ( Edges_Out (v,X)));

      correctness ;

    end

    registration

      let G be finite Graph, v be Vertex of G, X be set;

      cluster ( Edges_In (v,X)) -> finite;

      correctness

      proof

        the carrier' of G is finite by GRAPH_1:def 11;

        hence thesis;

      end;

      cluster ( Edges_Out (v,X)) -> finite;

      correctness

      proof

        the carrier' of G is finite by GRAPH_1:def 11;

        hence thesis;

      end;

      cluster ( Edges_At (v,X)) -> finite;

      correctness ;

    end

    registration

      let G be Graph, v be Vertex of G, X be empty set;

      cluster ( Edges_In (v,X)) -> empty;

      correctness by Def1;

      cluster ( Edges_Out (v,X)) -> empty;

      correctness by Def2;

      cluster ( Edges_At (v,X)) -> empty;

      correctness ;

    end

    definition

      let G be Graph, v be Vertex of G;

      :: GRAPH_3:def4

      func Edges_In v -> Subset of the carrier' of G equals ( Edges_In (v,the carrier' of G));

      correctness ;

      :: GRAPH_3:def5

      func Edges_Out v -> Subset of the carrier' of G equals ( Edges_Out (v,the carrier' of G));

      correctness ;

    end

    theorem :: GRAPH_3:20

    

     Th20: ( Edges_In (v,X)) c= ( Edges_In v)

    proof

      let e be object;

      assume

       A1: e in ( Edges_In (v,X));

      then (the Target of G . e) = v by Def1;

      hence thesis by A1, Def1;

    end;

    theorem :: GRAPH_3:21

    

     Th21: ( Edges_Out (v,X)) c= ( Edges_Out v)

    proof

      let e be object;

      assume

       A1: e in ( Edges_Out (v,X));

      then (the Source of G . e) = v by Def2;

      hence thesis by A1, Def2;

    end;

    registration

      let G be finite Graph, v be Vertex of G;

      cluster ( Edges_In v) -> finite;

      correctness ;

      cluster ( Edges_Out v) -> finite;

      correctness ;

    end

    reserve G for finite Graph,

v for Vertex of G,

c for Chain of G,

vs for FinSequence of the carrier of G,

X1,X2 for set;

    theorem :: GRAPH_3:22

    

     Th22: ( card ( Edges_In v)) = ( EdgesIn v)

    proof

      consider X be finite set such that

       A1: for z be set holds z in X iff z in the carrier' of G & (the Target of G . z) = v and

       A2: ( EdgesIn v) = ( card X) by GRAPH_1:def 21;

      now

        let e be object;

        e in ( Edges_In (v,the carrier' of G)) iff e in the carrier' of G & (the Target of G . e) = v by Def1;

        hence e in ( Edges_In v) iff e in X by A1;

      end;

      hence thesis by A2, TARSKI: 2;

    end;

    theorem :: GRAPH_3:23

    

     Th23: ( card ( Edges_Out v)) = ( EdgesOut v)

    proof

      consider X be finite set such that

       A1: for z be set holds z in X iff z in the carrier' of G & (the Source of G . z) = v and

       A2: ( EdgesOut v) = ( card X) by GRAPH_1:def 22;

      now

        let e be object;

        e in ( Edges_Out (v,the carrier' of G)) iff e in the carrier' of G & (the Source of G . e) = v by Def2;

        hence e in ( Edges_Out v) iff e in X by A1;

      end;

      hence thesis by A2, TARSKI: 2;

    end;

    definition

      let G be finite Graph, v be Vertex of G, X be set;

      :: GRAPH_3:def6

      func Degree (v,X) -> Element of NAT equals (( card ( Edges_In (v,X))) + ( card ( Edges_Out (v,X))));

      correctness ;

    end

    theorem :: GRAPH_3:24

    

     Th24: ( Degree v) = ( Degree (v,the carrier' of G))

    proof

      

      thus ( Degree v) = (( card ( Edges_In v)) + ( EdgesOut v)) by Th22

      .= (( card ( Edges_In (v,the carrier' of G))) + ( card ( Edges_Out v))) by Th23

      .= ( Degree (v,the carrier' of G));

    end;

    theorem :: GRAPH_3:25

    

     Th25: ( Degree (v,X)) <> 0 implies ( Edges_At (v,X)) is non empty

    proof

      assume

       A1: ( Degree (v,X)) <> 0 ;

      assume

       A2: not thesis;

      then ( Edges_In (v,X)) = {} ;

      hence contradiction by A1, A2;

    end;

    theorem :: GRAPH_3:26

    

     Th26: e in the carrier' of G & not e in X & (v = (the Target of G . e) or v = (the Source of G . e)) implies ( Degree v) <> ( Degree (v,X))

    proof

      set T = the Target of G, S = the Source of G, E = the carrier' of G;

      assume that

       A1: e in E and

       A2: not e in X and

       A3: v = (T . e) or v = (S . e);

      

       A4: ( Degree v) = ( Degree (v,E)) by Th24;

      ( Edges_Out v) = ( Edges_Out (v,E));

      then

       A5: ( Edges_Out (v,X)) c= ( Edges_Out (v,E)) by Th21;

      ( Edges_In v) = ( Edges_In (v,E));

      then

       A6: ( Edges_In (v,X)) c= ( Edges_In (v,E)) by Th20;

      per cases by A3;

        suppose

         A7: v = (T . e);

        

         A8: not e in ( Edges_In (v,X)) by A2, Def1;

        e in ( Edges_In (v,E)) by A1, A7, Def1;

        then ( Edges_In (v,X)) c< ( Edges_In (v,E)) by A6, A8;

        then ( card ( Edges_In (v,X))) < ( card ( Edges_In (v,E))) by CARD_2: 48;

        hence thesis by A4, A5, NAT_1: 43, XREAL_1: 8;

      end;

        suppose

         A9: v = (S . e);

        

         A10: not e in ( Edges_Out (v,X)) by A2, Def2;

        e in ( Edges_Out (v,E)) by A1, A9, Def2;

        then ( Edges_Out (v,X)) c< ( Edges_Out (v,E)) by A5, A10;

        then ( card ( Edges_Out (v,X))) < ( card ( Edges_Out (v,E))) by CARD_2: 48;

        hence thesis by A4, A6, NAT_1: 43, XREAL_1: 8;

      end;

    end;

    theorem :: GRAPH_3:27

    

     Th27: X2 c= X1 implies ( card ( Edges_In (v,(X1 \ X2)))) = (( card ( Edges_In (v,X1))) - ( card ( Edges_In (v,X2))))

    proof

      assume

       A1: X2 c= X1;

      then

       A2: X1 = (X2 \/ (X1 \ X2)) by XBOOLE_1: 45;

      now

        let x be object;

        hereby

          assume

           A3: x in ( Edges_In (v,X1));

          then x in X1 by Def1;

          then

           A4: x in X2 or x in (X1 \ X2) by A2, XBOOLE_0:def 3;

          (the Target of G . x) = v by A3, Def1;

          then x in ( Edges_In (v,X2)) or x in ( Edges_In (v,(X1 \ X2))) by A3, A4, Def1;

          hence x in (( Edges_In (v,X2)) \/ ( Edges_In (v,(X1 \ X2)))) by XBOOLE_0:def 3;

        end;

        assume

         A5: x in (( Edges_In (v,X2)) \/ ( Edges_In (v,(X1 \ X2))));

        then

         A6: x in ( Edges_In (v,X2)) or x in ( Edges_In (v,(X1 \ X2))) by XBOOLE_0:def 3;

        then

         A7: x in X2 or x in (X1 \ X2) by Def1;

        (the Target of G . x) = v by A6, Def1;

        hence x in ( Edges_In (v,X1)) by A1, A5, A7, Def1;

      end;

      then

       A8: ( Edges_In (v,X1)) = (( Edges_In (v,X2)) \/ ( Edges_In (v,(X1 \ X2)))) by TARSKI: 2;

      ( Edges_In (v,X2)) misses ( Edges_In (v,(X1 \ X2)))

      proof

        assume not thesis;

        then

        consider x be object such that

         A9: x in (( Edges_In (v,X2)) /\ ( Edges_In (v,(X1 \ X2)))) by XBOOLE_0: 4;

        x in ( Edges_In (v,(X1 \ X2))) by A9, XBOOLE_0:def 4;

        then

         A10: x in (X1 \ X2) by Def1;

        x in ( Edges_In (v,X2)) by A9, XBOOLE_0:def 4;

        then x in X2 by Def1;

        hence contradiction by A10, XBOOLE_0:def 5;

      end;

      then ( card ( Edges_In (v,X1))) = (( card ( Edges_In (v,X2))) + ( card ( Edges_In (v,(X1 \ X2))))) by A8, CARD_2: 40;

      hence thesis;

    end;

    theorem :: GRAPH_3:28

    

     Th28: X2 c= X1 implies ( card ( Edges_Out (v,(X1 \ X2)))) = (( card ( Edges_Out (v,X1))) - ( card ( Edges_Out (v,X2))))

    proof

      assume

       A1: X2 c= X1;

      then

       A2: X1 = (X2 \/ (X1 \ X2)) by XBOOLE_1: 45;

      now

        let x be object;

        hereby

          assume

           A3: x in ( Edges_Out (v,X1));

          then x in X1 by Def2;

          then

           A4: x in X2 or x in (X1 \ X2) by A2, XBOOLE_0:def 3;

          (the Source of G . x) = v by A3, Def2;

          then x in ( Edges_Out (v,X2)) or x in ( Edges_Out (v,(X1 \ X2))) by A3, A4, Def2;

          hence x in (( Edges_Out (v,X2)) \/ ( Edges_Out (v,(X1 \ X2)))) by XBOOLE_0:def 3;

        end;

        assume

         A5: x in (( Edges_Out (v,X2)) \/ ( Edges_Out (v,(X1 \ X2))));

        then

         A6: x in ( Edges_Out (v,X2)) or x in ( Edges_Out (v,(X1 \ X2))) by XBOOLE_0:def 3;

        then

         A7: x in X2 or x in (X1 \ X2) by Def2;

        (the Source of G . x) = v by A6, Def2;

        hence x in ( Edges_Out (v,X1)) by A1, A5, A7, Def2;

      end;

      then

       A8: ( Edges_Out (v,X1)) = (( Edges_Out (v,X2)) \/ ( Edges_Out (v,(X1 \ X2)))) by TARSKI: 2;

      ( Edges_Out (v,X2)) misses ( Edges_Out (v,(X1 \ X2)))

      proof

        assume not thesis;

        then

        consider x be object such that

         A9: x in (( Edges_Out (v,X2)) /\ ( Edges_Out (v,(X1 \ X2)))) by XBOOLE_0: 4;

        x in ( Edges_Out (v,(X1 \ X2))) by A9, XBOOLE_0:def 4;

        then

         A10: x in (X1 \ X2) by Def2;

        x in ( Edges_Out (v,X2)) by A9, XBOOLE_0:def 4;

        then x in X2 by Def2;

        hence contradiction by A10, XBOOLE_0:def 5;

      end;

      then ( card ( Edges_Out (v,X1))) = (( card ( Edges_Out (v,X2))) + ( card ( Edges_Out (v,(X1 \ X2))))) by A8, CARD_2: 40;

      hence thesis;

    end;

    theorem :: GRAPH_3:29

    

     Th29: X2 c= X1 implies ( Degree (v,(X1 \ X2))) = (( Degree (v,X1)) - ( Degree (v,X2)))

    proof

      assume X2 c= X1;

      then ( card ( Edges_In (v,(X1 \ X2)))) = (( card ( Edges_In (v,X1))) - ( card ( Edges_In (v,X2)))) & ( card ( Edges_Out (v,(X1 \ X2)))) = (( card ( Edges_Out (v,X1))) - ( card ( Edges_Out (v,X2)))) by Th27, Th28;

      hence thesis;

    end;

    theorem :: GRAPH_3:30

    

     Th30: ( Edges_In (v,X)) = ( Edges_In (v,(X /\ the carrier' of G))) & ( Edges_Out (v,X)) = ( Edges_Out (v,(X /\ the carrier' of G)))

    proof

      set E = the carrier' of G;

      now

        let x be object;

        hereby

          assume

           A1: x in ( Edges_In (v,X));

          then x in X by Def1;

          then

           A2: x in (X /\ E) by A1, XBOOLE_0:def 4;

          (the Target of G . x) = v by A1, Def1;

          hence x in ( Edges_In (v,(X /\ E))) by A1, A2, Def1;

        end;

        assume

         A3: x in ( Edges_In (v,(X /\ E)));

        then x in (X /\ E) by Def1;

        then

         A4: x in X by XBOOLE_0:def 4;

        (the Target of G . x) = v by A3, Def1;

        hence x in ( Edges_In (v,X)) by A3, A4, Def1;

      end;

      hence ( Edges_In (v,X)) = ( Edges_In (v,(X /\ the carrier' of G))) by TARSKI: 2;

      now

        let x be object;

        hereby

          assume

           A5: x in ( Edges_Out (v,X));

          then x in X by Def2;

          then

           A6: x in (X /\ E) by A5, XBOOLE_0:def 4;

          (the Source of G . x) = v by A5, Def2;

          hence x in ( Edges_Out (v,(X /\ E))) by A5, A6, Def2;

        end;

        assume

         A7: x in ( Edges_Out (v,(X /\ E)));

        then x in (X /\ E) by Def2;

        then

         A8: x in X by XBOOLE_0:def 4;

        (the Source of G . x) = v by A7, Def2;

        hence x in ( Edges_Out (v,X)) by A7, A8, Def2;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GRAPH_3:31

    

     Th31: ( Degree (v,X)) = ( Degree (v,(X /\ the carrier' of G)))

    proof

      set E = the carrier' of G;

      

      thus ( Degree (v,X)) = (( card ( Edges_In (v,(X /\ E)))) + ( card ( Edges_Out (v,X)))) by Th30

      .= ( Degree (v,(X /\ the carrier' of G))) by Th30;

    end;

    theorem :: GRAPH_3:32

    

     Th32: c is non empty & vs is_vertex_seq_of c implies (v in ( rng vs) iff ( Degree (v,( rng c))) <> 0 )

    proof

      assume that

       A1: c is non empty and

       A2: vs is_vertex_seq_of c;

      hereby

        c is FinSequence of the carrier' of G by MSSCYC_1:def 1;

        then

         A3: ( rng c) c= the carrier' of G by FINSEQ_1:def 4;

        assume that

         A4: v in ( rng vs) and

         A5: ( Degree (v,( rng c))) = 0 ;

        

         A6: ( Edges_In (v,( rng c))) = {} & ( Edges_Out (v,( rng c))) = {} by A5;

        

         A7: ( 0 + 1) <= ( len c) by A1, NAT_1: 13;

        

         A8: ( len vs) = (( len c) + 1) by A2;

        consider i be Nat such that

         A9: i in ( dom vs) and

         A10: (vs . i) = v by A4, FINSEQ_2: 10;

        

         A11: 1 <= i by A9, FINSEQ_3: 25;

        

         A12: i <= ( len vs) by A9, FINSEQ_3: 25;

        per cases by A12, XXREAL_0: 1;

          suppose

           A13: i = ( len vs);

          set ic = ( len c);

          ic in ( dom c) by A7, FINSEQ_3: 25;

          then

           A14: (c . ic) in ( rng c) by FUNCT_1:def 3;

          (vs . ( len vs)) = (the Target of G . (c . ( len c))) or (vs . ( len vs)) = (the Source of G . (c . ( len c))) by A2, A7, Lm3;

          hence contradiction by A6, A10, A3, A13, A14, Def1, Def2;

        end;

          suppose i < ( len vs);

          then

           A15: i <= ( len c) by A8, NAT_1: 13;

          then i in ( dom c) by A11, FINSEQ_3: 25;

          then

           A16: (c . i) in ( rng c) by FUNCT_1:def 3;

          (vs . i) = (the Target of G . (c . i)) or (vs . i) = (the Source of G . (c . i)) by A2, A11, A15, Lm3;

          hence contradiction by A6, A10, A3, A16, Def1, Def2;

        end;

      end;

      assume that

       A17: ( Degree (v,( rng c))) <> 0 and

       A18: not v in ( rng vs);

      per cases by A17;

        suppose ( card ( Edges_In (v,( rng c)))) <> 0 ;

        then

        consider e be object such that

         A19: e in ( Edges_In (v,( rng c))) by CARD_1: 27, XBOOLE_0:def 1;

        

         A20: (the Target of G . e) = v by A19, Def1;

        e in ( rng c) by A19, Def1;

        then

        consider i be Nat such that

         A21: i in ( dom c) and

         A22: (c . i) = e by FINSEQ_2: 10;

        

         A23: 1 <= i by A21, FINSEQ_3: 25;

        

         A24: i <= ( len c) by A21, FINSEQ_3: 25;

        then 1 <= (i + 1) & (i + 1) <= ( len vs) by A2, A23, Lm3;

        then

         A25: (i + 1) in ( dom vs) by FINSEQ_3: 25;

        i <= ( len vs) by A2, A23, A24, Lm3;

        then

         A26: i in ( dom vs) by A23, FINSEQ_3: 25;

        (vs . i) = (the Target of G . (c . i)) & (vs . (i + 1)) = (the Source of G . (c . i)) or (vs . i) = (the Source of G . (c . i)) & (vs . (i + 1)) = (the Target of G . (c . i)) by A2, A23, A24, Lm3;

        hence contradiction by A18, A20, A22, A26, A25, FUNCT_1:def 3;

      end;

        suppose ( card ( Edges_Out (v,( rng c)))) <> 0 ;

        then

        consider e be object such that

         A27: e in ( Edges_Out (v,( rng c))) by CARD_1: 27, XBOOLE_0:def 1;

        

         A28: (the Source of G . e) = v by A27, Def2;

        e in ( rng c) by A27, Def2;

        then

        consider i be Nat such that

         A29: i in ( dom c) and

         A30: (c . i) = e by FINSEQ_2: 10;

        

         A31: 1 <= i by A29, FINSEQ_3: 25;

        

         A32: i <= ( len c) by A29, FINSEQ_3: 25;

        then 1 <= (i + 1) & (i + 1) <= ( len vs) by A2, A31, Lm3;

        then

         A33: (i + 1) in ( dom vs) by FINSEQ_3: 25;

        i <= ( len vs) by A2, A31, A32, Lm3;

        then

         A34: i in ( dom vs) by A31, FINSEQ_3: 25;

        (vs . i) = (the Target of G . (c . i)) & (vs . (i + 1)) = (the Source of G . (c . i)) or (vs . i) = (the Source of G . (c . i)) & (vs . (i + 1)) = (the Target of G . (c . i)) by A2, A31, A32, Lm3;

        hence contradiction by A18, A28, A30, A34, A33, FUNCT_1:def 3;

      end;

    end;

    theorem :: GRAPH_3:33

    

     Th33: for G be non void finite connected Graph, v be Vertex of G holds ( Degree v) <> 0

    proof

      let G be non void finite connected Graph, v be Vertex of G;

      assume

       A1: ( Degree v) = 0 ;

      set E = the carrier' of G;

      

       A2: ( Degree v) = ( Degree (v,E)) by Th24

      .= (( card ( Edges_In (v,E))) + ( card ( Edges_Out (v,E))));

      then

       A3: ( Edges_In (v,E)) = {} by A1;

      

       A4: ( Edges_Out (v,E)) = {} by A1, A2;

      set S = the Source of G;

      set T = the Target of G;

      consider e be object such that

       A5: e in E by XBOOLE_0:def 1;

      reconsider s = (S . e) as Vertex of G by A5, FUNCT_2: 5;

      per cases ;

        suppose v = s;

        hence contradiction by A4, A5, Def2;

      end;

        suppose v <> s;

        then

        consider c be Chain of G, vs be FinSequence of the carrier of G such that

         A6: c is non empty and

         A7: vs is_vertex_seq_of c and

         A8: (vs . 1) = v and (vs . ( len vs)) = s by Th18;

        

         A9: ( 0 + 1) <= ( len c) by A6, NAT_1: 13;

        then 1 in ( dom c) by FINSEQ_3: 25;

        then

         A10: (c . 1) in ( rng c) by FUNCT_1:def 3;

        c is FinSequence of the carrier' of G by MSSCYC_1:def 1;

        then

         A11: ( rng c) c= the carrier' of G by FINSEQ_1:def 4;

        (vs . 1) = (T . (c . 1)) or (vs . 1) = (S . (c . 1)) by A7, A9, Lm3;

        hence contradiction by A3, A4, A8, A11, A10, Def1, Def2;

      end;

    end;

    begin

    definition

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

      :: GRAPH_3:def7

      func AddNewEdge (v1,v2) -> strict Graph means

      : Def7: the carrier of it = the carrier of G & the carrier' of it = (the carrier' of G \/ {the carrier' of G}) & the Source of it = (the Source of G +* (the carrier' of G .--> v1)) & the Target of it = (the Target of G +* (the carrier' of G .--> v2));

      existence

      proof

        set T = the Target of G;

        set E = the carrier' of G;

        set V = the carrier of G;

        set Eit = (E \/ {E});

        set t = (E .--> v2);

        

         A1: {v1} c= V by ZFMISC_1: 31;

        set Tit = (T +* (E .--> v2));

        

         A3: {v2} c= V by ZFMISC_1: 31;

        ( rng t) = {v2} & ( rng T) c= V by FUNCOP_1: 8, RELAT_1:def 19;

        then ( rng Tit) c= (( rng T) \/ ( rng t)) & (( rng T) \/ ( rng t)) c= V by A3, FUNCT_4: 17, XBOOLE_1: 8;

        then

         A4: ( rng Tit) c= V;

        ( dom Tit) = (( dom T) \/ ( dom t)) by FUNCT_4:def 1

        .= Eit by FUNCT_2:def 1;

        then

        reconsider Tit as Function of Eit, V by A4, FUNCT_2:def 1, RELSET_1: 4;

        set S = the Source of G;

        set s = (E .--> v1);

        set Sit = (S +* (E .--> v1));

        

         A6: ( dom Sit) = (( dom S) \/ ( dom s)) by FUNCT_4:def 1

        .= Eit by FUNCT_2:def 1;

        ( rng s) = {v1} & ( rng S) c= V by FUNCOP_1: 8, RELAT_1:def 19;

        then ( rng Sit) c= (( rng S) \/ ( rng s)) & (( rng S) \/ ( rng s)) c= V by A1, FUNCT_4: 17, XBOOLE_1: 8;

        then ( rng Sit) c= V;

        then

        reconsider Sit as Function of Eit, V by A6, FUNCT_2:def 1, RELSET_1: 4;

        reconsider IT = MultiGraphStruct (# V, Eit, Sit, Tit #) as strict non empty MultiGraphStruct;

        take IT;

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let G be finite Graph, v1,v2 be Vertex of G;

      cluster ( AddNewEdge (v1,v2)) -> finite;

      coherence

      proof

        reconsider E = the carrier' of G as finite set by GRAPH_1:def 11;

        reconsider V = the carrier of G as finite set by GRAPH_1:def 11;

        the carrier of ( AddNewEdge (v1,v2)) = V by Def7;

        hence the carrier of ( AddNewEdge (v1,v2)) is finite;

        the carrier' of ( AddNewEdge (v1,v2)) = (E \/ {the carrier' of G}) by Def7;

        hence thesis;

      end;

    end

    reserve G for Graph,

v,v1,v2 for Vertex of G,

c for Chain of G,

p for Path of G,

vs for FinSequence of the carrier of G,

v9 for Vertex of ( AddNewEdge (v1,v2)),

p9 for Path of ( AddNewEdge (v1,v2)),

vs9 for FinSequence of the carrier of ( AddNewEdge (v1,v2));

    theorem :: GRAPH_3:34

    

     Th34: the carrier' of G in the carrier' of ( AddNewEdge (v1,v2)) & the carrier' of G = (the carrier' of ( AddNewEdge (v1,v2)) \ {the carrier' of G}) & (the Source of ( AddNewEdge (v1,v2)) . the carrier' of G) = v1 & (the Target of ( AddNewEdge (v1,v2)) . the carrier' of G) = v2

    proof

      set G9 = ( AddNewEdge (v1,v2));

      set E = the carrier' of G;

      set S = the Source of G;

      set T = the Target of G;

      set E9 = the carrier' of G9;

      

       A1: E9 = (E \/ {E}) by Def7;

      E in {E} by TARSKI:def 1;

      hence E in E9 by A1, XBOOLE_0:def 3;

      now

        let x be object;

        hereby

          assume

           A2: x in E;

          then

          reconsider x1 = x as set;

           not x1 in x1;

          then x <> E by A2;

          then

           A3: not x in {E} by TARSKI:def 1;

          x in E9 by A1, A2, XBOOLE_0:def 3;

          hence x in (E9 \ {E}) by A3, XBOOLE_0:def 5;

        end;

        assume

         A4: x in (E9 \ {E});

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

        hence x in E by A1, A4, XBOOLE_0:def 3;

      end;

      hence E = (E9 \ {E}) by TARSKI: 2;

      

       A5: E in ( dom (E .--> v1)) by TARSKI:def 1;

      the Source of G9 = (S +* (E .--> v1)) by Def7;

      

      hence (the Source of G9 . E) = ((E .--> v1) . E) by A5, FUNCT_4: 13

      .= v1 by FUNCOP_1: 72;

      

       A6: E in ( dom (E .--> v2)) by TARSKI:def 1;

      the Target of G9 = (T +* (E .--> v2)) by Def7;

      

      hence (the Target of G9 . E) = ((E .--> v2) . E) by A6, FUNCT_4: 13

      .= v2 by FUNCOP_1: 72;

    end;

    theorem :: GRAPH_3:35

    

     Th35: e in the carrier' of G implies (the Source of ( AddNewEdge (v1,v2)) . e) = (the Source of G . e) & (the Target of ( AddNewEdge (v1,v2)) . e) = (the Target of G . e)

    proof

      set S = the Source of G;

      set T = the Target of G;

      set E = the carrier' of G;

      set G9 = ( AddNewEdge (v1,v2));

      set S9 = the Source of G9;

      set T9 = the Target of G9;

      assume

       A1: e in the carrier' of G;

      

       A2: not e in ( dom (E .--> v1))

      proof

        assume e in ( dom (E .--> v1));

        then e in {E};

        then e = E by TARSKI:def 1;

        hence contradiction by A1;

      end;

      

      thus (S9 . e) = ((S +* (E .--> v1)) . e) by Def7

      .= (S . e) by A2, FUNCT_4: 11;

      

       A3: not e in ( dom (E .--> v2))

      proof

        assume e in ( dom (E .--> v2));

        then e in {E};

        then e = E by TARSKI:def 1;

        hence contradiction by A1;

      end;

      

      thus (T9 . e) = ((T +* (E .--> v2)) . e) by Def7

      .= (T . e) by A3, FUNCT_4: 11;

    end;

    theorem :: GRAPH_3:36

    

     Th36: vs9 = vs & vs is_vertex_seq_of c implies vs9 is_vertex_seq_of c

    proof

      assume that

       A1: vs9 = vs and

       A2: vs is_vertex_seq_of c;

      thus ( len vs9) = (( len c) + 1) by A1, A2;

      let n be Nat;

      set T = the Target of G;

      set S = the Source of G;

      set v = (c . n);

      set x = (vs /. n);

      set y = (vs /. (n + 1));

      assume

       A3: 1 <= n & n <= ( len c);

      then (c . n) joins ((vs /. n),(vs /. (n + 1))) by A2;

      then

       A4: (S . v) = x & (T . v) = y or (S . v) = y & (T . v) = x;

      set G9 = ( AddNewEdge (v1,v2));

      set S9 = the Source of G9;

      set T9 = the Target of G9;

      

       A5: the carrier of G = the carrier of G9 by Def7;

      c is FinSequence of the carrier' of G by MSSCYC_1:def 1;

      then

       A6: ( rng c) c= the carrier' of G by FINSEQ_1:def 4;

      n in ( dom c) by A3, FINSEQ_3: 25;

      then (c . n) in ( rng c) by FUNCT_1:def 3;

      then (S9 . v) = (S . v) & (T . v) = (T9 . v) by A6, Th35;

      hence thesis by A1, A5, A4;

    end;

    theorem :: GRAPH_3:37

    

     Th37: c is Chain of ( AddNewEdge (v1,v2))

    proof

      set G9 = ( AddNewEdge (v1,v2));

      consider p be FinSequence of the carrier of G such that

       A1: p is_vertex_seq_of c by GRAPH_2: 33;

      c is FinSequence of the carrier' of G by MSSCYC_1:def 1;

      then

       A2: ( rng c) c= the carrier' of G by FINSEQ_1:def 4;

      the carrier' of G9 = (the carrier' of G \/ {the carrier' of G}) by Def7;

      then the carrier' of G c= the carrier' of G9 by XBOOLE_1: 7;

      then ( rng c) c= the carrier' of G9 by A2;

      hence c is FinSequence of the carrier' of G9 by FINSEQ_1:def 4;

      reconsider p9 = p as FinSequence of the carrier of G9 by Def7;

      take p9;

      thus thesis by A1, Th36;

    end;

    theorem :: GRAPH_3:38

    p is Path of ( AddNewEdge (v1,v2)) by Th37;

    theorem :: GRAPH_3:39

    

     Th39: v9 = v1 & v1 <> v2 implies ( Edges_In (v9,X)) = ( Edges_In (v1,X))

    proof

      assume that

       A1: v9 = v1 and

       A2: v1 <> v2;

      set G9 = ( AddNewEdge (v1,v2));

      set E = the carrier' of G;

      set T = the Target of G;

      set E9 = the carrier' of G9;

      set T9 = the Target of G9;

      

       A3: E9 = (E \/ {E}) by Def7;

      now

        let x be object;

        hereby

          assume

           A4: x in ( Edges_In (v9,X));

          then

           A5: x in X by Def1;

          

           A6: (T9 . x) = v9 by A4, Def1;

          (T9 . E) = v2 by Th34;

          then not x in {E} by A1, A2, A6, TARSKI:def 1;

          then

           A7: x in E by A3, A4, XBOOLE_0:def 3;

          then (T . x) = v1 by A1, A6, Th35;

          hence x in ( Edges_In (v1,X)) by A5, A7, Def1;

        end;

        assume

         A8: x in ( Edges_In (v1,X));

        then (T . x) = v1 by Def1;

        then

         A9: (T9 . x) = v9 by A1, A8, Th35;

        x in X & x in E9 by A3, A8, Def1, XBOOLE_0:def 3;

        hence x in ( Edges_In (v9,X)) by A9, Def1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GRAPH_3:40

    

     Th40: v9 = v2 & v1 <> v2 implies ( Edges_Out (v9,X)) = ( Edges_Out (v2,X))

    proof

      assume that

       A1: v9 = v2 and

       A2: v1 <> v2;

      set G9 = ( AddNewEdge (v1,v2));

      set E = the carrier' of G;

      set S = the Source of G;

      set E9 = the carrier' of G9;

      set S9 = the Source of G9;

      

       A3: E9 = (E \/ {E}) by Def7;

      now

        let x be object;

        hereby

          assume

           A4: x in ( Edges_Out (v9,X));

          then

           A5: x in X by Def2;

          

           A6: (S9 . x) = v9 by A4, Def2;

          (S9 . E) = v1 by Th34;

          then not x in {E} by A1, A2, A6, TARSKI:def 1;

          then

           A7: x in E by A3, A4, XBOOLE_0:def 3;

          then (S . x) = v2 by A1, A6, Th35;

          hence x in ( Edges_Out (v2,X)) by A5, A7, Def2;

        end;

        assume

         A8: x in ( Edges_Out (v2,X));

        then (S . x) = v2 by Def2;

        then

         A9: (S9 . x) = v9 by A1, A8, Th35;

        x in X & x in E9 by A3, A8, Def2, XBOOLE_0:def 3;

        hence x in ( Edges_Out (v9,X)) by A9, Def2;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GRAPH_3:41

    

     Th41: v9 = v1 & the carrier' of G in X implies ( Edges_Out (v9,X)) = (( Edges_Out (v1,X)) \/ {the carrier' of G}) & ( Edges_Out (v1,X)) misses {the carrier' of G}

    proof

      assume that

       A1: v9 = v1 and

       A2: the carrier' of G in X;

      set G9 = ( AddNewEdge (v1,v2));

      set E = the carrier' of G;

      set S = the Source of G;

      set E9 = the carrier' of G9;

      set S9 = the Source of G9;

      

       A3: E9 = (E \/ {E}) by Def7;

      now

        let x be object;

        hereby

          assume

           A4: x in ( Edges_Out (v9,X));

          then

           A5: x in X by Def2;

          

           A6: (S9 . x) = v9 by A4, Def2;

          per cases by A3, A4, XBOOLE_0:def 3;

            suppose

             A7: x in E;

            then (S . x) = v1 by A1, A6, Th35;

            then x in ( Edges_Out (v1,X)) by A5, A7, Def2;

            hence x in (( Edges_Out (v1,X)) \/ {E}) by XBOOLE_0:def 3;

          end;

            suppose x in {E};

            hence x in (( Edges_Out (v1,X)) \/ {E}) by XBOOLE_0:def 3;

          end;

        end;

        assume

         A8: x in (( Edges_Out (v1,X)) \/ {E});

        per cases by A8, XBOOLE_0:def 3;

          suppose

           A9: x in ( Edges_Out (v1,X));

          then (S . x) = v1 by Def2;

          then

           A10: (S9 . x) = v9 by A1, A9, Th35;

          x in X & x in E9 by A3, A9, Def2, XBOOLE_0:def 3;

          hence x in ( Edges_Out (v9,X)) by A10, Def2;

        end;

          suppose

           A11: x in {E};

          

           A12: (S9 . E) = v1 by Th34;

          x = E & x in E9 by A3, A11, TARSKI:def 1, XBOOLE_0:def 3;

          hence x in ( Edges_Out (v9,X)) by A1, A2, A12, Def2;

        end;

      end;

      hence ( Edges_Out (v9,X)) = (( Edges_Out (v1,X)) \/ {E}) by TARSKI: 2;

      assume (( Edges_Out (v1,X)) /\ {E}) <> {} ;

      then

      consider x be object such that

       A13: x in (( Edges_Out (v1,X)) /\ {E}) by XBOOLE_0:def 1;

      x in {E} by A13, XBOOLE_0:def 4;

      then

       A14: x = E by TARSKI:def 1;

      reconsider xx = x as set by TARSKI: 1;

      

       A: not xx in xx;

      x in E by A13;

      hence contradiction by A14, A;

    end;

    theorem :: GRAPH_3:42

    

     Th42: v9 = v2 & the carrier' of G in X implies ( Edges_In (v9,X)) = (( Edges_In (v2,X)) \/ {the carrier' of G}) & ( Edges_In (v2,X)) misses {the carrier' of G}

    proof

      assume that

       A1: v9 = v2 and

       A2: the carrier' of G in X;

      set G9 = ( AddNewEdge (v1,v2));

      set E = the carrier' of G;

      set T = the Target of G;

      set E9 = the carrier' of G9;

      set T9 = the Target of G9;

      

       A3: E9 = (E \/ {E}) by Def7;

      now

        let x be object;

        hereby

          assume

           A4: x in ( Edges_In (v9,X));

          then

           A5: x in X by Def1;

          

           A6: (T9 . x) = v9 by A4, Def1;

          per cases by A3, A4, XBOOLE_0:def 3;

            suppose

             A7: x in E;

            then (T . x) = v2 by A1, A6, Th35;

            then x in ( Edges_In (v2,X)) by A5, A7, Def1;

            hence x in (( Edges_In (v2,X)) \/ {E}) by XBOOLE_0:def 3;

          end;

            suppose x in {E};

            hence x in (( Edges_In (v2,X)) \/ {E}) by XBOOLE_0:def 3;

          end;

        end;

        assume

         A8: x in (( Edges_In (v2,X)) \/ {E});

        per cases by A8, XBOOLE_0:def 3;

          suppose

           A9: x in ( Edges_In (v2,X));

          then (T . x) = v2 by Def1;

          then

           A10: (T9 . x) = v9 by A1, A9, Th35;

          x in X & x in E9 by A3, A9, Def1, XBOOLE_0:def 3;

          hence x in ( Edges_In (v9,X)) by A10, Def1;

        end;

          suppose

           A11: x in {E};

          

           A12: (T9 . E) = v2 by Th34;

          x = E & x in E9 by A3, A11, TARSKI:def 1, XBOOLE_0:def 3;

          hence x in ( Edges_In (v9,X)) by A1, A2, A12, Def1;

        end;

      end;

      hence ( Edges_In (v9,X)) = (( Edges_In (v2,X)) \/ {E}) by TARSKI: 2;

      assume (( Edges_In (v2,X)) /\ {E}) <> {} ;

      then

      consider x be object such that

       A13: x in (( Edges_In (v2,X)) /\ {E}) by XBOOLE_0:def 1;

      x in {E} by A13, XBOOLE_0:def 4;

      then

       A14: x = E by TARSKI:def 1;

      

       A: x in E by A13;

      reconsider xx = x as set by TARSKI: 1;

       not xx in xx;

      hence contradiction by A14, A;

    end;

    theorem :: GRAPH_3:43

    

     Th43: v9 = v & v <> v2 implies ( Edges_In (v9,X)) = ( Edges_In (v,X))

    proof

      assume that

       A1: v9 = v and

       A2: v <> v2;

      set G9 = ( AddNewEdge (v1,v2));

      set E = the carrier' of G;

      set T = the Target of G;

      set E9 = the carrier' of G9;

      set T9 = the Target of G9;

      

       A3: E9 = (E \/ {E}) by Def7;

      now

        let x be object;

        hereby

          assume

           A4: x in ( Edges_In (v9,X));

          then

           A5: x in X by Def1;

          

           A6: (T9 . x) = v9 by A4, Def1;

          (T9 . E) = v2 by Th34;

          then not x in {E} by A1, A2, A6, TARSKI:def 1;

          then

           A7: x in E by A3, A4, XBOOLE_0:def 3;

          then (T . x) = v by A1, A6, Th35;

          hence x in ( Edges_In (v,X)) by A5, A7, Def1;

        end;

        assume

         A8: x in ( Edges_In (v,X));

        then (T . x) = v by Def1;

        then

         A9: (T9 . x) = v9 by A1, A8, Th35;

        x in X & x in E9 by A3, A8, Def1, XBOOLE_0:def 3;

        hence x in ( Edges_In (v9,X)) by A9, Def1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GRAPH_3:44

    

     Th44: v9 = v & v <> v1 implies ( Edges_Out (v9,X)) = ( Edges_Out (v,X))

    proof

      assume that

       A1: v9 = v and

       A2: v <> v1;

      set G9 = ( AddNewEdge (v1,v2));

      set E = the carrier' of G;

      set S = the Source of G;

      set E9 = the carrier' of G9;

      set S9 = the Source of G9;

      

       A3: E9 = (E \/ {E}) by Def7;

      now

        let x be object;

        hereby

          assume

           A4: x in ( Edges_Out (v9,X));

          then

           A5: x in X by Def2;

          

           A6: (S9 . x) = v9 by A4, Def2;

          (S9 . E) = v1 by Th34;

          then not x in {E} by A1, A2, A6, TARSKI:def 1;

          then

           A7: x in E by A3, A4, XBOOLE_0:def 3;

          then (S . x) = v by A1, A6, Th35;

          hence x in ( Edges_Out (v,X)) by A5, A7, Def2;

        end;

        assume

         A8: x in ( Edges_Out (v,X));

        then (S . x) = v by Def2;

        then

         A9: (S9 . x) = v9 by A1, A8, Th35;

        x in X & x in E9 by A3, A8, Def2, XBOOLE_0:def 3;

        hence x in ( Edges_Out (v9,X)) by A9, Def2;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GRAPH_3:45

    

     Th45: not the carrier' of G in ( rng p9) implies p9 is Path of G

    proof

      set G9 = ( AddNewEdge (v1,v2));

      set S = the Source of G;

      set T = the Target of G;

      set E = the carrier' of G;

      set S9 = the Source of G9;

      set T9 = the Target of G9;

      the carrier' of G9 = (E \/ {E}) by Def7;

      then

       A1: ( rng p9) c= (E \/ {E}) by FINSEQ_1:def 4;

      assume

       A2: not the carrier' of G in ( rng p9);

      

       A3: ( rng p9) c= E

      proof

        let x be object;

        assume

         A4: x in ( rng p9);

        then x in E or x in {E} by A1, XBOOLE_0:def 3;

        hence thesis by A2, A4, TARSKI:def 1;

      end;

      p9 is Chain of G

      proof

        thus p9 is FinSequence of the carrier' of G by A3, FINSEQ_1:def 4;

        consider vs9 be FinSequence of the carrier of G9 such that

         A5: vs9 is_vertex_seq_of p9 by MSSCYC_1:def 1;

        reconsider vs = vs9 as FinSequence of the carrier of G by Def7;

        take vs;

        thus vs is_vertex_seq_of p9

        proof

          thus

           A6: ( len vs) = (( len p9) + 1) by A5;

          let n be Nat;

          assume that

           A7: 1 <= n and

           A8: n <= ( len p9);

          set e = (p9 . n);

          reconsider vn9 = (vs9 /. n), vn19 = (vs9 /. (n + 1)) as Vertex of G9;

          (p9 . n) joins ((vs9 /. n),(vs9 /. (n + 1))) by A5, A7, A8;

          then

           A9: (S9 . e) = vn9 & (T9 . e) = vn19 or (S9 . e) = vn19 & (T9 . e) = vn9;

          reconsider vn = (vs /. n), vn1 = (vs /. (n + 1)) as Vertex of G;

          1 <= (n + 1) & (n + 1) <= ( len vs) by A6, A8, NAT_1: 11, XREAL_1: 6;

          then

           A10: (n + 1) in ( dom vs) by FINSEQ_3: 25;

          

          then

           A11: vn1 = (vs . (n + 1)) by PARTFUN1:def 6

          .= vn19 by A10, PARTFUN1:def 6;

          n in ( dom p9) by A7, A8, FINSEQ_3: 25;

          then e in ( rng p9) by FUNCT_1:def 3;

          then

           A12: (S9 . e) = (S . e) & (T9 . e) = (T . e) by A3, Th35;

          ( len p9) <= ( len vs) by A6, NAT_1: 11;

          then n <= ( len vs) by A8, XXREAL_0: 2;

          then

           A13: n in ( dom vs) by A7, FINSEQ_3: 25;

          

          then vn = (vs . n) by PARTFUN1:def 6

          .= vn9 by A13, PARTFUN1:def 6;

          hence thesis by A9, A12, A11;

        end;

      end;

      then

      reconsider p99 = p9 as Chain of G;

      p99 is one-to-one;

      hence thesis;

    end;

    theorem :: GRAPH_3:46

    

     Th46: not the carrier' of G in ( rng p9) & vs = vs9 & vs9 is_vertex_seq_of p9 implies vs is_vertex_seq_of p9

    proof

      set G9 = ( AddNewEdge (v1,v2));

      set S = the Source of G;

      set T = the Target of G;

      set E = the carrier' of G;

      set S9 = the Source of G9;

      set T9 = the Target of G9;

      the carrier' of G9 = (E \/ {E}) by Def7;

      then

       A1: ( rng p9) c= (E \/ {E}) by FINSEQ_1:def 4;

      assume

       A2: not the carrier' of G in ( rng p9);

      

       A3: ( rng p9) c= E

      proof

        let x be object;

        assume

         A4: x in ( rng p9);

        then x in E or x in {E} by A1, XBOOLE_0:def 3;

        hence thesis by A2, A4, TARSKI:def 1;

      end;

      assume that

       A5: vs = vs9 and

       A6: vs9 is_vertex_seq_of p9;

      thus vs is_vertex_seq_of p9

      proof

        thus

         A7: ( len vs) = (( len p9) + 1) by A5, A6;

        let n be Nat;

        assume that

         A8: 1 <= n and

         A9: n <= ( len p9);

        set e = (p9 . n);

        reconsider vn9 = (vs9 /. n), vn19 = (vs9 /. (n + 1)) as Vertex of G9;

        (p9 . n) joins ((vs9 /. n),(vs9 /. (n + 1))) by A6, A8, A9;

        then

         A10: (S9 . e) = vn9 & (T9 . e) = vn19 or (S9 . e) = vn19 & (T9 . e) = vn9;

        reconsider vn = (vs /. n), vn1 = (vs /. (n + 1)) as Vertex of G;

        1 <= (n + 1) & (n + 1) <= ( len vs) by A7, A9, NAT_1: 11, XREAL_1: 6;

        then

         A11: (n + 1) in ( dom vs) by FINSEQ_3: 25;

        

        then

         A12: vn1 = (vs . (n + 1)) by PARTFUN1:def 6

        .= vn19 by A5, A11, PARTFUN1:def 6;

        n in ( dom p9) by A8, A9, FINSEQ_3: 25;

        then e in ( rng p9) by FUNCT_1:def 3;

        then

         A13: (S9 . e) = (S . e) & (T9 . e) = (T . e) by A3, Th35;

        ( len p9) <= ( len vs) by A7, NAT_1: 11;

        then n <= ( len vs) by A9, XXREAL_0: 2;

        then

         A14: n in ( dom vs) by A8, FINSEQ_3: 25;

        

        then vn = (vs . n) by PARTFUN1:def 6

        .= vn9 by A5, A14, PARTFUN1:def 6;

        hence thesis by A10, A13, A12;

      end;

    end;

    registration

      let G be connected Graph, v1,v2 be Vertex of G;

      cluster ( AddNewEdge (v1,v2)) -> connected;

      coherence

      proof

        set G9 = ( AddNewEdge (v1,v2));

        now

          let v19,v29 be Vertex of G9;

          reconsider v1 = v19, v2 = v29 as Vertex of G by Def7;

          assume v19 <> v29;

          then

          consider c be Chain of G, vs be FinSequence of the carrier of G such that

           A1: c is non empty and

           A2: vs is_vertex_seq_of c and

           A3: (vs . 1) = v1 & (vs . ( len vs)) = v2 by Th18;

          reconsider vs9 = vs as FinSequence of the carrier of G9 by Def7;

          reconsider c9 = c as Chain of G9 by Th37;

          take c9;

          take vs9;

          thus c9 is non empty by A1;

          thus vs9 is_vertex_seq_of c9 by A2, Th36;

          thus (vs9 . 1) = v19 & (vs9 . ( len vs9)) = v29 by A3;

        end;

        hence thesis by Th18;

      end;

    end

    reserve G for finite Graph,

v,v1,v2 for Vertex of G,

vs for FinSequence of the carrier of G,

v9 for Vertex of ( AddNewEdge (v1,v2));

    theorem :: GRAPH_3:47

    

     Th47: v9 = v & v1 <> v2 & (v = v1 or v = v2) & the carrier' of G in X implies ( Degree (v9,X)) = (( Degree (v,X)) + 1)

    proof

      assume that

       A1: v9 = v and

       A2: v1 <> v2 and

       A3: v = v1 or v = v2 and

       A4: the carrier' of G in X;

      set E = the carrier' of G;

      per cases by A3;

        suppose

         A5: v = v1;

        then ( Edges_In (v9,X)) = ( Edges_In (v,X)) & ( Edges_Out (v9,X)) = (( Edges_Out (v,X)) \/ {E}) by A1, A2, A4, Th39, Th41;

        

        hence ( Degree (v9,X)) = (( card ( Edges_In (v,X))) + (( card ( Edges_Out (v,X))) + ( card {E}))) by A1, A4, A5, Th41, CARD_2: 40

        .= ((( card ( Edges_In (v,X))) + ( card ( Edges_Out (v,X)))) + ( card {E}))

        .= (( Degree (v,X)) + 1) by CARD_1: 30;

      end;

        suppose

         A6: v = v2;

        then ( Edges_Out (v9,X)) = ( Edges_Out (v,X)) & ( Edges_In (v9,X)) = (( Edges_In (v,X)) \/ {E}) by A1, A2, A4, Th40, Th42;

        

        hence ( Degree (v9,X)) = ((( card ( Edges_In (v,X))) + ( card {E})) + ( card ( Edges_Out (v,X)))) by A1, A4, A6, Th42, CARD_2: 40

        .= ((( card ( Edges_In (v,X))) + ( card ( Edges_Out (v,X)))) + ( card {E}))

        .= (( Degree (v,X)) + 1) by CARD_1: 30;

      end;

    end;

    theorem :: GRAPH_3:48

    

     Th48: v9 = v & v <> v1 & v <> v2 implies ( Degree (v9,X)) = ( Degree (v,X))

    proof

      assume that

       A1: v9 = v and

       A2: v <> v1 and

       A3: v <> v2;

      

      thus ( Degree (v9,X)) = (( card ( Edges_In (v,X))) + ( card ( Edges_Out (v9,X)))) by A1, A3, Th43

      .= ( Degree (v,X)) by A1, A2, Th44;

    end;

    begin

    

     Lm4: for G be finite Graph, c be cyclic Path of G, vs be FinSequence of the carrier of G, v be Vertex of G st vs is_vertex_seq_of c & v in ( rng vs) holds ( Degree (v,( rng c))) is even

    proof

      let G be finite Graph, c be cyclic Path of G, vs be FinSequence of the carrier of G, v be Vertex of G;

      assume that

       A1: vs is_vertex_seq_of c and

       A2: v in ( rng vs);

      set S = the Source of G;

      set T = the Target of G;

      per cases ;

        suppose c is empty;

        then

        reconsider rc = ( rng c) as empty set;

        ( Degree (v,rc)) = (2 * 0 );

        hence thesis;

      end;

        suppose

         A3: c is non empty;

        set ev = { n where n be Element of NAT : 1 <= n & n <= ( len c) & (vs . n) = v };

        

         A4: ev c= ( Seg ( len c))

        proof

          let x be object;

          assume x in ev;

          then ex n be Element of NAT st x = n & 1 <= n & n <= ( len c) & (vs . n) = v;

          hence thesis by FINSEQ_1: 1;

        end;

        reconsider rc = ( rng c) as non empty set by A3;

        

         A5: ( len vs) = (( len c) + 1) by A1;

        set evout = [: {1}, ( Edges_Out (v,rc)):];

        set evin = [: { 0 }, ( Edges_In (v,rc)):];

        

         A6: ( card evout) = (( card {1}) * ( card ( Edges_Out (v,rc)))) by CARD_2: 46

        .= (1 * ( card ( Edges_Out (v,rc)))) by CARD_1: 30

        .= ( card ( Edges_Out (v,rc)));

        

         A7: ( card evin) = (( card { 0 }) * ( card ( Edges_In (v,rc)))) by CARD_2: 46

        .= (1 * ( card ( Edges_In (v,rc)))) by CARD_1: 30

        .= ( card ( Edges_In (v,rc)));

        now

          assume

           A8: (evin \/ evout) is empty;

          then evin is empty;

          then ( Degree (v,rc)) = ( 0 + 0 ) by A7, A6, A8;

          hence contradiction by A1, A2, A3, Th32;

        end;

        then

        reconsider evio = (evin \/ evout) as non empty set;

        

         A9: evin misses evout

        proof

          assume not thesis;

          then

          consider x be object such that

           A10: x in (evin /\ evout) by XBOOLE_0: 4;

          x in evout by A10, XBOOLE_0:def 4;

          then

          consider x21,x22 be object such that

           A11: x21 in {1} and x22 in ( Edges_Out (v,rc)) and

           A12: x = [x21, x22] by ZFMISC_1:def 2;

          

           A13: x21 = 1 by A11, TARSKI:def 1;

          x in evin by A10, XBOOLE_0:def 4;

          then

          consider x11,x12 be object such that

           A14: x11 in { 0 } and x12 in ( Edges_In (v,rc)) and

           A15: x = [x11, x12] by ZFMISC_1:def 2;

          x11 = 0 by A14, TARSKI:def 1;

          hence contradiction by A15, A12, A13, XTUPLE_0: 1;

        end;

        reconsider ev as Subset of ( Seg ( len c)) by A4;

        

         A16: rc c= the carrier' of G by FINSEQ_1:def 4;

        then

        reconsider G9 = G as non void finite Graph;

        reconsider vs9 = vs as FinSequence of the carrier of G9;

        

         A17: (vs9 . 1) = (vs . ( len vs)) by A1, MSSCYC_1: 6;

        now

          

           A18: ( 0 + 1) <= ( len c) by A3, NAT_1: 13;

          consider n be object such that

           A19: n in ( dom vs) and

           A20: (vs . n) = v by A2, FUNCT_1:def 3;

          reconsider n as Element of NAT by A19;

          

           A21: n <= ( len vs) by A19, FINSEQ_3: 25;

          

           A22: 1 <= n by A19, FINSEQ_3: 25;

          thus ev is non empty

          proof

            per cases by A21, XXREAL_0: 1;

              suppose n = ( len vs);

              then 1 in ev by A17, A20, A18;

              hence thesis;

            end;

              suppose n < ( len vs);

              then n <= ( len c) by A5, NAT_1: 13;

              then n in ev by A20, A22;

              hence thesis;

            end;

          end;

        end;

        then

        reconsider ev as finite non empty set;

        set ev92 = [:2, ev:];

        now

          defpred R[ Element of ev92, Element of evio, Element of NAT ] means $1 = [1, $3] & (((vs . $3) = (S . (c . $3)) & $2 = [1, (c . $3)]) or ((vs . $3) = (T . (c . $3)) & $2 = [ 0 , (c . $3)] & (T . (c . $3)) <> (S . (c . $3))));

          defpred L[ Element of ev92, Element of evio, Element of NAT ] means $1 = [ 0 , $3] & ((ex k be Element of NAT st 1 <= k & $3 = (k + 1) & ((vs . $3) = (T . (c . k)) & $2 = [ 0 , (c . k)] or (vs . $3) = (S . (c . k)) & $2 = [1, (c . k)] & (T . (c . k)) <> (S . (c . k)))) or $3 = 1 & ((vs . 1) = (T . (c . ( len c))) & $2 = [ 0 , (c . ( len c))] or (vs . 1) = (S . (c . ( len c))) & $2 = [1, (c . ( len c))] & (T . (c . ( len c))) <> (S . (c . ( len c)))));

          take Z = { [x, y] where x be Element of ev92, y be Element of evio : ex n be Element of NAT st 1 <= n & n <= ( len c) & ( L[x, y, n] or R[x, y, n]) };

          thus for x be object st x in ev92 holds ex y be object st y in (evin \/ evout) & [x, y] in Z

          proof

            

             A23: 1 in {1} by TARSKI:def 1;

            let x be object;

            

             A24: 0 in { 0 } by TARSKI:def 1;

            assume

             A25: x in ev92;

            then

            consider u,w be object such that

             A26: [u, w] = x by RELAT_1:def 1;

            reconsider x9 = x as Element of ev92 by A25;

            

             A27: u in 2 by A25, A26, ZFMISC_1: 87;

            w in ev by A25, A26, ZFMISC_1: 87;

            then

            consider n be Element of NAT such that

             A28: w = n and

             A29: 1 <= n and

             A30: n <= ( len c) and

             A31: (vs . n) = v;

            per cases by A27, CARD_1: 50, TARSKI:def 2;

              suppose

               A32: u = 0 ;

              thus ex y be object st y in (evin \/ evout) & [x, y] in Z

              proof

                per cases by A29, XXREAL_0: 1;

                  suppose 1 < n;

                  then

                  consider k be Element of NAT such that

                   A33: n = (1 + k) and

                   A34: 1 <= k by FINSEQ_4: 84;

                  k <= n by A33, NAT_1: 11;

                  then

                   A35: k <= ( len c) by A30, XXREAL_0: 2;

                  then k in ( dom c) by A34, FINSEQ_3: 25;

                  then

                  reconsider e = (c . k) as Element of rc by FUNCT_1:def 3;

                  

                   A36: e in rc;

                  thus thesis

                  proof

                    per cases by A1, A34, A35, Lm3;

                      suppose

                       A37: (T . (c . k)) = (vs . (k + 1));

                      take y = [ 0 , (c . k)];

                      e in ( Edges_In (v,rc)) by A16, A31, A33, A36, A37, Def1;

                      then

                       A38: y in evin by A24, ZFMISC_1: 87;

                      hence y in (evin \/ evout) by XBOOLE_0:def 3;

                      reconsider y9 = y as Element of evio by A38, XBOOLE_0:def 3;

                       L[x9, y9, n] by A26, A28, A32, A33, A34, A37;

                      hence thesis by A29, A30;

                    end;

                      suppose

                       A39: (S . (c . k)) = (vs . (k + 1)) & (T . (c . k)) <> (S . (c . k));

                      take y = [1, (c . k)];

                      e in ( Edges_Out (v,rc)) by A16, A31, A33, A36, A39, Def2;

                      then

                       A40: y in evout by A23, ZFMISC_1: 87;

                      hence y in (evin \/ evout) by XBOOLE_0:def 3;

                      reconsider y9 = y as Element of evio by A40, XBOOLE_0:def 3;

                       L[x9, y9, n] by A26, A28, A32, A33, A34, A39;

                      hence thesis by A29, A30;

                    end;

                  end;

                end;

                  suppose

                   A41: n = 1;

                  

                   A42: 1 <= ( len c) by A29, A30, XXREAL_0: 2;

                  then ( len c) in ( dom c) by FINSEQ_3: 25;

                  then

                  reconsider e = (c . ( len c)) as Element of rc by FUNCT_1:def 3;

                  

                   A43: 1 <= ( len c) by A29, A30, XXREAL_0: 2;

                  

                   A44: e in rc & (vs . 1) = (vs . (( len c) + 1)) by A1, MSSCYC_1: 6;

                  thus thesis

                  proof

                    per cases by A1, A42, Lm3;

                      suppose

                       A45: (T . (c . ( len c))) = (vs . (( len c) + 1));

                      take y = [ 0 , (c . ( len c))];

                      e in ( Edges_In (v,rc)) by A16, A31, A41, A44, A45, Def1;

                      then

                       A46: y in evin by A24, ZFMISC_1: 87;

                      hence y in (evin \/ evout) by XBOOLE_0:def 3;

                      reconsider y9 = y as Element of evio by A46, XBOOLE_0:def 3;

                       L[x9, y9, 1] by A1, A26, A28, A32, A41, A45, MSSCYC_1: 6;

                      hence thesis by A43;

                    end;

                      suppose

                       A47: (S . (c . ( len c))) = (vs . (( len c) + 1)) & (T . (c . ( len c))) <> (S . (c . ( len c)));

                      take y = [1, (c . ( len c))];

                      e in ( Edges_Out (v,rc)) by A16, A31, A41, A44, A47, Def2;

                      then

                       A48: y in evout by A23, ZFMISC_1: 87;

                      hence y in (evin \/ evout) by XBOOLE_0:def 3;

                      reconsider y9 = y as Element of evio by A48, XBOOLE_0:def 3;

                       L[x9, y9, 1] by A1, A26, A28, A32, A41, A47, MSSCYC_1: 6;

                      hence thesis by A43;

                    end;

                  end;

                end;

              end;

            end;

              suppose

               A49: u = 1;

              n in ( dom c) by A29, A30, FINSEQ_3: 25;

              then

              reconsider e = (c . n) as Element of rc by FUNCT_1:def 3;

              

               A50: e in rc;

              thus ex y be object st y in (evin \/ evout) & [x, y] in Z

              proof

                per cases by A1, A29, A30, Lm3;

                  suppose

                   A51: (vs . n) = (S . (c . n));

                  take y = [1, (c . n)];

                  e in ( Edges_Out (v,rc)) by A16, A31, A50, A51, Def2;

                  then

                   A52: y in evout by A23, ZFMISC_1: 87;

                  hence y in (evin \/ evout) by XBOOLE_0:def 3;

                  reconsider y9 = y as Element of evio by A52, XBOOLE_0:def 3;

                   R[x9, y9, n] by A26, A28, A49, A51;

                  hence thesis by A29, A30;

                end;

                  suppose

                   A53: (vs . n) = (T . (c . n)) & (T . (c . n)) <> (S . (c . n));

                  take y = [ 0 , (c . n)];

                  e in ( Edges_In (v,rc)) by A16, A31, A50, A53, Def1;

                  then

                   A54: y in evin by A24, ZFMISC_1: 87;

                  hence y in (evin \/ evout) by XBOOLE_0:def 3;

                  reconsider y9 = y as Element of evio by A54, XBOOLE_0:def 3;

                   R[x9, y9, n] by A26, A28, A49, A53;

                  hence thesis by A29, A30;

                end;

              end;

            end;

          end;

          thus for y be object st y in (evin \/ evout) holds ex x be object st x in ev92 & [x, y] in Z

          proof

            let y be object;

            assume

             A55: y in (evin \/ evout);

            then

            reconsider y9 = y as Element of evio;

            per cases by A55, XBOOLE_0:def 3;

              suppose

               A56: y in evin;

              then

              consider u,e be object such that

               A57: [u, e] = y by RELAT_1:def 1;

              

               A58: e in ( Edges_In (v,rc)) by A56, A57, ZFMISC_1: 87;

              then

               A59: (T . e) = v by Def1;

              e in rc by A58, Def1;

              then

              consider n be object such that

               A60: n in ( dom c) and

               A61: e = (c . n) by FUNCT_1:def 3;

              reconsider n as Element of NAT by A60;

              

               A62: ( dom c) = ( Seg ( len c)) by FINSEQ_1:def 3;

              then

               A63: 1 <= n by A60, FINSEQ_1: 1;

              

               A64: 1 in 2 by CARD_1: 50, TARSKI:def 2;

              

               A65: 0 in 2 by CARD_1: 50, TARSKI:def 2;

              

               A66: n <= ( len c) by A60, A62, FINSEQ_1: 1;

              

               A67: u in { 0 } by A56, A57, ZFMISC_1: 87;

              then

               A68: u = 0 by TARSKI:def 1;

              thus ex x be object st x in ev92 & [x, y] in Z

              proof

                per cases by A1, A63, A66, Lm3;

                  suppose

                   A69: (vs . (n + 1)) = (T . (c . n));

                  thus thesis

                  proof

                    per cases by A66, XXREAL_0: 1;

                      suppose

                       A70: n = ( len c);

                      take x = [ 0 , 1];

                      (vs . 1) = v by A1, A59, A61, A69, A70, MSSCYC_1: 6;

                      then

                       A71: 1 in ev by A63, A70;

                      hence x in ev92 by A65, ZFMISC_1: 87;

                      reconsider x9 = x as Element of ev92 by A65, A71, ZFMISC_1: 87;

                      1 <= ( len c) & L[x9, y9, 1] by A1, A57, A67, A60, A61, A62, A69, A70, FINSEQ_1: 1, MSSCYC_1: 6, TARSKI:def 1;

                      hence thesis;

                    end;

                      suppose

                       A72: n < ( len c);

                      take x = [ 0 , (n + 1)];

                      

                       A73: 1 <= (n + 1) & (n + 1) <= ( len c) by A72, NAT_1: 11, NAT_1: 13;

                      then

                       A74: (n + 1) in ev by A59, A61, A69;

                      hence x in ev92 by A65, ZFMISC_1: 87;

                      reconsider x9 = x as Element of ev92 by A65, A74, ZFMISC_1: 87;

                       L[x9, y9, (n + 1)] by A57, A68, A61, A63, A69;

                      hence thesis by A73;

                    end;

                  end;

                end;

                  suppose

                   A75: (vs . n) = (T . (c . n)) & (T . (c . n)) <> (S . (c . n));

                  take x = [1, n];

                  

                   A76: n in ev by A59, A61, A63, A66, A75;

                  hence x in ev92 by A64, ZFMISC_1: 87;

                  reconsider x9 = x as Element of ev92 by A64, A76, ZFMISC_1: 87;

                   R[x9, y9, n] by A57, A67, A61, A75, TARSKI:def 1;

                  hence thesis by A63, A66;

                end;

              end;

            end;

              suppose

               A77: y in evout;

              then

              consider u,e be object such that

               A78: [u, e] = y by RELAT_1:def 1;

              

               A79: e in ( Edges_Out (v,rc)) by A77, A78, ZFMISC_1: 87;

              then

               A80: (S . e) = v by Def2;

              e in rc by A79, Def2;

              then

              consider n be object such that

               A81: n in ( dom c) and

               A82: e = (c . n) by FUNCT_1:def 3;

              reconsider n as Element of NAT by A81;

              

               A83: ( dom c) = ( Seg ( len c)) by FINSEQ_1:def 3;

              then

               A84: 1 <= n by A81, FINSEQ_1: 1;

              

               A85: 1 in 2 by CARD_1: 50, TARSKI:def 2;

              

               A86: 0 in 2 by CARD_1: 50, TARSKI:def 2;

              

               A87: n <= ( len c) by A81, A83, FINSEQ_1: 1;

              

               A88: u in {1} by A77, A78, ZFMISC_1: 87;

              then

               A89: u = 1 by TARSKI:def 1;

              thus ex x be object st x in ev92 & [x, y] in Z

              proof

                per cases by A1, A84, A87, Lm3;

                  suppose

                   A90: (vs . (n + 1)) = (S . (c . n)) & (T . (c . n)) <> (S . (c . n));

                  thus thesis

                  proof

                    per cases by A87, XXREAL_0: 1;

                      suppose

                       A91: n = ( len c);

                      take x = [ 0 , 1];

                      (vs . 1) = v by A1, A80, A82, A90, A91, MSSCYC_1: 6;

                      then

                       A92: 1 in ev by A84, A91;

                      hence x in ev92 by A86, ZFMISC_1: 87;

                      reconsider x9 = x as Element of ev92 by A86, A92, ZFMISC_1: 87;

                      1 <= ( len c) & L[x9, y9, 1] by A1, A78, A88, A81, A82, A83, A90, A91, FINSEQ_1: 1, MSSCYC_1: 6, TARSKI:def 1;

                      hence thesis;

                    end;

                      suppose

                       A93: n < ( len c);

                      take x = [ 0 , (n + 1)];

                      

                       A94: 1 <= (n + 1) & (n + 1) <= ( len c) by A93, NAT_1: 11, NAT_1: 13;

                      then

                       A95: (n + 1) in ev by A80, A82, A90;

                      hence x in ev92 by A86, ZFMISC_1: 87;

                      reconsider x9 = x as Element of ev92 by A86, A95, ZFMISC_1: 87;

                       L[x9, y9, (n + 1)] by A78, A89, A82, A84, A90;

                      hence thesis by A94;

                    end;

                  end;

                end;

                  suppose

                   A96: (vs . n) = (S . (c . n));

                  take x = [1, n];

                  

                   A97: n in ev by A80, A82, A84, A87, A96;

                  hence x in ev92 by A85, ZFMISC_1: 87;

                  reconsider x9 = x as Element of ev92 by A85, A97, ZFMISC_1: 87;

                   R[x9, y9, n] by A78, A88, A82, A96, TARSKI:def 1;

                  hence thesis by A84, A87;

                end;

              end;

            end;

          end;

          thus for x,y,z,u be object st [x, y] in Z & [z, u] in Z holds x = z iff y = u

          proof

            let x,y,z,u be object;

            assume that

             A98: [x, y] in Z and

             A99: [z, u] in Z;

            consider x9 be Element of ev92, y9 be Element of evio such that

             A100: [x, y] = [x9, y9] and

             A101: ex n be Element of NAT st 1 <= n & n <= ( len c) & ( L[x9, y9, n] or R[x9, y9, n]) by A98;

            consider z9 be Element of ev92, u9 be Element of evio such that

             A102: [z, u] = [z9, u9] and

             A103: ex n be Element of NAT st 1 <= n & n <= ( len c) & ( L[z9, u9, n] or R[z9, u9, n]) by A99;

            

             A104: x = x9 by A100, XTUPLE_0: 1;

            

             A105: y = y9 by A100, XTUPLE_0: 1;

            consider n2 be Element of NAT such that

             A106: 1 <= n2 and

             A107: n2 <= ( len c) and

             A108: L[z9, u9, n2] or R[z9, u9, n2] by A103;

            consider n1 be Element of NAT such that

             A109: 1 <= n1 and

             A110: n1 <= ( len c) and

             A111: L[x9, y9, n1] or R[x9, y9, n1] by A101;

            

             A112: z = z9 by A102, XTUPLE_0: 1;

            thus x = z implies y = u

            proof

              assume

               A113: x = z;

              per cases by A111, A108;

                suppose

                 A114: L[x9, y9, n1] & L[z9, u9, n2];

                then

                 A115: n1 = n2 by A104, A112, A113, XTUPLE_0: 1;

                thus y = u

                proof

                  per cases by A114;

                    suppose (ex k be Element of NAT st 1 <= k & n1 = (k + 1) & ((vs . n1) = (T . (c . k)) & y9 = [ 0 , (c . k)] or (vs . n1) = (S . (c . k)) & y9 = [1, (c . k)] & (T . (c . k)) <> (S . (c . k)))) & ex k be Element of NAT st 1 <= k & n2 = (k + 1) & ((vs . n2) = (T . (c . k)) & u9 = [ 0 , (c . k)] or (vs . n2) = (S . (c . k)) & u9 = [1, (c . k)] & (T . (c . k)) <> (S . (c . k)));

                    hence thesis by A102, A105, A115, XTUPLE_0: 1;

                  end;

                    suppose (ex k be Element of NAT st 1 <= k & n1 = (k + 1) & ((vs . n1) = (T . (c . k)) & y9 = [ 0 , (c . k)] or (vs . n1) = (S . (c . k)) & y9 = [1, (c . k)] & (T . (c . k)) <> (S . (c . k)))) & n2 = 1 & ((vs . 1) = (T . (c . ( len c))) & u9 = [ 0 , (c . ( len c))] or (vs . 1) = (S . (c . ( len c))) & u9 = [1, (c . ( len c))] & (T . (c . ( len c))) <> (S . (c . ( len c))));

                    hence thesis by A115;

                  end;

                    suppose n1 = 1 & ((vs . 1) = (T . (c . ( len c))) & y9 = [ 0 , (c . ( len c))] or (vs . 1) = (S . (c . ( len c))) & y9 = [1, (c . ( len c))] & (T . (c . ( len c))) <> (S . (c . ( len c)))) & ex k be Element of NAT st 1 <= k & n2 = (k + 1) & ((vs . n2) = (T . (c . k)) & u9 = [ 0 , (c . k)] or (vs . n2) = (S . (c . k)) & u9 = [1, (c . k)] & (T . (c . k)) <> (S . (c . k)));

                    hence thesis by A115;

                  end;

                    suppose n1 = 1 & ((vs . 1) = (T . (c . ( len c))) & y9 = [ 0 , (c . ( len c))] or (vs . 1) = (S . (c . ( len c))) & y9 = [1, (c . ( len c))] & (T . (c . ( len c))) <> (S . (c . ( len c)))) & n2 = 1 & ((vs . 1) = (T . (c . ( len c))) & u9 = [ 0 , (c . ( len c))] or (vs . 1) = (S . (c . ( len c))) & u9 = [1, (c . ( len c))] & (T . (c . ( len c))) <> (S . (c . ( len c))));

                    hence thesis by A102, A105, XTUPLE_0: 1;

                  end;

                end;

              end;

                suppose L[x9, y9, n1] & R[z9, u9, n2];

                hence thesis by A104, A112, A113, XTUPLE_0: 1;

              end;

                suppose R[x9, y9, n1] & L[z9, u9, n2];

                hence thesis by A104, A112, A113, XTUPLE_0: 1;

              end;

                suppose

                 A116: R[x9, y9, n1] & R[z9, u9, n2];

                then n1 = n2 by A104, A112, A113, XTUPLE_0: 1;

                hence thesis by A100, A102, A116, XTUPLE_0: 1;

              end;

            end;

            

             A117: u = u9 by A102, XTUPLE_0: 1;

            thus y = u implies x = z

            proof

              assume

               A118: y = u;

              per cases by A111, A108;

                suppose

                 A119: L[x9, y9, n1] & L[z9, u9, n2];

                thus x = z

                proof

                  per cases by A119;

                    suppose

                     A120: (ex k be Element of NAT st 1 <= k & n1 = (k + 1) & ((vs . n1) = (T . (c . k)) & y9 = [ 0 , (c . k)] or (vs . n1) = (S . (c . k)) & y9 = [1, (c . k)] & (T . (c . k)) <> (S . (c . k)))) & ex k be Element of NAT st 1 <= k & n2 = (k + 1) & ((vs . n2) = (T . (c . k)) & u9 = [ 0 , (c . k)] or (vs . n2) = (S . (c . k)) & u9 = [1, (c . k)] & (T . (c . k)) <> (S . (c . k)));

                    then

                    consider k2 be Element of NAT such that

                     A121: 1 <= k2 and

                     A122: n2 = (k2 + 1) and

                     A123: (vs . n2) = (T . (c . k2)) & u9 = [ 0 , (c . k2)] or (vs . n2) = (S . (c . k2)) & u9 = [1, (c . k2)] & (T . (c . k2)) <> (S . (c . k2));

                    k2 <= n2 by A122, NAT_1: 12;

                    then

                     A124: k2 <= ( len c) by A107, XXREAL_0: 2;

                    consider k1 be Element of NAT such that

                     A125: 1 <= k1 and

                     A126: n1 = (k1 + 1) and

                     A127: (vs . n1) = (T . (c . k1)) & y9 = [ 0 , (c . k1)] or (vs . n1) = (S . (c . k1)) & y9 = [1, (c . k1)] & (T . (c . k1)) <> (S . (c . k1)) by A120;

                    k1 <= n1 by A126, NAT_1: 12;

                    then

                     A128: k1 <= ( len c) by A110, XXREAL_0: 2;

                    (c . k1) = (c . k2) by A105, A117, A118, A127, A123, XTUPLE_0: 1;

                    then k1 = k2 by A125, A121, A128, A124, Lm2;

                    hence thesis by A100, A102, A119, A126, A122, XTUPLE_0: 1;

                  end;

                    suppose

                     A129: (ex k be Element of NAT st 1 <= k & n1 = (k + 1) & ((vs . n1) = (T . (c . k)) & y9 = [ 0 , (c . k)] or (vs . n1) = (S . (c . k)) & y9 = [1, (c . k)] & (T . (c . k)) <> (S . (c . k)))) & n2 = 1 & ((vs . 1) = (T . (c . ( len c))) & u9 = [ 0 , (c . ( len c))] or (vs . 1) = (S . (c . ( len c))) & u9 = [1, (c . ( len c))] & (T . (c . ( len c))) <> (S . (c . ( len c))));

                    

                     A130: 1 <= ( len c) by A109, A110, XXREAL_0: 2;

                    consider k1 be Element of NAT such that

                     A131: 1 <= k1 and

                     A132: n1 = (k1 + 1) and (vs . n1) = (T . (c . k1)) & y9 = [ 0 , (c . k1)] or (vs . n1) = (S . (c . k1)) & y9 = [1, (c . k1)] & (T . (c . k1)) <> (S . (c . k1)) by A129;

                    k1 <= n1 by A132, NAT_1: 12;

                    then

                     A133: k1 <= ( len c) by A110, XXREAL_0: 2;

                    (c . k1) = (c . ( len c)) by A105, A117, A118, A129, A132, XTUPLE_0: 1;

                    then (( len c) + 1) <= ( len c) by A110, A131, A132, A133, A130, Lm2;

                    hence thesis by NAT_1: 13;

                  end;

                    suppose

                     A134: n1 = 1 & ((vs . 1) = (T . (c . ( len c))) & y9 = [ 0 , (c . ( len c))] or (vs . 1) = (S . (c . ( len c))) & y9 = [1, (c . ( len c))] & (T . (c . ( len c))) <> (S . (c . ( len c)))) & ex k be Element of NAT st 1 <= k & n2 = (k + 1) & ((vs . n2) = (T . (c . k)) & u9 = [ 0 , (c . k)] or (vs . n2) = (S . (c . k)) & u9 = [1, (c . k)] & (T . (c . k)) <> (S . (c . k)));

                    

                     A135: 1 <= ( len c) by A106, A107, XXREAL_0: 2;

                    consider k2 be Element of NAT such that

                     A136: 1 <= k2 and

                     A137: n2 = (k2 + 1) and (vs . n2) = (T . (c . k2)) & u9 = [ 0 , (c . k2)] or (vs . n2) = (S . (c . k2)) & u9 = [1, (c . k2)] & (T . (c . k2)) <> (S . (c . k2)) by A134;

                    k2 <= n2 by A137, NAT_1: 12;

                    then

                     A138: k2 <= ( len c) by A107, XXREAL_0: 2;

                    (c . k2) = (c . ( len c)) by A105, A117, A118, A134, A137, XTUPLE_0: 1;

                    then (( len c) + 1) <= ( len c) by A107, A136, A137, A138, A135, Lm2;

                    hence thesis by NAT_1: 13;

                  end;

                    suppose n1 = 1 & ((vs . 1) = (T . (c . ( len c))) & y9 = [ 0 , (c . ( len c))] or (vs . 1) = (S . (c . ( len c))) & y9 = [1, (c . ( len c))] & (T . (c . ( len c))) <> (S . (c . ( len c)))) & n2 = 1 & ((vs . 1) = (T . (c . ( len c))) & u9 = [ 0 , (c . ( len c))] or (vs . 1) = (S . (c . ( len c))) & u9 = [1, (c . ( len c))] & (T . (c . ( len c))) <> (S . (c . ( len c))));

                    hence thesis by A100, A102, A119, XTUPLE_0: 1;

                  end;

                end;

              end;

                suppose

                 A139: L[x9, y9, n1] & R[z9, u9, n2];

                thus x = z

                proof

                  per cases by A139;

                    suppose ex k be Element of NAT st 1 <= k & n1 = (k + 1) & ((vs . n1) = (T . (c . k)) & y9 = [ 0 , (c . k)] or (vs . n1) = (S . (c . k)) & y9 = [1, (c . k)] & (T . (c . k)) <> (S . (c . k)));

                    then

                    consider k be Element of NAT such that

                     A140: 1 <= k and

                     A141: n1 = (k + 1) and (vs . n1) = (T . (c . k)) & y9 = [ 0 , (c . k)] or (vs . n1) = (S . (c . k)) & y9 = [1, (c . k)] & (T . (c . k)) <> (S . (c . k));

                    k <= n1 by A141, NAT_1: 12;

                    then

                     A142: k <= ( len c) by A110, XXREAL_0: 2;

                    (c . n2) = (c . k) by A105, A117, A118, A139, A140, A141, XTUPLE_0: 1;

                    then n2 = k by A106, A107, A140, A142, Lm2;

                    hence thesis by A1, A105, A117, A106, A107, A118, A139, A141, Lm3, XTUPLE_0: 1;

                  end;

                    suppose

                     A143: n1 = 1 & ((vs . 1) = (T . (c . ( len c))) & y9 = [ 0 , (c . ( len c))] or (vs . 1) = (S . (c . ( len c))) & y9 = [1, (c . ( len c))] & (T . (c . ( len c))) <> (S . (c . ( len c))));

                    

                     A144: 1 <= ( len c) by A109, A110, XXREAL_0: 2;

                    (c . n2) = (c . ( len c)) by A105, A117, A118, A139, A143, XTUPLE_0: 1;

                    then

                     A145: n2 = ( len c) by A106, A107, A144, Lm2;

                    (vs . n2) = (T . (c . n2)) & (vs . (n2 + 1)) = (S . (c . n2)) or (vs . n2) = (S . (c . n2)) & (vs . (n2 + 1)) = (T . (c . n2)) by A1, A106, A107, Lm3;

                    hence x = z by A1, A105, A117, A118, A139, A143, A145, MSSCYC_1: 6, XTUPLE_0: 1;

                  end;

                end;

              end;

                suppose

                 A146: R[x9, y9, n1] & L[z9, u9, n2];

                thus x = z

                proof

                  per cases by A146;

                    suppose ex k be Element of NAT st 1 <= k & n2 = (k + 1) & ((vs . n2) = (T . (c . k)) & u9 = [ 0 , (c . k)] or (vs . n2) = (S . (c . k)) & u9 = [1, (c . k)] & (T . (c . k)) <> (S . (c . k)));

                    then

                    consider k be Element of NAT such that

                     A147: 1 <= k and

                     A148: n2 = (k + 1) and (vs . n2) = (T . (c . k)) & u9 = [ 0 , (c . k)] or (vs . n2) = (S . (c . k)) & u9 = [1, (c . k)] & (T . (c . k)) <> (S . (c . k));

                    k <= n2 by A148, NAT_1: 12;

                    then

                     A149: k <= ( len c) by A107, XXREAL_0: 2;

                    (c . n1) = (c . k) by A105, A117, A118, A146, A147, A148, XTUPLE_0: 1;

                    then n1 = k by A109, A110, A147, A149, Lm2;

                    hence thesis by A1, A105, A117, A109, A110, A118, A146, A148, Lm3, XTUPLE_0: 1;

                  end;

                    suppose

                     A150: n2 = 1 & ((vs . 1) = (T . (c . ( len c))) & u9 = [ 0 , (c . ( len c))] or (vs . 1) = (S . (c . ( len c))) & u9 = [1, (c . ( len c))] & (T . (c . ( len c))) <> (S . (c . ( len c))));

                    

                     A151: 1 <= ( len c) by A109, A110, XXREAL_0: 2;

                    (c . n1) = (c . ( len c)) by A105, A117, A118, A146, A150, XTUPLE_0: 1;

                    then

                     A152: n1 = ( len c) by A109, A110, A151, Lm2;

                    (vs . n1) = (T . (c . n1)) & (vs . (n1 + 1)) = (S . (c . n1)) or (vs . n1) = (S . (c . n1)) & (vs . (n1 + 1)) = (T . (c . n1)) by A1, A109, A110, Lm3;

                    hence x = z by A1, A105, A117, A118, A146, A150, A152, MSSCYC_1: 6, XTUPLE_0: 1;

                  end;

                end;

              end;

                suppose

                 A153: R[x9, y9, n1] & R[z9, u9, n2];

                then (c . n1) = (c . n2) by A105, A117, A118, XTUPLE_0: 1;

                then n1 = n2 by A109, A110, A106, A107, Lm2;

                hence thesis by A100, A102, A153, XTUPLE_0: 1;

              end;

            end;

          end;

        end;

        then (ev92,(evin \/ evout)) are_equipotent ;

        

        then ( card ev92) = ( card (evin \/ evout)) by CARD_1: 5

        .= (( card evin) + ( card evout)) by A9, CARD_2: 40;

        

        then ( Degree (v,rc)) = (( card 2) * ( card ev)) by A7, A6, CARD_2: 46

        .= (2 * ( card ev));

        hence thesis;

      end;

    end;

    theorem :: GRAPH_3:49

    

     Th49: for c be cyclic Path of G holds ( Degree (v,( rng c))) is even

    proof

      let c be cyclic Path of G;

      per cases ;

        suppose c is empty;

        then

        reconsider rc = ( rng c) as empty set;

        ( Degree (v,rc)) = (2 * 0 );

        hence thesis;

      end;

        suppose

         A1: c is non empty;

        consider vs be FinSequence of the carrier of G such that

         A2: vs is_vertex_seq_of c by GRAPH_2: 33;

        thus ( Degree (v,( rng c))) is even

        proof

          per cases ;

            suppose v in ( rng vs);

            hence thesis by A2, Lm4;

          end;

            suppose not v in ( rng vs);

            then ( Degree (v,( rng c))) = (2 * 0 ) by A1, A2, Th32;

            hence thesis;

          end;

        end;

      end;

    end;

    theorem :: GRAPH_3:50

    

     Th50: for c be Path of G st c is non cyclic & vs is_vertex_seq_of c holds ( Degree (v,( rng c))) is even iff v <> (vs . 1) & v <> (vs . ( len vs))

    proof

      let c be Path of G such that

       A1: c is non cyclic and

       A2: vs is_vertex_seq_of c;

      ( len vs) = (( len c) + 1) by A2;

      then

       A3: 1 <= ( len vs) by NAT_1: 11;

      then 1 in ( dom vs) & ( len vs) in ( dom vs) by FINSEQ_3: 25;

      then

      reconsider v1 = (vs . 1), v2 = (vs . ( len vs)) as Vertex of G by FINSEQ_2: 11;

      

       A4: v1 <> v2 by A1, A2;

      set G9 = ( AddNewEdge (v1,v2));

      reconsider vs9 = vs as FinSequence of the carrier of G9 by Def7;

      reconsider c9 = c as Path of G9 by Th37;

      

       A5: vs9 is_vertex_seq_of c9 by A2, Th36;

      reconsider v9 = v, v19 = v1, v29 = v2 as Vertex of G9 by Def7;

      set v219 = <*v29, v19*>;

      set vs9e = (vs9 ^' <*v29, v19*>);

      ( len v219) = 2 by FINSEQ_1: 44;

      then

       A6: (vs9e . ( len vs9e)) = (v219 . 2) by FINSEQ_6: 142;

      set E = the carrier' of G;

      set e = E;

      

       A7: e in {E} by TARSKI:def 1;

      the carrier' of G9 = (the carrier' of G \/ {E}) by Def7;

      then e in the carrier' of G9 by A7, XBOOLE_0:def 3;

      then

      reconsider ep = <*e*> as Path of G9 by Th4;

      

       A8: ( rng ep) = {e} by FINSEQ_1: 39;

      

       A9: not e in e;

      then ( rng ep) misses E by A8, ZFMISC_1: 50;

      then

       A10: (( rng ep) /\ E) = {} ;

      (the Source of G9 . e) = v19 & (the Target of G9 . e) = v29 by Th34;

      then

       A11: (vs9 . ( len vs9)) = ( <*v29, v19*> . 1) & <*v29, v19*> is_vertex_seq_of ep by Th11, FINSEQ_1: 44;

      

       A12: ( rng c) c= the carrier' of G by FINSEQ_1:def 4;

      then

       A13: not e in ( rng c) by A9;

      ( rng c9) misses ( rng ep)

      proof

        assume not thesis;

        then ex x be object st x in ( rng c9) & x in ( rng ep) by XBOOLE_0: 3;

        hence contradiction by A13, A8, TARSKI:def 1;

      end;

      then

      reconsider c9e = (c9 ^ ep) as Path of G9 by A5, A11, Th6;

      

       A14: vs9e is_vertex_seq_of c9e by A5, A11, GRAPH_2: 44;

      (vs9e . 1) = (vs . 1) by A3, FINSEQ_6: 140;

      then (vs9e . 1) = (vs9e . ( len vs9e)) by A6, FINSEQ_1: 44;

      then

      reconsider c9e as cyclic Path of G9 by A14, MSSCYC_1:def 2;

      ( rng c9e) = (( rng c) \/ ( rng ep)) by FINSEQ_1: 31;

      then

       A15: e in ( rng c9e) by A7, A8, XBOOLE_0:def 3;

      

       A16: (( rng c9e) /\ E) = ((( rng c) \/ ( rng ep)) /\ E) by FINSEQ_1: 31

      .= ((( rng c) /\ E) \/ {} ) by A10, XBOOLE_1: 23

      .= ( rng c) by A12, XBOOLE_1: 28;

      then

       A17: ( Degree (v,( rng c9e))) = ( Degree (v,( rng c))) by Th31;

      reconsider dv9 = ( Degree (v9,( rng c9e))) as even Element of NAT by Th49;

      

       A18: ( Degree (v9,( rng c9e))) is even by Th49;

      per cases ;

        suppose v <> v1 & v <> v2;

        hence thesis by A18, A17, Th48;

      end;

        suppose

         A19: v = v1 or v = v2;

        then ( Degree (v9,( rng c9e))) = (( Degree (v,( rng c9e))) + 1) by A4, A15, Th47;

        then ( Degree (v,( rng c9e))) = (dv9 - 1);

        hence thesis by A16, A19, Th31;

      end;

    end;

    reserve G for Graph,

v for Vertex of G,

vs for FinSequence of the carrier of G;

    definition

      let G be Graph;

      :: GRAPH_3:def8

      func G -CycleSet -> FinSequenceSet of the carrier' of G means

      : Def8: for x be set holds x in it iff x is cyclic Path of G;

      existence

      proof

        defpred P[ set] means $1 is cyclic Path of G;

        set IT = { p where p be Element of (the carrier' of G * ) : P[p] };

        IT is Subset of (the carrier' of G * ) from DOMAIN_1:sch 7;

        then for x be object st x in IT holds x is FinSequence of the carrier' of G by FINSEQ_1:def 11;

        then

        reconsider IT as FinSequenceSet of the carrier' of G by FINSEQ_2:def 3;

        reconsider p = {} as Path of G by GRAPH_1: 14;

        set v = the Vertex of G;

        reconsider IT as FinSequenceSet of the carrier' of G;

        take IT;

        let x be set;

        hereby

          assume x in IT;

          then ex p be Element of (the carrier' of G * ) st p = x & p is cyclic Path of G;

          hence x is cyclic Path of G;

        end;

        assume

         A1: x is cyclic Path of G;

        then x is Element of (the carrier' of G * ) by FINSEQ_1:def 11;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be FinSequenceSet of the carrier' of G such that

         A2: for x be set holds x in it1 iff x is cyclic Path of G and

         A3: for x be set holds x in it2 iff x is cyclic Path of G;

        now

          let x be object;

          x in it1 iff x is cyclic Path of G by A2;

          hence x in it1 iff x in it2 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: GRAPH_3:51

    

     Th51: {} in (G -CycleSet )

    proof

      reconsider p = {} as Path of G by GRAPH_1: 14;

      set v = the Vertex of G;

       <*v*> is_vertex_seq_of p & ( <*v*> . 1) = ( <*v*> . ( len <*v*>)) by FINSEQ_1: 40;

      then p is cyclic;

      hence thesis by Def8;

    end;

    registration

      let G be Graph;

      cluster (G -CycleSet ) -> non empty;

      coherence by Th51;

    end

    theorem :: GRAPH_3:52

    

     Th52: for c be Element of (G -CycleSet ) st v in (G -VSet ( rng c)) holds { c9 where c9 be Element of (G -CycleSet ) : ( rng c9) = ( rng c) & ex vs st vs is_vertex_seq_of c9 & (vs . 1) = v } is non empty Subset of (G -CycleSet )

    proof

      let c be Element of (G -CycleSet );

      set Cset = { c9 where c9 be Element of (G -CycleSet ) : ( rng c9) = ( rng c) & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c9 & (vs . 1) = v };

      reconsider c9 = c as cyclic Path of G by Def8;

      consider vs be FinSequence of the carrier of G such that

       A1: vs is_vertex_seq_of c9 by GRAPH_2: 33;

      

       A2: ( len vs) = (( len c) + 1) by A1;

      assume

       A3: v in (G -VSet ( rng c));

      then

       A4: ex vv be Vertex of G st vv = v & ex e be Element of the carrier' of G st e in ( rng c) & (vv = (the Source of G . e) or vv = (the Target of G . e));

      then (G -VSet ( rng c9)) = ( rng vs) by A1, GRAPH_2: 31, RELAT_1: 38;

      then

      consider n be Nat such that

       A5: n in ( dom vs) and

       A6: (vs . n) = v by A3, FINSEQ_2: 10;

      reconsider n as Element of NAT by ORDINAL1:def 12;

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

      then

       A7: 1 <= n & n <= ( len vs) by A5, FINSEQ_1: 1;

       A8:

      now

        per cases by A7, XXREAL_0: 1;

          suppose 1 = n & n = ( len vs);

          then ( 0 + 1) = (( len c) + 1) by A1;

          then c = {} ;

          hence Cset is non empty by A4;

        end;

          suppose 1 = n;

          then c in Cset by A1, A6;

          hence Cset is non empty;

        end;

          suppose n = ( len vs);

          then (vs . 1) = v by A1, A6, MSSCYC_1: 6;

          then c in Cset by A1;

          hence Cset is non empty;

        end;

          suppose

           A9: 1 < n & n < ( len vs);

          set vs2 = ((n,( len vs)) -cut vs);

          consider m be Element of NAT such that

           A10: n = (1 + m) and

           A11: 1 <= m by A9, FINSEQ_4: 84;

          set vs1 = ((1,(m + 1)) -cut vs);

          

           A12: 1 <= ((m + 1) + 1) by A9, A10, NAT_1: 13;

          then

           A13: (( len vs1) + 1) = ((m + 1) + 1) by A9, A10, Lm1;

          then

           A14: (vs1 . 1) = (vs . (1 + 0 )) by A9, A10, A12, Lm1;

          reconsider c1 = ((1,m) -cut c9), c2 = ((n,( len c)) -cut c9) as Path of G by Th5;

          

           A15: n <= ( len c) by A2, A9, NAT_1: 13;

          then

           A16: vs2 is_vertex_seq_of c2 by A1, A9, GRAPH_2: 42;

          

           A17: (( len vs2) + n) = (( len vs) + 1) by A9, FINSEQ_6:def 4;

           A18:

          now

            assume ( len vs2) = 0 ;

            then (( len vs) + 1) < (( len vs) + 0 ) by A9, A17;

            hence contradiction by XREAL_1: 6;

          end;

          then

           A19: (1 + 0 ) <= ( len vs2) by NAT_1: 13;

          then

          consider lv2 be Nat such that 0 <= lv2 and

           A20: lv2 < ( len vs2) and

           A21: ( len vs2) = (lv2 + 1) by FINSEQ_6: 127;

          reconsider vs21 = (vs2 ^' vs1) as FinSequence of the carrier of G;

          

           A22: (vs21 . 1) = (vs2 . ( 0 + 1)) by A19, FINSEQ_6: 140

          .= (vs . (n + 0 )) by A9, A18, FINSEQ_6:def 4;

          

           A23: m <= (m + 1) by NAT_1: 11;

          then m <= ( len c) by A10, A15, XXREAL_0: 2;

          then

           A24: vs1 is_vertex_seq_of c1 by A1, A11, GRAPH_2: 42;

          

           A25: (vs2 . ( len vs2)) = (vs . (n + lv2)) by A9, A20, A21, FINSEQ_6:def 4

          .= (vs1 . 1) by A1, A17, A21, A14, MSSCYC_1: 6;

          now

            given y be object such that

             A26: y in ( rng c1) and

             A27: y in ( rng c2);

            consider b be Nat such that

             A28: b in ( dom c2) and

             A29: (c2 . b) = y by A27, FINSEQ_2: 10;

            

             A30: ex l be Nat st l in ( dom c9) & (c . l) = (c2 . b) & (l + 1) = (n + b) & n <= l & l <= ( len c) by A28, Th2;

            consider a be Nat such that

             A31: a in ( dom c1) and

             A32: (c1 . a) = y by A26, FINSEQ_2: 10;

            consider k be Nat such that

             A33: k in ( dom c9) & (c . k) = (c1 . a) and (k + 1) = (1 + a) and 1 <= k and

             A34: k <= m by A31, Th2;

            k < n by A10, A34, NAT_1: 13;

            hence contradiction by A32, A29, A33, A30, FUNCT_1:def 4;

          end;

          then ( rng c1) misses ( rng c2) by XBOOLE_0: 3;

          then

          reconsider c219 = (c2 ^ c1) as Path of G by A24, A16, A25, Th6;

          

           A35: vs21 is_vertex_seq_of c219 by A24, A16, A25, GRAPH_2: 44;

          

           A36: c = (c1 ^ c2) by A10, A15, A23, FINSEQ_6: 135, XXREAL_0: 2;

          1 < ( len vs1) by A11, A13, NAT_1: 13;

          

          then (vs21 . ( len vs21)) = (vs1 . ( len vs1)) by FINSEQ_6: 142

          .= (vs . n) by A9, A10, FINSEQ_6: 138;

          then

          reconsider c219 as cyclic Path of G by A22, A35, MSSCYC_1:def 2;

          reconsider c21 = c219 as Element of (G -CycleSet ) by Def8;

          ( rng c21) = (( rng c2) \/ ( rng c1)) by FINSEQ_1: 31

          .= ( rng c) by A36, FINSEQ_1: 31;

          then c21 in Cset by A6, A22, A35;

          hence Cset is non empty;

        end;

      end;

      Cset c= (G -CycleSet )

      proof

        let x be object;

        assume x in Cset;

        then ex c9 be Element of (G -CycleSet ) st c9 = x & ( rng c9) = ( rng c) & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c9 & (vs . 1) = v;

        hence thesis;

      end;

      hence thesis by A8;

    end;

    definition

      let G, v;

      let c be Element of (G -CycleSet );

      assume

       A1: v in (G -VSet ( rng c));

      :: GRAPH_3:def9

      func Rotate (c,v) -> Element of (G -CycleSet ) equals

      : Def9: the Element of { c9 where c9 be Element of (G -CycleSet ) : ( rng c9) = ( rng c) & ex vs st vs is_vertex_seq_of c9 & (vs . 1) = v };

      coherence

      proof

        set Rotated = { c9 where c9 be Element of (G -CycleSet ) : ( rng c9) = ( rng c) & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c9 & (vs . 1) = v };

        set IT = the Element of Rotated;

        Rotated is non empty by A1, Th52;

        then IT in Rotated;

        then ex c9 be Element of (G -CycleSet ) st IT = c9 & ( rng c9) = ( rng c) & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c9 & (vs . 1) = v;

        hence thesis;

      end;

    end

    

     Lm5: for G be Graph, c be Element of (G -CycleSet ), v be Vertex of G st v in (G -VSet ( rng c)) holds ( rng ( Rotate (c,v))) = ( rng c)

    proof

      let G be Graph, c be Element of (G -CycleSet ), v be Vertex of G;

      assume

       A1: v in (G -VSet ( rng c));

      then

      reconsider Rotated = { c9 where c9 be Element of (G -CycleSet ) : ( rng c9) = ( rng c) & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c9 & (vs . 1) = v } as non empty Subset of (G -CycleSet ) by Th52;

      ( Rotate (c,v)) = the Element of Rotated by A1, Def9;

      then ( Rotate (c,v)) in Rotated;

      then ex c9 be Element of (G -CycleSet ) st ( Rotate (c,v)) = c9 & ( rng c9) = ( rng c) & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c9 & (vs . 1) = v;

      hence thesis;

    end;

    definition

      let G be Graph, c1,c2 be Element of (G -CycleSet );

      assume that

       A1: (G -VSet ( rng c1)) meets (G -VSet ( rng c2)) and

       A2: ( rng c1) misses ( rng c2);

      :: GRAPH_3:def10

      func CatCycles (c1,c2) -> Element of (G -CycleSet ) means

      : Def10: ex v be Vertex of G st v = the Element of ((G -VSet ( rng c1)) /\ (G -VSet ( rng c2))) & it = (( Rotate (c1,v)) ^ ( Rotate (c2,v)));

      existence

      proof

        set v = the Element of ((G -VSet ( rng c1)) /\ (G -VSet ( rng c2)));

        

         A3: ((G -VSet ( rng c1)) /\ (G -VSet ( rng c2))) is non empty by A1;

        then

         A4: v in ((G -VSet ( rng c1)) /\ (G -VSet ( rng c2)));

        

         A5: v in (G -VSet ( rng c1)) by A3, XBOOLE_0:def 4;

        

         A6: v in (G -VSet ( rng c2)) by A3, XBOOLE_0:def 4;

        reconsider v as Vertex of G by A4;

        reconsider Rotated2 = { c9 where c9 be Element of (G -CycleSet ) : ( rng c9) = ( rng c2) & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c9 & (vs . 1) = v } as non empty Subset of (G -CycleSet ) by A6, Th52;

        set r2 = ( Rotate (c2,v));

        r2 = the Element of Rotated2 by A6, Def9;

        then r2 in Rotated2;

        then

        consider c99 be Element of (G -CycleSet ) such that

         A7: r2 = c99 and

         A8: ( rng c99) = ( rng c2) and

         A9: ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c99 & (vs . 1) = v;

        consider vs2 be FinSequence of the carrier of G such that

         A10: vs2 is_vertex_seq_of c99 and

         A11: (vs2 . 1) = v by A9;

        reconsider c92 = c99 as cyclic Path of G by Def8;

        

         A12: r2 = c92 by A7;

        ( rng c2) is non empty by A6, Th16;

        then c99 is non empty by A8;

        then ( 0 + 1) < (( len c99) + 1) by XREAL_1: 6;

        then

         A13: 1 < ( len vs2) by A10;

        

         A14: vs2 is_vertex_seq_of c92 by A10;

        reconsider Rotated1 = { c9 where c9 be Element of (G -CycleSet ) : ( rng c9) = ( rng c1) & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c9 & (vs . 1) = v } as non empty Subset of (G -CycleSet ) by A5, Th52;

        set r1 = ( Rotate (c1,v));

        r1 = the Element of Rotated1 by A5, Def9;

        then r1 in Rotated1;

        then

        consider c9 be Element of (G -CycleSet ) such that

         A15: r1 = c9 and

         A16: ( rng c9) = ( rng c1) and

         A17: ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c9 & (vs . 1) = v;

        reconsider c91 = c9 as cyclic Path of G by Def8;

        consider vs1 be FinSequence of the carrier of G such that

         A18: vs1 is_vertex_seq_of c9 and

         A19: (vs1 . 1) = v by A17;

        vs1 is_vertex_seq_of c91 by A18;

        then

         A20: (vs1 . 1) = (vs1 . ( len vs1)) by MSSCYC_1: 6;

        set vs12 = (vs1 ^' vs2);

        ( len vs1) = (( len c9) + 1) by A18;

        then 1 <= ( len vs1) by NAT_1: 11;

        

        then

         A21: (vs12 . 1) = (vs1 . 1) by FINSEQ_6: 140

        .= (vs2 . ( len vs2)) by A19, A11, A14, MSSCYC_1: 6

        .= (vs12 . ( len vs12)) by A13, FINSEQ_6: 142;

        

         A22: r1 = c91 by A15;

        then

        reconsider c = (r1 ^ r2) as Path of G by A2, A16, A8, A18, A19, A10, A11, A20, A12, Th6;

        vs12 is_vertex_seq_of c by A18, A19, A10, A11, A20, A22, A12, GRAPH_2: 44;

        then c is cyclic by A21;

        then

        reconsider c as Element of (G -CycleSet ) by Def8;

        take c;

        take v;

        thus thesis;

      end;

      correctness ;

    end

    theorem :: GRAPH_3:53

    

     Th53: for G be Graph, c1,c2 be Element of (G -CycleSet ) st (G -VSet ( rng c1)) meets (G -VSet ( rng c2)) & ( rng c1) misses ( rng c2) & (c1 <> {} or c2 <> {} ) holds ( CatCycles (c1,c2)) is non empty

    proof

      let G be Graph, c1,c2 be Element of (G -CycleSet );

      assume that

       A1: (G -VSet ( rng c1)) meets (G -VSet ( rng c2)) and

       A2: ( rng c1) misses ( rng c2) and

       A3: c1 <> {} or c2 <> {} ;

      consider v be Vertex of G such that

       A4: v = the Element of ((G -VSet ( rng c1)) /\ (G -VSet ( rng c2))) and

       A5: ( CatCycles (c1,c2)) = (( Rotate (c1,v)) ^ ( Rotate (c2,v))) by A1, A2, Def10;

      

       A6: ((G -VSet ( rng c1)) /\ (G -VSet ( rng c2))) <> {} by A1;

      then

       A7: v in (G -VSet ( rng c1)) by A4, XBOOLE_0:def 4;

      

       A8: v in (G -VSet ( rng c2)) by A4, A6, XBOOLE_0:def 4;

      per cases by A3;

        suppose c1 <> {} ;

        then ( rng ( Rotate (c1,v))) <> {} by A7, Lm5;

        hence thesis by A5, FINSEQ_1: 35, RELAT_1: 38;

      end;

        suppose c2 <> {} ;

        then ( rng ( Rotate (c2,v))) <> {} by A8, Lm5;

        hence thesis by A5, FINSEQ_1: 35, RELAT_1: 38;

      end;

    end;

    reserve G for finite Graph,

v for Vertex of G,

vs for FinSequence of the carrier of G;

    definition

      let G, v;

      let X be set;

      assume

       A1: ( Degree (v,X)) <> 0 ;

      :: GRAPH_3:def11

      func X -PathSet v -> non empty FinSequenceSet of the carrier' of G equals

      : Def11: { c where c be Element of (X * ) : c is Path of G & c is non empty & ex vs st vs is_vertex_seq_of c & (vs . 1) = v };

      coherence

      proof

        set e = the Element of ( Edges_At (v,X));

        set IT = { c where c be Element of (X * ) : c is Path of G & c is non empty & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c & (vs . 1) = v };

         A2:

        now

          let x be object;

          assume x in IT;

          then ex c be Element of (X * ) st x = c & c is Path of G & c is non empty & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c & (vs . 1) = v;

          hence x is FinSequence of the carrier' of G;

        end;

        

         A3: not ( Edges_At (v,X)) is empty by A1, Th25;

        now

          per cases by A3, XBOOLE_0:def 3;

            suppose

             A4: e in ( Edges_In (v,X));

            then e in X & (the Target of G . e) = v by Def1;

            hence ex e9 be Element of X st e = e9 & e9 in X & e9 in the carrier' of G & (v = (the Target of G . e9) or v = (the Source of G . e9)) by A4;

          end;

            suppose

             A5: e in ( Edges_Out (v,X));

            then e in X & (the Source of G . e) = v by Def2;

            hence ex e9 be Element of X st e = e9 & e9 in X & e9 in the carrier' of G & (v = (the Target of G . e9) or v = (the Source of G . e9)) by A5;

          end;

        end;

        then

        consider e9 be Element of X such that e = e9 and

         A6: e9 in X and

         A7: e9 in the carrier' of G and

         A8: v = (the Target of G . e9) or v = (the Source of G . e9);

        reconsider X9 = X as non empty set by A6;

        reconsider e9 as Element of X9;

        reconsider c = <*e9*> as Element of (X * ) by FINSEQ_1:def 11;

        

         A9: ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c & (vs . 1) = v

        proof

          set s = (the Source of G . e9);

          reconsider s as Vertex of G by A7, FUNCT_2: 5;

          set t = (the Target of G . e9);

          reconsider t as Vertex of G by A7, FUNCT_2: 5;

          per cases by A8;

            suppose

             A10: v = (the Target of G . e9);

            take <*t, s*>;

            thus thesis by A10, Th11, FINSEQ_1: 44;

          end;

            suppose

             A11: v = (the Source of G . e9);

            take <*s, t*>;

            thus thesis by A11, FINSEQ_1: 44, MSSCYC_1: 4;

          end;

        end;

        c is Path of G by A7, Th4;

        then c in IT by A9;

        hence thesis by A2, FINSEQ_2:def 3;

      end;

    end

    theorem :: GRAPH_3:54

    

     Th54: for p be Element of (X -PathSet v), Y be finite set st Y = the carrier' of G & ( Degree (v,X)) <> 0 holds ( len p) <= ( card Y)

    proof

      let p be Element of (X -PathSet v), Y be finite set;

      assume that

       A1: Y = the carrier' of G and

       A2: ( Degree (v,X)) <> 0 ;

      

       A3: p in (X -PathSet v);

      (X -PathSet v) = { c where c be Element of (X * ) : c is Path of G & c is non empty & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c & (vs . 1) = v } by A2, Def11;

      then ex c be Element of (X * ) st p = c & c is Path of G & c is non empty & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c & (vs . 1) = v by A3;

      then

       A4: ( card ( rng p)) = ( len p) by FINSEQ_4: 62;

      ( rng p) c= Y by A1, FINSEQ_1:def 4;

      hence thesis by A4, NAT_1: 43;

    end;

    definition

      let G, v;

      let X be set;

      assume that

       A1: for v be Vertex of G holds ( Degree (v,X)) is even and

       A2: ( Degree (v,X)) <> 0 ;

      :: GRAPH_3:def12

      func X -CycleSet v -> non empty Subset of (G -CycleSet ) equals

      : Def12: { c where c be Element of (G -CycleSet ) : ( rng c) c= X & c is non empty & ex vs st vs is_vertex_seq_of c & (vs . 1) = v };

      coherence

      proof

        reconsider E = the carrier' of G as finite set by GRAPH_1:def 11;

        set XL = the set of all ( len p) where p be Element of (X -PathSet v);

        set IT = { c where c be Element of (G -CycleSet ) : ( rng c) c= X & c is non empty & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c & (vs . 1) = v };

        set p = the Element of (X -PathSet v);

        

         A3: ( len p) in XL;

        

         A4: XL c= NAT

        proof

          let x be object;

          assume x in XL;

          then ex p be Element of (X -PathSet v) st x = ( len p);

          hence thesis;

        end;

        

         A5: (X -PathSet v) = { c where c be Element of (X * ) : c is Path of G & c is non empty & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c & (vs . 1) = v } by A2, Def11;

        XL c= ( Seg ( card E))

        proof

          let x be object;

          assume x in XL;

          then

          consider p be Element of (X -PathSet v) such that

           A6: x = ( len p);

          p in (X -PathSet v);

          then ex c be Element of (X * ) st p = c & c is Path of G & c is non empty & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c & (vs . 1) = v by A5;

          then

           A7: ( 0 + 1) <= ( len p) by NAT_1: 13;

          ( len p) <= ( card E) by A2, Th54;

          hence thesis by A6, A7, FINSEQ_1: 1;

        end;

        then

        reconsider XL as finite non empty Subset of NAT by A3, A4;

        set maxl = ( max XL);

        maxl in XL by XXREAL_2:def 8;

        then

        consider p be Element of (X -PathSet v) such that

         A8: maxl = ( len p);

        p in (X -PathSet v);

        then

        consider c be Element of (X * ) such that

         A9: p = c and

         A10: c is Path of G and

         A11: c is non empty and

         A12: ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c & (vs . 1) = v by A5;

        reconsider p as Path of G by A9, A10;

        

         A13: ( rng c) c= X by FINSEQ_1:def 4;

        now

          set T = the Target of G;

          set S = the Source of G;

          

           A14: ( rng p) c= X by A9, FINSEQ_1:def 4;

          consider vs be FinSequence of the carrier of G such that

           A15: vs is_vertex_seq_of p and

           A16: (vs . 1) = v by A9, A12;

          ( len vs) = (( len p) + 1) by A15;

          then

           A17: 1 <= ( len vs) by NAT_1: 11;

          then ( len vs) in ( dom vs) by FINSEQ_3: 25;

          then

          reconsider v1 = (vs . ( len vs)) as Vertex of G by FINSEQ_2: 11;

          assume not p is cyclic;

          then

           A18: ( Degree (v1,( rng p))) is odd by A15, Th50;

          then ( rng p) <> X by A1;

          then ( rng p) c< X by A14;

          then ex xx be object st xx in X & not xx in ( rng p) by XBOOLE_0: 6;

          then

          reconsider Xp = (X \ ( rng p)) as non empty set by XBOOLE_0:def 5;

          set e = the Element of ( Edges_At (v1,Xp));

          ( Degree (v1,Xp)) = (( Degree (v1,X)) - ( Degree (v1,( rng p)))) by A14, Th29;

          then ( Degree (v1,Xp)) <> 0 by A1, A18;

          then

           A19: not ( Edges_At (v1,Xp)) is empty by Th25;

           A20:

          now

            per cases by A19, XBOOLE_0:def 3;

              suppose

               A21: e in ( Edges_In (v1,Xp));

              then e in Xp & (the Target of G . e) = v1 by Def1;

              hence ex e9 be Element of Xp st e = e9 & e9 in Xp & e9 in the carrier' of G & (v1 = (the Target of G . e9) or v1 = (the Source of G . e9)) by A21;

            end;

              suppose

               A22: e in ( Edges_Out (v1,Xp));

              then e in Xp & (the Source of G . e) = v1 by Def2;

              hence ex e9 be Element of Xp st e = e9 & e9 in Xp & e9 in the carrier' of G & (v1 = (the Target of G . e9) or v1 = (the Source of G . e9)) by A22;

            end;

          end;

          then

          reconsider ep = <*e*> as Path of G by Th4;

          reconsider t = (T . e), s = (S . e) as Vertex of G by A20, FUNCT_2: 5;

          now

            given x be object such that

             A23: x in ( rng ep) and

             A24: x in ( rng p);

            ( rng ep) = {e} by FINSEQ_1: 38;

            then x in Xp by A20, A23, TARSKI:def 1;

            hence contradiction by A24, XBOOLE_0:def 5;

          end;

          then

           A25: ( rng ep) misses ( rng p) by XBOOLE_0: 3;

          per cases by A20;

            suppose

             A26: v1 = (T . e);

            reconsider ts = <*t, s*> as FinSequence of the carrier of G;

            

             A27: (vs . ( len vs)) = (ts . 1) by A26, FINSEQ_1: 44;

            reconsider X9 = X as non empty set by A20;

            reconsider vs1 = (vs ^' ts) as FinSequence of the carrier of G;

            reconsider e9 = e as Element of X9 by A20;

            

             A28: (vs1 . 1) = v by A16, A17, FINSEQ_6: 140;

            

             A29: ts is_vertex_seq_of ep by Th11;

            then

            reconsider p1 = (p ^ ep) as Path of G by A15, A25, A27, Th6;

            

             A30: ( len p1) = (( len p) + ( len ep)) by FINSEQ_1: 22

            .= (( len p) + 1) by FINSEQ_1: 39;

            reconsider p as FinSequence of X by A9;

            reconsider ep = <*e9*> as FinSequence of X;

            reconsider xp1 = (p ^ ep) as Element of (X * ) by FINSEQ_1:def 11;

            vs1 is_vertex_seq_of p1 by A15, A29, A27, GRAPH_2: 44;

            then xp1 in (X -PathSet v) by A5, A28;

            then

            reconsider xp1 as Element of (X -PathSet v);

            ( len xp1) in XL;

            then (( len p) + 1) <= (( len p) + 0 ) by A8, A30, XXREAL_2:def 8;

            hence contradiction by XREAL_1: 6;

          end;

            suppose

             A31: v1 = (S . e);

            reconsider ts = <*s, t*> as FinSequence of the carrier of G;

            

             A32: ts is_vertex_seq_of ep & (vs . ( len vs)) = (ts . 1) by A31, FINSEQ_1: 44, MSSCYC_1: 4;

            then

            reconsider p1 = (p ^ ep) as Path of G by A15, A25, Th6;

            

             A33: ( len p1) = (( len p) + ( len ep)) by FINSEQ_1: 22

            .= (( len p) + 1) by FINSEQ_1: 39;

            reconsider X9 = X as non empty set by A20;

            reconsider vs1 = (vs ^' ts) as FinSequence of the carrier of G;

            reconsider e9 = e as Element of X9 by A20;

            

             A34: (vs1 . 1) = v by A16, A17, FINSEQ_6: 140;

            reconsider p as FinSequence of X by A9;

            reconsider ep = <*e9*> as FinSequence of X;

            reconsider xp1 = (p ^ ep) as Element of (X * ) by FINSEQ_1:def 11;

            vs1 is_vertex_seq_of p1 by A15, A32, GRAPH_2: 44;

            then xp1 in (X -PathSet v) by A5, A34;

            then

            reconsider xp1 as Element of (X -PathSet v);

            ( len xp1) in XL;

            then (( len p) + 1) <= (( len p) + 0 ) by A8, A33, XXREAL_2:def 8;

            hence contradiction by XREAL_1: 6;

          end;

        end;

        then

        reconsider c as Element of (G -CycleSet ) by A9, Def8;

         A35:

        now

          let c be object;

          assume c in IT;

          then ex c9 be Element of (G -CycleSet ) st c = c9 & ( rng c9) c= X & c9 is non empty & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c9 & (vs . 1) = v;

          hence c in (G -CycleSet );

        end;

        c in IT by A11, A12, A13;

        hence thesis by A35, TARSKI:def 3;

      end;

    end

    theorem :: GRAPH_3:55

    

     Th55: ( Degree (v,X)) <> 0 & (for v holds ( Degree (v,X)) is even) implies for c be Element of (X -CycleSet v) holds c is non empty & ( rng c) c= X & v in (G -VSet ( rng c))

    proof

      assume ( Degree (v,X)) <> 0 & for v holds ( Degree (v,X)) is even;

      then

       A1: (X -CycleSet v) = { c9 where c9 be Element of (G -CycleSet ) : ( rng c9) c= X & c9 is non empty & ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c9 & (vs . 1) = v } by Def12;

      let c be Element of (X -CycleSet v);

      c in (X -CycleSet v);

      then

      consider c9 be Element of (G -CycleSet ) such that

       A2: c = c9 and

       A3: ( rng c9) c= X and

       A4: c9 is non empty and

       A5: ex vs be FinSequence of the carrier of G st vs is_vertex_seq_of c9 & (vs . 1) = v by A1;

      thus c is non empty by A2, A4;

      thus ( rng c) c= X by A2, A3;

      reconsider c9 as Path of G by Def8;

      consider vs be FinSequence of the carrier of G such that

       A6: vs is_vertex_seq_of c9 and

       A7: (vs . 1) = v by A5;

      ( len vs) = (( len c9) + 1) by A6;

      then 1 <= ( len vs) by NAT_1: 11;

      then

       A8: 1 in ( dom vs) by FINSEQ_3: 25;

      (G -VSet ( rng c9)) = ( rng vs) by A4, A6, GRAPH_2: 31;

      hence thesis by A2, A7, A8, FUNCT_1:def 3;

    end;

    theorem :: GRAPH_3:56

    

     Th56: for G be finite connected Graph, c be Element of (G -CycleSet ) st ( rng c) <> the carrier' of G & c is non empty holds { v9 where v9 be Vertex of G : v9 in (G -VSet ( rng c)) & ( Degree v9) <> ( Degree (v9,( rng c))) } is non empty Subset of the carrier of G

    proof

      let G be finite connected Graph, c be Element of (G -CycleSet );

      defpred P[ Vertex of G] means $1 in (G -VSet ( rng c)) & ( Degree $1) <> ( Degree ($1,( rng c)));

      set X = { v9 where v9 be Vertex of G : P[v9] };

      set T = the Target of G;

      set S = the Source of G;

      set E = the carrier' of G;

      

       A1: ( rng c) c= E by FINSEQ_1:def 4;

      reconsider cp = c as cyclic Path of G by Def8;

      assume that

       A2: ( rng c) <> the carrier' of G and

       A3: c is non empty;

      consider vs be FinSequence of the carrier of G such that

       A4: vs is_vertex_seq_of cp by GRAPH_2: 33;

      

       A5: (G -VSet ( rng cp)) = ( rng vs) by A3, A4, GRAPH_2: 31;

      now

        consider x be object such that

         A6: not (x in ( rng c) iff x in E) by A2, TARSKI: 2;

        reconsider x as Element of E by A1, A6;

        reconsider v = (the Target of G . x) as Vertex of G by A1, A6, FUNCT_2: 5;

        per cases ;

          suppose

           A7: v in ( rng vs);

          ( Degree v) <> ( Degree (v,( rng c))) by A1, A6, Th26;

          hence ex v be Vertex of G st v in ( rng vs) & ( Degree v) <> ( Degree (v,( rng c))) by A7;

        end;

          suppose

           A8: not v in ( rng vs);

          

           A9: ex e be object st e in ( rng c) by A3, XBOOLE_0:def 1;

          then ( rng c) meets E by A1, XBOOLE_0: 3;

          then

          consider v9 be Vertex of G, e be Element of E such that

           A10: v9 in ( rng vs) and

           A11: ( not e in ( rng c)) & (v9 = (T . e) or v9 = (S . e)) by A5, A8, Th19;

          ( Degree v9) <> ( Degree (v9,( rng c))) by A1, A9, A11, Th26;

          hence ex v be Vertex of G st v in ( rng vs) & ( Degree v) <> ( Degree (v,( rng c))) by A10;

        end;

      end;

      then

      consider v be Vertex of G such that

       A12: v in ( rng vs) & ( Degree v) <> ( Degree (v,( rng c)));

      

       A13: X is Subset of the carrier of G from DOMAIN_1:sch 7;

      v in X by A5, A12;

      hence thesis by A13;

    end;

    definition

      let G be finite connected Graph, c be Element of (G -CycleSet );

      assume that

       A1: ( rng c) <> the carrier' of G and

       A2: c is non empty;

      :: GRAPH_3:def13

      func ExtendCycle c -> Element of (G -CycleSet ) means

      : Def13: ex c9 be Element of (G -CycleSet ), v be Vertex of G st v = the Element of { v9 where v9 be Vertex of G : v9 in (G -VSet ( rng c)) & ( Degree v9) <> ( Degree (v9,( rng c))) } & c9 = the Element of ((the carrier' of G \ ( rng c)) -CycleSet v) & it = ( CatCycles (c,c9));

      existence

      proof

        set X = { v9 where v9 be Vertex of G : v9 in (G -VSet ( rng c)) & ( Degree v9) <> ( Degree (v9,( rng c))) };

        set v = the Element of X;

        X is non empty by A1, A2, Th56;

        then v in X;

        then ex v9 be Vertex of G st v = v9 & v9 in (G -VSet ( rng c)) & ( Degree v9) <> ( Degree (v9,( rng c)));

        then

        reconsider v as Vertex of G;

        set E = the carrier' of G;

        reconsider E9 = E as finite set by GRAPH_1:def 11;

        ( rng c) c= E by FINSEQ_1:def 4;

        then ( rng c) c< E by A1;

        then ex xx be object st xx in E & not xx in ( rng c) by XBOOLE_0: 6;

        then

        reconsider Erc = (E9 \ ( rng c)) as finite non empty set by XBOOLE_0:def 5;

        set c9 = the Element of (Erc -CycleSet v);

        c9 in (Erc -CycleSet v);

        then

        reconsider c9 as Element of (G -CycleSet );

        reconsider IT = ( CatCycles (c,c9)) as Element of (G -CycleSet );

        take IT;

        take c9;

        take v;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: GRAPH_3:57

    

     Th57: for G be finite connected Graph, c be Element of (G -CycleSet ) st ( rng c) <> the carrier' of G & c is non empty & for v be Vertex of G holds ( Degree v) is even holds ( ExtendCycle c) is non empty & ( card ( rng c)) < ( card ( rng ( ExtendCycle c)))

    proof

      let G be finite connected Graph, c be Element of (G -CycleSet );

      set E = the carrier' of G;

      reconsider E9 = E as finite set by GRAPH_1:def 11;

      reconsider ccp = c as cyclic Path of G by Def8;

      assume that

       A1: ( rng c) <> the carrier' of G and

       A2: c is non empty and

       A3: for v be Vertex of G holds ( Degree v) is even;

      

       A4: ( rng c) c= E by FINSEQ_1:def 4;

      then ( rng c) c< the carrier' of G by A1;

      then ex xx be object st xx in E & not xx in ( rng c) by XBOOLE_0: 6;

      then

      reconsider Erc = (E9 \ ( rng c)) as finite non empty set by XBOOLE_0:def 5;

      reconsider X = { v9 where v9 be Vertex of G : v9 in (G -VSet ( rng c)) & ( Degree v9) <> ( Degree (v9,( rng c))) } as non empty set by A1, A2, Th56;

      consider c9 be Element of (G -CycleSet ), v be Vertex of G such that

       A5: v = the Element of X and

       A6: c9 = the Element of (Erc -CycleSet v) and

       A7: ( ExtendCycle c) = ( CatCycles (c,c9)) by A1, A2, Def13;

      v in X by A5;

      then

       A8: ex v9 be Vertex of G st v = v9 & v9 in (G -VSet ( rng c)) & ( Degree v9) <> ( Degree (v9,( rng c)));

       A9:

      now

        let v be Vertex of G;

        

         A10: ( Degree v) = ( Degree (v,E)) & ( Degree v) is even by A3, Th24;

        ( Degree (v,Erc)) = (( Degree (v,E9)) - ( Degree (v,( rng c)))) & ( Degree (v,( rng ccp))) is even by A4, Th29, Th49;

        hence ( Degree (v,Erc)) is even by A10;

      end;

      ( rng c) misses (E \ ( rng c)) by XBOOLE_1: 79;

      then

       A11: (( rng c) /\ (E \ ( rng c))) = {} ;

      ( Degree (v,Erc)) = (( Degree (v,E9)) - ( Degree (v,( rng c)))) by A4, Th29;

      then

       A12: ( Degree (v,Erc)) <> 0 by A8, Th24;

      then ( rng c9) c= (E \ ( rng c)) by A6, A9, Th55;

      

      then (( rng c) /\ ( rng c9)) = (( rng c) /\ ((E \ ( rng c)) /\ ( rng c9))) by XBOOLE_1: 28

      .= ( {} /\ ( rng c9)) by A11, XBOOLE_1: 16

      .= {} ;

      then

       A13: ( rng c) misses ( rng c9);

      v in (G -VSet ( rng c9)) by A6, A9, A12, Th55;

      then

       A14: (G -VSet ( rng c)) meets (G -VSet ( rng c9)) by A8, XBOOLE_0: 3;

      hence ( ExtendCycle c) is non empty by A2, A7, A13, Th53;

      consider vr be Vertex of G such that

       A15: vr = the Element of ((G -VSet ( rng c)) /\ (G -VSet ( rng c9))) and

       A16: ( CatCycles (c,c9)) = (( Rotate (c,vr)) ^ ( Rotate (c9,vr))) by A14, A13, Def10;

      

       A17: ((G -VSet ( rng c)) /\ (G -VSet ( rng c9))) <> {} by A14;

      then vr in (G -VSet ( rng c9)) by A15, XBOOLE_0:def 4;

      then

       A18: ( rng ( Rotate (c9,vr))) = ( rng c9) by Lm5;

      vr in (G -VSet ( rng c)) by A17, A15, XBOOLE_0:def 4;

      then ( rng ( Rotate (c,vr))) = ( rng c) by Lm5;

      then ( rng ( ExtendCycle c)) = (( rng c) \/ ( rng c9)) by A7, A16, A18, FINSEQ_1: 31;

      then

       A19: ( card ( rng ( ExtendCycle c))) = (( card ( rng c)) + ( card ( rng c9))) by A13, CARD_2: 40;

      c9 is non empty by A6, A9, A12, Th55;

      hence thesis by A19, XREAL_1: 29;

    end;

    begin

    definition

      let G be Graph;

      let p be Path of G;

      :: GRAPH_3:def14

      attr p is Eulerian means ( rng p) = the carrier' of G;

    end

    theorem :: GRAPH_3:58

    

     Th58: for G be connected Graph, p be Path of G, vs be FinSequence of the carrier of G st p is Eulerian & vs is_vertex_seq_of p holds ( rng vs) = the carrier of G

    proof

      let G be connected Graph, p be Path of G, vs be FinSequence of the carrier of G such that

       A1: p is Eulerian and

       A2: vs is_vertex_seq_of p and

       A3: ( rng vs) <> the carrier of G;

      consider x be object such that

       A4: x in ( rng vs) & not x in the carrier of G or x in the carrier of G & not x in ( rng vs) by A3, TARSKI: 2;

      vs <> {} by A2;

      then

      consider y be object such that

       A5: y in ( rng vs) by XBOOLE_0:def 1;

      

       A6: ( rng vs) c= the carrier of G by FINSEQ_1:def 4;

      then

      consider c be Chain of G, vs1 be FinSequence of the carrier of G such that

       A7: c is non empty and

       A8: vs1 is_vertex_seq_of c & (vs1 . 1) = x and (vs1 . ( len vs1)) = y by A4, A5, Th18;

      

       A9: 1 <= ( len c) by A7, NAT_1: 14;

      

       A10: ( rng p) = the carrier' of G by A1;

      reconsider c as FinSequence of the carrier' of G by MSSCYC_1:def 1;

      1 in ( dom c) by A9, FINSEQ_3: 25;

      then (c . 1) in the carrier' of G by PARTFUN1: 4;

      then (the Target of G . (c . 1)) in ( rng vs) & (the Source of G . (c . 1)) in ( rng vs) by A2, A10, Th15;

      hence contradiction by A6, A4, A8, A9, Lm3;

    end;

    theorem :: GRAPH_3:59

    

     Th59: for G be finite connected Graph holds (ex p be cyclic Path of G st p is Eulerian) iff for v be Vertex of G holds ( Degree v) is even

    proof

      let G be finite connected Graph;

      set E = the carrier' of G;

      hereby

        given c be cyclic Path of G such that

         A1: c is Eulerian;

        let v be Vertex of G;

        consider vs be FinSequence of the carrier of G such that

         A2: vs is_vertex_seq_of c and (vs . 1) = (vs . ( len vs)) by MSSCYC_1:def 2;

        ( rng vs) = the carrier of G by A1, A2, Th58;

        then

         A3: ( Degree (v,( rng c))) is even by A2, Lm4;

        ( rng c) = the carrier' of G by A1;

        hence ( Degree v) is even by A3, Th24;

      end;

      assume

       A4: for v be Vertex of G holds ( Degree v) is even;

      per cases ;

        suppose

         A5: G is void;

         {} is Element of (G -CycleSet ) by Th51;

        then

        reconsider ec = {} as cyclic Path of G by Def8;

        take ec;

        the carrier' of G is empty by A5;

        hence ( rng ec) = the carrier' of G;

      end;

        suppose G is non void;

        then

        reconsider G9 = G as non void finite connected Graph;

        reconsider V = the Element of the carrier of G as Vertex of G9;

        defpred P[ Nat, set, set] means ex E be Element of (G9 -CycleSet ) st E = $2 & $3 = ( ExtendCycle E);

         the Element of (E -CycleSet V) in (E -CycleSet V);

        then

        reconsider ec = the Element of (E -CycleSet V) as Element of (G9 -CycleSet );

        

         A6: for n be Nat holds for x be Element of (G9 -CycleSet ) holds ex y be Element of (G9 -CycleSet ) st P[n, x, y]

        proof

          let n;

          let x be Element of (G9 -CycleSet );

          take ( ExtendCycle x);

          thus thesis;

        end;

        consider f be sequence of (G9 -CycleSet ) such that

         A7: (f . 0 ) = ec & for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A6);

         A8:

        now

          let v be Vertex of G;

          ( Degree v) = ( Degree (v,E)) by Th24;

          hence ( Degree (v,E)) is even by A4;

        end;

        ( Degree V) = ( Degree (V,E)) by Th24;

        then

         A9: ( Degree (V,E)) <> 0 by Th33;

        now

          defpred P[ Nat] means ex c be Element of (G9 -CycleSet ) st c is non empty & c = (f . $1) & $1 <= ( card ( rng c));

          reconsider E as finite set by GRAPH_1:def 11;

          assume

           A10: not ex n be Nat, c be Element of (G9 -CycleSet ) st c = (f . n) & ( rng c) = the carrier' of G;

          

           A11: for n st P[n] holds P[(n + 1)]

          proof

            let n be Nat;

            given c be Element of (G9 -CycleSet ) such that

             A12: c is non empty and

             A13: c = (f . n) and

             A14: n <= ( card ( rng c));

            reconsider r = ( ExtendCycle c) as Element of (G9 -CycleSet );

            take r;

            ( rng c) <> E by A10, A13;

            hence r is non empty by A4, A12, Th57;

             P[n, (f . n), (f . (n + 1))] by A7;

            hence r = (f . (n + 1)) by A13;

            ( rng c) <> E by A10, A13;

            then n < ( card ( rng r)) by A4, A12, A14, Th57, XXREAL_0: 2;

            hence thesis by NAT_1: 13;

          end;

          

           A15: P[ 0 ]

          proof

            take ec;

            thus ec is non empty by A8, A9, Th55;

            thus ec = (f . 0 ) by A7;

            thus thesis;

          end;

          for n be Nat holds P[n] from NAT_1:sch 2( A15, A11);

          then

          consider c be Element of (G -CycleSet ) such that c is non empty and c = (f . (( card E) + 1)) and

           A16: (( card E) + 1) <= ( card ( rng c));

          ( rng c) c= E by FINSEQ_1:def 4;

          then ( card ( rng c)) <= ( card E) by NAT_1: 43;

          then (( card E) + 1) <= (( card E) + 0 ) by A16, XXREAL_0: 2;

          hence contradiction by XREAL_1: 6;

        end;

        then

        consider n be Nat, c be Element of (G -CycleSet ) such that c = (f . n) and

         A17: ( rng c) = the carrier' of G;

        reconsider c as cyclic Path of G by Def8;

        take c;

        thus ( rng c) = the carrier' of G by A17;

      end;

    end;

    theorem :: GRAPH_3:60

    for G be finite connected Graph holds (ex p be Path of G st p is non cyclic & p is Eulerian) iff ex v1,v2 be Vertex of G st v1 <> v2 & for v be Vertex of G holds ( Degree v) is even iff v <> v1 & v <> v2

    proof

      let G be finite connected Graph;

      set V = the carrier of G, E = the carrier' of G;

       A1:

      now

        assume {E} meets E;

        then

        consider x be object such that

         A2: x in {E} and

         A3: x in E by XBOOLE_0: 3;

        

         A: x = E by A2, TARSKI:def 1;

        reconsider xx = x as set by TARSKI: 1;

         not xx in xx;

        hence contradiction by A, A3;

      end;

      hereby

        given p be Path of G such that

         A4: p is non cyclic and

         A5: p is Eulerian;

        consider vs be FinSequence of the carrier of G such that

         A6: vs is_vertex_seq_of p by GRAPH_2: 33;

        ( len vs) = (( len p) + 1) by A6;

        then 1 <= ( len vs) by NAT_1: 11;

        then 1 in ( dom vs) & ( len vs) in ( dom vs) by FINSEQ_3: 25;

        then

        reconsider v1 = (vs . 1), v2 = (vs . ( len vs)) as Vertex of G by FINSEQ_2: 11;

        take v1, v2;

        thus v1 <> v2 by A4, A6;

        let v be Vertex of G;

        ( Degree v) = ( Degree (v,the carrier' of G)) by Th24

        .= ( Degree (v,( rng p))) by A5;

        hence ( Degree v) is even iff v <> v1 & v <> v2 by A4, A6, Th50;

      end;

      given v1,v2 be Vertex of G such that

       A7: v1 <> v2 and

       A8: for v be Vertex of G holds ( Degree v) is even iff v <> v1 & v <> v2;

      set G9 = ( AddNewEdge (v1,v2));

      set E9 = the carrier' of G9;

      

       A9: the carrier' of G9 = (the carrier' of G \/ {E}) by Def7;

      E in {E} by TARSKI:def 1;

      then

       A10: E in the carrier' of G9 by A9, XBOOLE_0:def 3;

      

       A11: E = (E9 /\ E) by A9, XBOOLE_1: 21;

      for v be Vertex of G9 holds ( Degree v) is even

      proof

        let v9 be Vertex of G9;

        reconsider v = v9 as Vertex of G by Def7;

        

         A12: ( Degree v9) = ( Degree (v9,E9)) by Th24;

        

         A13: ( Degree (v,E9)) = ( Degree (v,E)) by A11, Th31;

        per cases ;

          suppose

           A14: v9 <> v1 & v9 <> v2;

          

          then ( Degree v9) = ( Degree (v,E9)) by A12, Th48

          .= ( Degree v) by A13, Th24;

          hence thesis by A8, A14;

        end;

          suppose

           A15: v = v1 or v = v2;

          then

          reconsider dv = ( Degree v) as odd Element of NAT by A8;

          

           A16: (dv + 1) is even;

          ( Degree v9) = (( Degree (v,E9)) + 1) by A7, A10, A12, A15, Th47

          .= (( Degree v) + 1) by A13, Th24;

          hence thesis by A16;

        end;

      end;

      then

      consider P9 be cyclic Path of G9 such that

       A17: P9 is Eulerian by Th59;

      

       A18: ( rng P9) = the carrier' of G9 by A17;

      then

      consider n be Nat such that

       A19: n in ( dom P9) and

       A20: (P9 . n) = E by A10, FINSEQ_2: 10;

      consider p9 be cyclic Path of G9 such that

       A21: (p9 . 1) = (P9 . n) and

       A22: ( len p9) = ( len P9) and

       A23: ( rng p9) = ( rng P9) by A19, Th10;

      reconsider p = (((1 + 1),( len p9)) -cut p9) as Path of G9 by Th5;

      consider vs9 be FinSequence of the carrier of G9 such that

       A24: vs9 is_vertex_seq_of p9 by GRAPH_2: 33;

       A25:

      now

        assume E in ( rng p);

        then

        consider a be Nat such that

         A26: a in ( dom p) and

         A27: (p . a) = E by FINSEQ_2: 10;

        consider k be Nat such that

         A28: k in ( dom p9) and

         A29: (p9 . k) = (p . a) and (k + 1) = ((1 + 1) + a) and

         A30: (1 + 1) <= k and k <= ( len p9) by A26, Th2;

        1 in ( dom p9) by A28, FINSEQ_5: 6, RELAT_1: 38;

        then k = 1 by A20, A21, A27, A28, A29, FUNCT_1:def 4;

        hence contradiction by A30;

      end;

      

       A31: 1 <= n & n <= ( len P9) by A19, FINSEQ_3: 25;

      then

       A32: 1 <= ( len P9) by XXREAL_0: 2;

      then

      reconsider p1 = ((1,1) -cut p9) as Chain of G9 by A22, GRAPH_2: 41;

      

       A33: p9 = (p1 ^ (((1 + 1),( len p9)) -cut p9)) by A31, A22, FINSEQ_6: 135, XXREAL_0: 2;

      reconsider vs = (((1 + 1),( len vs9)) -cut vs9) as FinSequence of the carrier of G9;

      

       A34: ( len vs9) = (( len p9) + 1) by A24;

      now

        consider c be Chain of G, vs be FinSequence of V such that

         A35: c is non empty and vs is_vertex_seq_of c and (vs . 1) = v1 and (vs . ( len vs)) = v2 by A7, Th18;

        reconsider c as FinSequence of the carrier' of G by MSSCYC_1:def 1;

        1 in ( dom c) by A35, FINSEQ_5: 6;

        then

         A36: ( rng c) c= E & (c . 1) in ( rng c) by FINSEQ_1:def 4, FUNCT_1:def 3;

        then

         A37: (c . 1) in E;

        (c . 1) in the carrier' of G9 by A9, A36, XBOOLE_0:def 3;

        then

        consider m be Nat such that

         A38: m in ( dom P9) and

         A39: (P9 . m) = (c . 1) by A18, FINSEQ_2: 10;

        assume

         A40: ( len P9) = 1;

        1 <= m & m <= ( len P9) by A38, FINSEQ_3: 25;

        then

         A41: m = 1 by A40, XXREAL_0: 1;

        n = 1 by A31, A40, XXREAL_0: 1;

        hence contradiction by A20, A37, A39, A41;

      end;

      then 1 < ( len P9) by A32, XXREAL_0: 1;

      then

       A42: (1 + 1) <= ( len P9) by NAT_1: 13;

      then

       A43: vs is_vertex_seq_of p by A22, A24, GRAPH_2: 42;

      reconsider vs as FinSequence of the carrier of G by Def7;

      reconsider p as Path of G by A25, Th45;

      take p;

      

       A44: (the Source of G9 . E) = v1 & (the Target of G9 . E) = v2 by Th34;

      now

        (1 + 1) <= (( len p9) + 1) by A42, A22, NAT_1: 12;

        then

         A45: (1 + 1) <= (( len vs9) + 1) by A34, NAT_1: 12;

        then

         A46: (( len vs) + (1 + 1)) = (( len p9) + (1 + 1)) by A34, Lm1;

        then ( 0 + 1) <= ( len vs) by A31, A22, XXREAL_0: 2;

        then

        consider i be Nat such that 0 <= i and

         A47: i < ( len vs) and

         A48: ( len vs) = (i + 1) by FINSEQ_6: 127;

        ((( len vs) + 1) + 1) = (( len vs) + (1 + 1))

        .= (( len vs9) + 1) by A45, Lm1;

        then

         A49: ( len vs9) = (i + (1 + 1)) by A48;

        

         A50: (vs9 . 1) = (vs9 . ( len vs9)) by A24, MSSCYC_1: 6;

        

         A51: (vs9 . 1) = v1 & (vs9 . (1 + 1)) = v2 or (vs9 . 1) = v2 & (vs9 . (1 + 1)) = v1 by A44, A20, A32, A21, A22, A24, Lm3;

        assume

         A52: (vs . 1) = (vs . ( len vs));

        (vs . ( 0 + 1)) = (vs9 . ((1 + 1) + 0 )) by A31, A22, A45, A46, Lm1;

        hence contradiction by A7, A52, A45, A47, A48, A49, A50, A51, Lm1;

      end;

      hence p is non cyclic by A43, A25, Th46, MSSCYC_1: 6;

      ( rng <*E*>) = {E} & p1 = <*E*> by A20, A32, A21, A22, FINSEQ_1: 39, FINSEQ_6: 132;

      then ( rng p9) = ( {E} \/ ( rng p)) & {E} misses ( rng p) by A33, FINSEQ_1: 31, FINSEQ_3: 91;

      hence ( rng p) = E by A9, A18, A23, A1, XBOOLE_1: 72;

    end;