glib_013.miz



    begin

    theorem :: GLIB_013:1

    

     Th1: for G be non-Dmulti _Graph holds ex f be one-to-one Function st ( dom f) = ( the_Edges_of G) & ( rng f) c= [:( the_Vertices_of G), ( the_Vertices_of G):] & for e be object st e in ( dom f) holds (f . e) = [(( the_Source_of G) . e), (( the_Target_of G) . e)]

    proof

      let G be non-Dmulti _Graph;

      deffunc F( object) = [(( the_Source_of G) . $1), (( the_Target_of G) . $1)];

      consider f be Function such that

       A1: ( dom f) = ( the_Edges_of G) and

       A2: for e be object st e in ( the_Edges_of G) holds (f . e) = F(e) from FUNCT_1:sch 3;

      now

        let x1,x2 be object;

        assume

         A3: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

        then (f . x1) = [(( the_Source_of G) . x1), (( the_Target_of G) . x1)] & (f . x2) = [(( the_Source_of G) . x2), (( the_Target_of G) . x2)] by A1, A2;

        then

         A4: (( the_Source_of G) . x1) = (( the_Source_of G) . x2) & (( the_Target_of G) . x1) = (( the_Target_of G) . x2) by A3, XTUPLE_0: 1;

        x1 DJoins ((( the_Source_of G) . x1),(( the_Target_of G) . x1),G) & x2 DJoins ((( the_Source_of G) . x2),(( the_Target_of G) . x2),G) by A1, A3, GLIB_000:def 14;

        hence x1 = x2 by A4, GLIB_000:def 21;

      end;

      then

      reconsider f as one-to-one Function by FUNCT_1:def 4;

      take f;

      thus ( dom f) = ( the_Edges_of G) by A1;

      now

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A5: x in ( dom f) & (f . x) = y by FUNCT_1:def 3;

        

         A6: y = [(( the_Source_of G) . x), (( the_Target_of G) . x)] by A1, A2, A5;

        x Joins ((( the_Source_of G) . x),(( the_Target_of G) . x),G) by A1, A5, GLIB_000:def 13;

        then (( the_Source_of G) . x) is Vertex of G & (( the_Target_of G) . x) is Vertex of G by GLIB_000: 13;

        hence y in [:( the_Vertices_of G), ( the_Vertices_of G):] by A6, ZFMISC_1:def 2;

      end;

      hence ( rng f) c= [:( the_Vertices_of G), ( the_Vertices_of G):] by TARSKI:def 3;

      thus thesis by A1, A2;

    end;

    theorem :: GLIB_013:2

    

     Th2: for G be non-Dmulti _Graph holds (G .size() ) c= ((G .order() ) *` (G .order() ))

    proof

      let G be non-Dmulti _Graph;

      consider f be one-to-one Function such that

       A1: ( dom f) = ( the_Edges_of G) & ( rng f) c= [:( the_Vertices_of G), ( the_Vertices_of G):] and for e be object st e in ( dom f) holds (f . e) = [(( the_Source_of G) . e), (( the_Target_of G) . e)] by Th1;

      (G .size() ) c= ( card [:( the_Vertices_of G), ( the_Vertices_of G):]) by A1, CARD_1: 10;

      then (G .size() ) c= ( card [:(G .order() ), ( card ( the_Vertices_of G)):]) by CARD_2: 7;

      hence thesis by CARD_2:def 2;

    end;

    theorem :: GLIB_013:3

    

     Th3: for G be Dsimple _Graph holds ex f be one-to-one Function st ( dom f) = ( the_Edges_of G) & ( rng f) c= ( [:( the_Vertices_of G), ( the_Vertices_of G):] \ ( id ( the_Vertices_of G))) & for e be object st e in ( dom f) holds (f . e) = [(( the_Source_of G) . e), (( the_Target_of G) . e)]

    proof

      let G be Dsimple _Graph;

      consider f be one-to-one Function such that

       A1: ( dom f) = ( the_Edges_of G) & ( rng f) c= [:( the_Vertices_of G), ( the_Vertices_of G):] and

       A2: for e be object st e in ( dom f) holds (f . e) = [(( the_Source_of G) . e), (( the_Target_of G) . e)] by Th1;

      take f;

      ( rng f) misses ( id ( the_Vertices_of G))

      proof

        assume ( rng f) meets ( id ( the_Vertices_of G));

        then

        consider y be object such that

         A3: y in ( rng f) & y in ( id ( the_Vertices_of G)) by XBOOLE_0: 3;

        consider x be object such that

         A4: x in ( dom f) & (f . x) = y by A3, FUNCT_1:def 3;

        y = [(( the_Source_of G) . x), (( the_Target_of G) . x)] by A2, A4;

        then (( the_Source_of G) . x) = (( the_Target_of G) . x) by A3, RELAT_1:def 10;

        hence contradiction by A1, A4, GLIB_000:def 18;

      end;

      hence thesis by A1, A2, XBOOLE_1: 86;

    end;

    theorem :: GLIB_013:4

    

     Th4: for G be non-multi _Graph holds ex f be one-to-one Function st ( dom f) = ( the_Edges_of G) & ( rng f) c= (( 2Set ( the_Vertices_of G)) \/ ( singletons ( the_Vertices_of G))) & for e be object st e in ( dom f) holds (f . e) = {(( the_Source_of G) . e), (( the_Target_of G) . e)}

    proof

      let G be non-multi _Graph;

      deffunc F( object) = {(( the_Source_of G) . $1), (( the_Target_of G) . $1)};

      consider f be Function such that

       A1: ( dom f) = ( the_Edges_of G) and

       A2: for e be object st e in ( the_Edges_of G) holds (f . e) = F(e) from FUNCT_1:sch 3;

      now

        let x1,x2 be object;

        assume

         A3: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

        then

         A4: (f . x1) = {(( the_Source_of G) . x1), (( the_Target_of G) . x1)} & (f . x2) = {(( the_Source_of G) . x2), (( the_Target_of G) . x2)} by A1, A2;

        

         A5: x1 Joins ((( the_Source_of G) . x1),(( the_Target_of G) . x1),G) & x2 Joins ((( the_Source_of G) . x2),(( the_Target_of G) . x2),G) by A1, A3, GLIB_000:def 13;

        per cases by A3, A4, ZFMISC_1: 22;

          suppose (( the_Source_of G) . x1) = (( the_Source_of G) . x2) & (( the_Target_of G) . x1) = (( the_Target_of G) . x2);

          hence x1 = x2 by A5, GLIB_000:def 20;

        end;

          suppose (( the_Source_of G) . x1) = (( the_Target_of G) . x2) & (( the_Target_of G) . x1) = (( the_Source_of G) . x2);

          then x2 Joins ((( the_Source_of G) . x1),(( the_Target_of G) . x1),G) by A5, GLIB_000: 14;

          hence x1 = x2 by A5, GLIB_000:def 20;

        end;

      end;

      then

      reconsider f as one-to-one Function by FUNCT_1:def 4;

      take f;

      thus ( dom f) = ( the_Edges_of G) by A1;

      for y be object st y in ( rng f) holds y in (( 2Set ( the_Vertices_of G)) \/ ( singletons ( the_Vertices_of G)))

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A6: x in ( dom f) & (f . x) = y by FUNCT_1:def 3;

        reconsider z = y as set by TARSKI: 1;

        

         A7: y = {(( the_Source_of G) . x), (( the_Target_of G) . x)} by A1, A2, A6;

        x Joins ((( the_Source_of G) . x),(( the_Target_of G) . x),G) by A1, A6, GLIB_000:def 13;

        then

         A8: (( the_Source_of G) . x) is Vertex of G & (( the_Target_of G) . x) is Vertex of G by GLIB_000: 13;

        per cases ;

          suppose (( the_Source_of G) . x) = (( the_Target_of G) . x);

          then y = {(( the_Source_of G) . x)} by A7, ENUMSET1: 29;

          then z c= ( the_Vertices_of G) & z is 1 -element by A8, ZFMISC_1: 31;

          then z in ( singletons ( the_Vertices_of G));

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose (( the_Source_of G) . x) <> (( the_Target_of G) . x);

          then z c= ( the_Vertices_of G) & ( card z) = 2 by A7, A8, ZFMISC_1: 32, CARD_2: 57;

          then z in ( TWOELEMENTSETS ( the_Vertices_of G));

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      hence ( rng f) c= (( 2Set ( the_Vertices_of G)) \/ ( singletons ( the_Vertices_of G))) by TARSKI:def 3;

      thus thesis by A1, A2;

    end;

    theorem :: GLIB_013:5

    

     Th5: for G be simple _Graph holds ex f be one-to-one Function st ( dom f) = ( the_Edges_of G) & ( rng f) c= ( 2Set ( the_Vertices_of G)) & for e be object st e in ( dom f) holds (f . e) = {(( the_Source_of G) . e), (( the_Target_of G) . e)}

    proof

      let G be simple _Graph;

      consider f be one-to-one Function such that

       A1: ( dom f) = ( the_Edges_of G) and

       A2: ( rng f) c= (( 2Set ( the_Vertices_of G)) \/ ( singletons ( the_Vertices_of G))) and

       A3: for e be object st e in ( dom f) holds (f . e) = {(( the_Source_of G) . e), (( the_Target_of G) . e)} by Th4;

      take f;

      (( rng f) /\ ( singletons ( the_Vertices_of G))) = {}

      proof

        assume (( rng f) /\ ( singletons ( the_Vertices_of G))) <> {} ;

        then

        consider y be object such that

         A4: y in (( rng f) /\ ( singletons ( the_Vertices_of G))) by XBOOLE_0:def 1;

        

         A5: y in ( rng f) & y in ( singletons ( the_Vertices_of G)) by A4, XBOOLE_0:def 4;

        then

        consider e be object such that

         A6: e in ( dom f) & (f . e) = y by FUNCT_1:def 3;

        consider Y be Subset of ( the_Vertices_of G) such that

         A7: y = Y & Y is 1 -element by A5;

        ( card Y) = 1 by A7, CARD_1:def 7

        .= ( card { the object}) by CARD_1: 30;

        then

        consider v be object such that

         A8: Y = {v} by CARD_1: 29;

        y = {(( the_Source_of G) . e), (( the_Target_of G) . e)} by A3, A6;

        hence contradiction by A1, A6, A7, A8, ZFMISC_1: 5, GLIB_000:def 18;

      end;

      hence thesis by A1, A2, A3, XBOOLE_1: 73, XBOOLE_0:def 7;

    end;

    begin

    definition

      let G be _Graph;

      :: GLIB_013:def1

      attr G is vertex-finite means

      : Def1: ( the_Vertices_of G) is finite;

      :: GLIB_013:def2

      attr G is edge-finite means

      : Def2: ( the_Edges_of G) is finite;

    end

    theorem :: GLIB_013:6

    

     Th6: for G be _Graph holds G is vertex-finite iff (G .order() ) is finite;

    theorem :: GLIB_013:7

    

     Th7: for G be _Graph holds G is edge-finite iff (G .size() ) is finite;

    theorem :: GLIB_013:8

    

     Th8: for G1,G2 be _Graph st G1 == G2 holds (G1 is vertex-finite implies G2 is vertex-finite) & (G1 is edge-finite implies G2 is edge-finite) by GLIB_000:def 34;

    registration

      let V be non empty finite set, E be set;

      let S,T be Function of E, V;

      cluster ( createGraph (V,E,S,T)) -> vertex-finite;

      coherence by GLIB_000: 6;

    end

    registration

      let V be infinite set, E be set;

      let S,T be Function of E, V;

      cluster ( createGraph (V,E,S,T)) -> non vertex-finite;

      coherence by GLIB_000: 6;

    end

    registration

      let V be non empty set, E be finite set;

      let S,T be Function of E, V;

      cluster ( createGraph (V,E,S,T)) -> edge-finite;

      coherence by GLIB_000: 6;

    end

    registration

      let V be non empty set, E be infinite set;

      let S,T be Function of E, V;

      cluster ( createGraph (V,E,S,T)) -> non edge-finite;

      coherence by GLIB_000: 6;

    end

    registration

      cluster _finite -> vertex-finite edge-finite for _Graph;

      coherence ;

      cluster vertex-finite edge-finite -> _finite for _Graph;

      coherence by GLIB_000:def 17;

      cluster edgeless -> edge-finite for _Graph;

      coherence ;

      cluster _trivial -> vertex-finite for _Graph;

      coherence ;

      cluster vertex-finite non-Dmulti -> edge-finite for _Graph;

      coherence

      proof

        let G be _Graph;

        assume

         A1: G is vertex-finite non-Dmulti;

        then

         A2: (G .size() ) c= ((G .order() ) *` (G .order() )) by Th2;

        reconsider X = (G .order() ) as finite set by A1;

        ((G .order() ) *` (G .order() )) = ( card [:(G .order() ), (G .order() ):]) by CARD_2:def 2

        .= (( card X) * ( card X)) by CARD_2: 46;

        hence thesis by A2;

      end;

      cluster non vertex-finite loopfull -> non edge-finite for _Graph;

      coherence

      proof

        let G be _Graph;

        assume

         A3: G is non vertex-finite loopfull;

        (G .loops() ) is infinite

        proof

          assume

           A4: (G .loops() ) is finite;

          set f = (( the_Source_of G) | (G .loops() ));

          now

            let v be object;

            assume v in ( the_Vertices_of G);

            then

            consider e be object such that

             A5: e Joins (v,v,G) by A3, GLIB_012:def 1;

            

             A6: e in (G .loops() ) by A5, GLIB_009:def 2;

            

             A7: v = (( the_Source_of G) . e) by A5, GLIB_000:def 13

            .= (f . e) by A6, FUNCT_1: 49;

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

            then e in ( dom ( the_Source_of G)) by FUNCT_2:def 1;

            then e in ( dom f) by A6, RELAT_1: 57;

            hence v in ( rng f) by A7, FUNCT_1:def 3;

          end;

          then ( the_Vertices_of G) c= ( rng f) by TARSKI:def 3;

          hence contradiction by A3, A4;

        end;

        hence thesis;

      end;

      cluster vertex-finite edge-finite simple for _Graph;

      existence

      proof

        take the _finite simple _Graph;

        thus thesis;

      end;

      cluster vertex-finite non edge-finite for _Graph;

      existence

      proof

        set x = the object;

        set E = the infinite set;

        set f = the Function of E, {x};

        set G = ( createGraph ( {x},E,f,f));

        take G;

        thus thesis;

      end;

      cluster non vertex-finite edge-finite for _Graph;

      existence

      proof

        set V = the infinite set;

        set E = the empty set;

        set f = the Function of E, V;

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

        take G;

        thus thesis;

      end;

      cluster non vertex-finite non edge-finite for _Graph;

      existence

      proof

        set V = the infinite set;

        set f = the Function of V, V;

        set G = ( createGraph (V,V,f,f));

        take G;

        thus thesis;

      end;

    end

    registration

      let G be vertex-finite _Graph;

      cluster (G .order() ) -> non zero natural;

      coherence

      proof

        (G .order() ) is finite by Th6;

        hence thesis;

      end;

    end

    definition

      let G be vertex-finite _Graph;

      :: original: .order()

      redefine

      func G .order() -> non zero Nat ;

      coherence ;

    end

    registration

      let G be edge-finite _Graph;

      cluster (G .size() ) -> natural;

      coherence

      proof

        (G .size() ) is finite by Th7;

        hence thesis;

      end;

    end

    definition

      let G be edge-finite _Graph;

      :: original: .size()

      redefine

      func G .size() -> Nat ;

      coherence ;

    end

    theorem :: GLIB_013:9

    for G be vertex-finite non-Dmulti _Graph holds (G .size() ) <= ((G .order() ) ^2 )

    proof

      let G be vertex-finite non-Dmulti _Graph;

      ((G .order() ) *` (G .order() )) = ( card [:(G .order() ), (G .order() ):]) by CARD_2:def 2

      .= (( card (G .order() )) * (G .order() )) by CARD_2: 46

      .= ( Segm ((G .order() ) * (G .order() )));

      then ( Segm (G .size() )) c= ( Segm ((G .order() ) * (G .order() ))) by Th2;

      then (G .size() ) <= ((G .order() ) * (G .order() )) by NAT_1: 39;

      hence thesis by SQUARE_1:def 1;

    end;

    theorem :: GLIB_013:10

    for G be vertex-finite Dsimple _Graph holds (G .size() ) <= (((G .order() ) ^2 ) - (G .order() ))

    proof

      let G be vertex-finite Dsimple _Graph;

      set P = [:( the_Vertices_of G), ( the_Vertices_of G):];

      set I = ( id ( the_Vertices_of G));

      consider f be one-to-one Function such that

       A1: ( dom f) = ( the_Edges_of G) & ( rng f) c= (P \ I) and for e be object st e in ( dom f) holds (f . e) = [(( the_Source_of G) . e), (( the_Target_of G) . e)] by Th3;

      

       A2: ((G .order() ) - 1) is Nat by CHORD: 1;

      (((G .order() ) ^2 ) - (G .order() )) = (((G .order() ) * (G .order() )) - (G .order() )) by SQUARE_1:def 1

      .= ((G .order() ) * ((G .order() ) - 1));

      then

       A3: (((G .order() ) ^2 ) - (G .order() )) is Nat by A2;

      ( card (P \ I)) = (( card P) - ( card I)) by CARD_2: 44

      .= (((G .order() ) * ( card ( the_Vertices_of G))) - ( card I)) by CARD_2: 46

      .= (((G .order() ) ^2 ) - ( card I)) by SQUARE_1:def 1

      .= (((G .order() ) ^2 ) - ( card ( dom ( id ( the_Vertices_of G))))) by CARD_1: 62

      .= (((G .order() ) ^2 ) - (G .order() ));

      then ( Segm (G .size() )) c= ( Segm (((G .order() ) ^2 ) - (G .order() ))) by A1, CARD_1: 10;

      hence (G .size() ) <= (((G .order() ) ^2 ) - (G .order() )) by A3, NAT_1: 39;

    end;

    theorem :: GLIB_013:11

    for G be vertex-finite non-multi _Graph holds (G .size() ) <= ((((G .order() ) ^2 ) + (G .order() )) / 2)

    proof

      let G be vertex-finite non-multi _Graph;

      set V1 = ( singletons ( the_Vertices_of G)), V2 = ( 2Set ( the_Vertices_of G));

      consider f be one-to-one Function such that

       A1: ( dom f) = ( the_Edges_of G) & ( rng f) c= (V2 \/ V1) and for e be object st e in ( dom f) holds (f . e) = {(( the_Source_of G) . e), (( the_Target_of G) . e)} by Th4;

      reconsider n = ((G .order() ) - 1) as Nat by CHORD: 1;

      

       A2: ( card (V2 \/ V1)) = (( card V2) +` ( card V1)) by CARD_2: 35, GLIBPRE0: 18

      .= (( card V2) +` ( card ( the_Vertices_of G))) by BSPACE: 41

      .= (((n + 1) choose 2) + (n + 1)) by GLIBPRE0: 20;

      

       A3: (((n + 1) choose 2) + (n + 1)) = (((n * (n + 1)) / 2) + ((2 * (n + 1)) / 2)) by NUMPOLY1: 72

      .= ((((G .order() ) * (G .order() )) + (G .order() )) / 2)

      .= ((((G .order() ) ^2 ) + (G .order() )) / 2) by SQUARE_1:def 1;

      ( card ( rng f)) c= (((n + 1) choose 2) + (n + 1)) by A1, A2, CARD_1: 11;

      then ( Segm (G .size() )) c= ( Segm (((n + 1) choose 2) + (n + 1))) by A1, CARD_1: 70;

      hence thesis by A3, NAT_1: 39;

    end;

    theorem :: GLIB_013:12

    for G be vertex-finite simple _Graph holds (G .size() ) <= ((((G .order() ) ^2 ) - (G .order() )) / 2)

    proof

      let G be vertex-finite simple _Graph;

      consider f be one-to-one Function such that

       A1: ( dom f) = ( the_Edges_of G) & ( rng f) c= ( 2Set ( the_Vertices_of G)) and for e be object st e in ( dom f) holds (f . e) = {(( the_Source_of G) . e), (( the_Target_of G) . e)} by Th5;

      reconsider n = ((G .order() ) - 1) as Nat by CHORD: 1;

      

       A2: ( card ( 2Set ( the_Vertices_of G))) = (( card ( the_Vertices_of G)) choose 2) by GLIBPRE0: 20

      .= ((n * (n + 1)) / 2) by NUMPOLY1: 72

      .= ((((G .order() ) * (G .order() )) - (G .order() )) / 2)

      .= ((((G .order() ) ^2 ) - (G .order() )) / 2) by SQUARE_1:def 1;

      ( card ( rng f)) c= ( card ( 2Set ( the_Vertices_of G))) by A1, CARD_1: 11;

      then ( Segm (G .size() )) c= ( Segm ( card ( 2Set ( the_Vertices_of G)))) by A1, CARD_1: 70;

      hence thesis by A2, NAT_1: 39;

    end;

    registration

      let G be vertex-finite _Graph;

      cluster ( the_Vertices_of G) -> finite;

      coherence by Def1;

      cluster -> vertex-finite for Subgraph of G;

      coherence

      proof

        let G2 be Subgraph of G;

        ( the_Vertices_of G2) c= ( the_Vertices_of G);

        hence thesis;

      end;

      cluster -> vertex-finite edge-finite for DLGraphComplement of G;

      coherence

      proof

        let H be DLGraphComplement of G;

        ( the_Vertices_of H) = ( the_Vertices_of G) by GLIB_012:def 6;

        hence H is vertex-finite;

        hence thesis;

      end;

      cluster -> vertex-finite edge-finite for LGraphComplement of G;

      coherence

      proof

        let H be LGraphComplement of G;

        ( the_Vertices_of H) = ( the_Vertices_of G) by GLIB_012:def 7;

        hence H is vertex-finite;

        hence thesis;

      end;

      cluster -> vertex-finite edge-finite for DGraphComplement of G;

      coherence

      proof

        let H be DGraphComplement of G;

        ( the_Vertices_of H) = ( the_Vertices_of G) by GLIB_012: 80;

        hence H is vertex-finite;

        hence thesis;

      end;

      cluster -> vertex-finite edge-finite for GraphComplement of G;

      coherence

      proof

        let H be GraphComplement of G;

        ( the_Vertices_of H) = ( the_Vertices_of G) by GLIB_012: 98;

        hence H is vertex-finite;

        hence thesis;

      end;

      let V be finite set;

      cluster -> vertex-finite for addVertices of G, V;

      coherence

      proof

        let G1 be addVertices of G, V;

        ( the_Vertices_of G1) = (( the_Vertices_of G) \/ V) by GLIB_006:def 10;

        hence thesis;

      end;

    end

    registration

      let G be vertex-finite _Graph, v be object;

      cluster -> vertex-finite for addVertex of G, v;

      coherence ;

      let e,w be object;

      cluster -> vertex-finite for addEdge of G, v, e, w;

      coherence

      proof

        let G1 be addEdge of G, v, e, w;

        per cases ;

          suppose v in ( the_Vertices_of G) & w in ( the_Vertices_of G) & not e in ( the_Edges_of G);

          hence thesis by GLIB_006:def 11;

        end;

          suppose not (v in ( the_Vertices_of G) & w in ( the_Vertices_of G) & not e in ( the_Edges_of G));

          then G == G1 by GLIB_006:def 11;

          hence thesis by Th8;

        end;

      end;

      cluster -> vertex-finite for addAdjVertex of G, v, e, w;

      coherence

      proof

        let G1 be addAdjVertex of G, v, e, w;

        per cases ;

          suppose v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & not w in ( the_Vertices_of G);

          then ( the_Vertices_of G1) = (( the_Vertices_of G) \/ {w}) by GLIB_006:def 12;

          hence thesis;

        end;

          suppose not v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & w in ( the_Vertices_of G);

          then ( the_Vertices_of G1) = (( the_Vertices_of G) \/ {v}) by GLIB_006:def 12;

          hence thesis;

        end;

          suppose not (v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & not w in ( the_Vertices_of G)) & not ( not v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & w in ( the_Vertices_of G));

          then G == G1 by GLIB_006:def 12;

          hence thesis by Th8;

        end;

      end;

    end

    registration

      let G be vertex-finite _Graph, E be set;

      cluster -> vertex-finite for reverseEdgeDirections of G, E;

      coherence

      proof

        let G2 be reverseEdgeDirections of G, E;

        ( the_Vertices_of G) = ( the_Vertices_of G2) by GLIB_007: 4;

        hence thesis;

      end;

    end

    registration

      let G be vertex-finite _Graph, v be object, V be set;

      cluster -> vertex-finite for addAdjVertexAll of G, v, V;

      coherence

      proof

        let G1 be addAdjVertexAll of G, v, V;

        per cases ;

          suppose V c= ( the_Vertices_of G) & not v in ( the_Vertices_of G);

          then ( the_Vertices_of G1) = (( the_Vertices_of G) \/ {v}) by GLIB_007:def 4;

          hence thesis;

        end;

          suppose not (V c= ( the_Vertices_of G) & not v in ( the_Vertices_of G));

          then G == G1 by GLIB_007:def 4;

          hence thesis by Th8;

        end;

      end;

    end

    registration

      let G be vertex-finite _Graph, V be set;

      cluster -> vertex-finite for addLoops of G, V;

      coherence

      proof

        let G1 be addLoops of G, V;

        ( the_Vertices_of G1) = ( the_Vertices_of G) by GLIB_012: 15;

        hence thesis;

      end;

    end

    registration

      let G be _Graph;

      let V be infinite set;

      cluster -> non vertex-finite for addVertices of G, V;

      coherence

      proof

        let G1 be addVertices of G, V;

        ( the_Vertices_of G1) = (( the_Vertices_of G) \/ V) by GLIB_006:def 10;

        hence thesis;

      end;

    end

    registration

      let G be non vertex-finite _Graph;

      cluster ( the_Vertices_of G) -> infinite;

      coherence by Def1;

      cluster -> non vertex-finite for Supergraph of G;

      coherence

      proof

        let G1 be Supergraph of G;

        G is Subgraph of G1 by GLIB_006: 57;

        hence thesis;

      end;

      cluster spanning -> non vertex-finite for Subgraph of G;

      coherence

      proof

        let G2 be Subgraph of G;

        assume G2 is spanning;

        then ( the_Vertices_of G2) = ( the_Vertices_of G) by GLIB_000:def 33;

        hence thesis;

      end;

      cluster -> non vertex-finite for DLGraphComplement of G;

      coherence

      proof

        let H be DLGraphComplement of G;

        ( the_Vertices_of H) = ( the_Vertices_of G) by GLIB_012:def 6;

        hence thesis;

      end;

      cluster -> non vertex-finite for LGraphComplement of G;

      coherence

      proof

        let H be LGraphComplement of G;

        ( the_Vertices_of H) = ( the_Vertices_of G) by GLIB_012:def 7;

        hence thesis;

      end;

      cluster -> non vertex-finite for DGraphComplement of G;

      coherence

      proof

        let H be DGraphComplement of G;

        ( the_Vertices_of H) = ( the_Vertices_of G) by GLIB_012: 80;

        hence thesis;

      end;

      cluster -> non vertex-finite for GraphComplement of G;

      coherence

      proof

        let H be GraphComplement of G;

        ( the_Vertices_of H) = ( the_Vertices_of G) by GLIB_012: 98;

        hence thesis;

      end;

      let V be infinite set, E be set;

      cluster -> non vertex-finite for inducedSubgraph of G, V, E;

      coherence

      proof

        let G2 be inducedSubgraph of G, V, E;

        per cases ;

          suppose V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V);

          hence thesis by GLIB_000:def 37;

        end;

          suppose not (V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V));

          then G == G2 by GLIB_000:def 37;

          hence thesis by Th8;

        end;

      end;

    end

    registration

      let G be non vertex-finite _Graph, V be infinite Subset of ( the_Vertices_of G);

      cluster -> non edge-finite for addLoops of G, V;

      coherence

      proof

        let G1 be addLoops of G, V;

        consider E be set, f be one-to-one Function such that

         A1: E misses ( the_Edges_of G) & ( the_Edges_of G1) = (( the_Edges_of G) \/ E) and

         A2: ( dom f) = E & ( rng f) = V and ( the_Source_of G1) = (( the_Source_of G) +* f) & ( the_Target_of G1) = (( the_Target_of G) +* f) by GLIB_012:def 5;

        E is infinite by A2, FINSET_1: 8;

        hence thesis by A1;

      end;

    end

    registration

      let G be edge-finite _Graph;

      cluster ( the_Edges_of G) -> finite;

      coherence by Def2;

      cluster -> edge-finite for Subgraph of G;

      coherence

      proof

        let G2 be Subgraph of G;

        ( the_Edges_of G2) c= ( the_Edges_of G);

        hence thesis;

      end;

      let V be set;

      cluster -> edge-finite for addVertices of G, V;

      coherence

      proof

        let G1 be addVertices of G, V;

        ( the_Edges_of G1) = ( the_Edges_of G) by GLIB_006:def 10;

        hence thesis;

      end;

    end

    registration

      let G be edge-finite _Graph, E be set;

      cluster -> edge-finite for reverseEdgeDirections of G, E;

      coherence

      proof

        let G2 be reverseEdgeDirections of G, E;

        ( the_Edges_of G2) = ( the_Edges_of G) by GLIB_007: 4;

        hence thesis;

      end;

    end

    registration

      let G be edge-finite _Graph, v be object;

      cluster -> edge-finite for addVertex of G, v;

      coherence ;

      let e,w be object;

      cluster -> edge-finite for addEdge of G, v, e, w;

      coherence

      proof

        let G1 be addEdge of G, v, e, w;

        per cases ;

          suppose v in ( the_Vertices_of G) & w in ( the_Vertices_of G) & not e in ( the_Edges_of G);

          then ( the_Edges_of G1) = (( the_Edges_of G) \/ {e}) by GLIB_006:def 11;

          hence thesis;

        end;

          suppose not (v in ( the_Vertices_of G) & w in ( the_Vertices_of G) & not e in ( the_Edges_of G));

          then G == G1 by GLIB_006:def 11;

          hence thesis by Th8;

        end;

      end;

      cluster -> edge-finite for addAdjVertex of G, v, e, w;

      coherence

      proof

        let G1 be addAdjVertex of G, v, e, w;

        per cases ;

          suppose v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & not w in ( the_Vertices_of G);

          then ( the_Edges_of G1) = (( the_Edges_of G) \/ {e}) by GLIB_006:def 12;

          hence thesis;

        end;

          suppose not v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & w in ( the_Vertices_of G);

          then ( the_Edges_of G1) = (( the_Edges_of G) \/ {e}) by GLIB_006:def 12;

          hence thesis;

        end;

          suppose not (v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & not w in ( the_Vertices_of G)) & not ( not v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & w in ( the_Vertices_of G));

          then G == G1 by GLIB_006:def 12;

          hence thesis by Th8;

        end;

      end;

    end

    registration

      let G be edge-finite _Graph, v be object, V be finite set;

      cluster -> edge-finite for addAdjVertexAll of G, v, V;

      coherence

      proof

        let G1 be addAdjVertexAll of G, v, V;

        per cases ;

          suppose V c= ( the_Vertices_of G) & not v in ( the_Vertices_of G);

          then

          consider E be set such that

           A1: ( card V) = ( card E) & E misses ( the_Edges_of G) and

           A2: ( the_Edges_of G1) = (( the_Edges_of G) \/ E) and for v1 be object st v1 in V holds ex e1 be object st e1 in E & e1 Joins (v1,v,G1) & for e2 be object st e2 Joins (v1,v,G1) holds e1 = e2 by GLIB_007:def 4;

          E is finite by A1;

          hence thesis by A2;

        end;

          suppose not (V c= ( the_Vertices_of G) & not v in ( the_Vertices_of G));

          then G1 == G by GLIB_007:def 4;

          hence thesis by Th8;

        end;

      end;

    end

    registration

      let G be edge-finite _Graph, V be finite Subset of ( the_Vertices_of G);

      cluster -> edge-finite for addLoops of G, V;

      coherence

      proof

        let G1 be addLoops of G, V;

        consider E be set, f be one-to-one Function such that

         A1: E misses ( the_Edges_of G) & ( the_Edges_of G1) = (( the_Edges_of G) \/ E) and

         A2: ( dom f) = E & ( rng f) = V and ( the_Source_of G1) = (( the_Source_of G) +* f) & ( the_Target_of G1) = (( the_Target_of G) +* f) by GLIB_012:def 5;

        ( card E) = ( card V) by A2, CARD_1: 70;

        then E is finite;

        hence thesis by A1;

      end;

    end

    registration

      let G be non vertex-finite edge-finite _Graph;

      cluster isolated for Vertex of G;

      existence

      proof

        set R = (( rng ( the_Source_of G)) \/ ( rng ( the_Target_of G)));

        set v = the Element of (( the_Vertices_of G) \ R);

        reconsider v as Vertex of G;

        take v;

         not v in R by XBOOLE_0:def 5;

        hence v is isolated by GLIBPRE0: 23;

      end;

    end

    registration

      let G be non vertex-finite edge-finite _Graph;

      cluster -> non edge-finite for DLGraphComplement of G;

      coherence

      proof

        let H be DLGraphComplement of G;

        set v = the isolated Vertex of G;

        reconsider w = v as Vertex of H by GLIB_012:def 6;

        ( the_Vertices_of H) = (w .inNeighbors() ) by GLIB_012: 61

        .= (( the_Source_of H) .: (w .edgesIn() ));

        hence thesis;

      end;

      cluster -> non edge-finite for LGraphComplement of G;

      coherence

      proof

        let H be LGraphComplement of G;

        set v = the isolated Vertex of G;

        reconsider w = v as Vertex of H by GLIB_012:def 7;

        ( the_Vertices_of H) = (w .allNeighbors() ) by GLIB_012: 78

        .= ((w .inNeighbors() ) \/ (w .outNeighbors() ));

        hence thesis;

      end;

      cluster -> non edge-finite for DGraphComplement of G;

      coherence

      proof

        let H be DGraphComplement of G;

        set v = the isolated Vertex of G;

        reconsider w = v as Vertex of H by GLIB_012: 80;

        (( the_Vertices_of H) \ {w}) = (w .inNeighbors() ) by GLIB_012: 96

        .= (( the_Source_of H) .: (w .edgesIn() ));

        hence thesis;

      end;

      cluster -> non edge-finite for GraphComplement of G;

      coherence

      proof

        let H be GraphComplement of G;

        set v = the isolated Vertex of G;

        reconsider w = v as Vertex of H by GLIB_012: 98;

        (( the_Vertices_of H) \ {w}) = (w .allNeighbors() ) by GLIB_012: 119

        .= ((w .inNeighbors() ) \/ (w .outNeighbors() ));

        hence thesis;

      end;

    end

    registration

      let G be non edge-finite _Graph;

      cluster ( the_Edges_of G) -> infinite;

      coherence by Def2;

      cluster -> non edge-finite for Supergraph of G;

      coherence

      proof

        let G1 be Supergraph of G;

        G is Subgraph of G1 by GLIB_006: 57;

        hence thesis;

      end;

      let V be set, E be infinite Subset of ( the_Edges_of G);

      cluster -> non edge-finite for inducedSubgraph of G, V, E;

      coherence

      proof

        let G2 be inducedSubgraph of G, V, E;

        per cases ;

          suppose V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V);

          hence thesis by GLIB_000:def 37;

        end;

          suppose not (V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V));

          then G == G2 by GLIB_000:def 37;

          hence thesis by Th8;

        end;

      end;

    end

    registration

      let G be non edge-finite _Graph, E be finite set;

      cluster -> non edge-finite for removeEdges of G, E;

      coherence ;

    end

    registration

      let G be non edge-finite _Graph, e be set;

      cluster -> non edge-finite for removeEdge of G, e;

      coherence ;

    end

    theorem :: GLIB_013:13

    

     Th13: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is weak_SG-embedding holds (G2 is vertex-finite implies G1 is vertex-finite) & (G2 is edge-finite implies G1 is edge-finite)

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is weak_SG-embedding;

      hereby

        assume

         A2: G2 is vertex-finite;

        ( dom (F _V )) = ( the_Vertices_of G1) & (F _V ) is one-to-one by A1, GLIB_010:def 11;

        then (( the_Vertices_of G1),((F _V ) .: ( the_Vertices_of G1))) are_equipotent by CARD_1: 33;

        hence G1 is vertex-finite by A2, CARD_1: 38;

      end;

      assume

       A3: G2 is edge-finite;

      ( dom (F _E )) = ( the_Edges_of G1) & (F _E ) is one-to-one by A1, GLIB_010:def 11;

      then (( the_Edges_of G1),((F _E ) .: ( the_Edges_of G1))) are_equipotent by CARD_1: 33;

      hence G1 is edge-finite by A3, CARD_1: 38;

    end;

    theorem :: GLIB_013:14

    

     Th14: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is onto holds (G1 is vertex-finite implies G2 is vertex-finite) & (G1 is edge-finite implies G2 is edge-finite)

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is onto;

      hereby

        assume

         A2: G1 is vertex-finite;

        ( dom (F _V )) is finite by A2;

        then ( rng (F _V )) is finite by FINSET_1: 8;

        hence G2 is vertex-finite by A1, GLIB_010:def 12;

      end;

      assume G1 is edge-finite;

      then ( dom (F _E )) is finite;

      then ( rng (F _E )) is finite by FINSET_1: 8;

      hence G2 is edge-finite by A1, GLIB_010:def 12;

    end;

    theorem :: GLIB_013:15

    for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is isomorphism holds (G1 is vertex-finite iff G2 is vertex-finite) & (G1 is edge-finite iff G2 is edge-finite) by Th13, Th14;

    begin

    definition

      let c be Cardinal, G be _Graph;

      :: GLIB_013:def3

      attr G is c -vertex means

      : Def3: (G .order() ) = c;

      :: GLIB_013:def4

      attr G is c -edge means

      : Def4: (G .size() ) = c;

    end

    theorem :: GLIB_013:16

    for G be _Graph holds G is vertex-finite iff ex n be non zero Nat st G is n -vertex

    proof

      let G be _Graph;

      hereby

        assume G is vertex-finite;

        then

        reconsider n = ( card ( the_Vertices_of G)) as Nat;

        reconsider n as non zero Nat;

        take n;

        thus G is n -vertex;

      end;

      thus thesis;

    end;

    theorem :: GLIB_013:17

    for G be _Graph holds G is edge-finite iff ex n be Nat st G is n -edge

    proof

      let G be _Graph;

      hereby

        assume G is edge-finite;

        then

        reconsider n = ( card ( the_Edges_of G)) as Nat;

        take n;

        thus G is n -edge;

      end;

      thus thesis;

    end;

    theorem :: GLIB_013:18

    

     Th18: for G1,G2 be _Graph, c be Cardinal st ( the_Vertices_of G1) = ( the_Vertices_of G2) holds G1 is c -vertex implies G2 is c -vertex;

    theorem :: GLIB_013:19

    

     Th19: for G1,G2 be _Graph, c be Cardinal st ( the_Edges_of G1) = ( the_Edges_of G2) holds G1 is c -edge implies G2 is c -edge;

    theorem :: GLIB_013:20

    

     Th20: for G1,G2 be _Graph, c be Cardinal st G1 == G2 holds (G1 is c -vertex implies G2 is c -vertex) & (G1 is c -edge implies G2 is c -edge) by GLIB_000:def 34;

    theorem :: GLIB_013:21

    for G be _Graph holds G is (G .order() ) -vertex(G .size() ) -edge;

    registration

      let V be non empty set, E be set;

      let S,T be Function of E, V;

      cluster ( createGraph (V,E,S,T)) -> ( card V) -vertex( card E) -edge;

      coherence by GLIB_000: 6;

    end

    registration

      let a be non zero Cardinal, b be Cardinal;

      cluster a -vertexb -edge for _Graph;

      existence

      proof

        set V = the a -element set;

        set E = the b -element set;

        set v = the Element of V;

        set f = (E --> v);

        reconsider f as Function of E, V;

        take G = ( createGraph (V,E,f,f));

        ( card V) = a & ( card E) = b by CARD_1:def 7;

        hence thesis;

      end;

    end

    registration

      let c be Cardinal;

      cluster _trivialc -edge for _Graph;

      existence

      proof

        take G = the 1 -vertexc -edge _Graph;

        (G .order() ) = 1 by Def3;

        hence thesis by GLIB_000:def 19;

      end;

    end

    registration

      cluster -> non 0 -vertex for _Graph;

      coherence ;

      cluster _trivial -> 1 -vertex for _Graph;

      coherence by GLIB_000:def 19;

      cluster 1 -vertex -> _trivial for _Graph;

      coherence by GLIB_000:def 19;

      let n be non zero Nat;

      cluster n -vertex -> vertex-finite for _Graph;

      coherence ;

    end

    registration

      let c be non zero Cardinal, G be c -vertex _Graph;

      cluster spanning -> c -vertex for Subgraph of G;

      coherence

      proof

        let G2 be Subgraph of G;

        assume G2 is spanning;

        then ( the_Vertices_of G) = ( the_Vertices_of G2) by GLIB_000:def 33;

        hence thesis by Th18;

      end;

      cluster -> c -vertex for DLGraphComplement of G;

      coherence

      proof

        let H be DLGraphComplement of G;

        ( the_Vertices_of G) = ( the_Vertices_of H) by GLIB_012:def 6;

        hence thesis by Th18;

      end;

      cluster -> c -vertex for LGraphComplement of G;

      coherence

      proof

        let H be LGraphComplement of G;

        ( the_Vertices_of G) = ( the_Vertices_of H) by GLIB_012:def 7;

        hence thesis by Th18;

      end;

      cluster -> c -vertex for DGraphComplement of G;

      coherence

      proof

        let H be DGraphComplement of G;

        ( the_Vertices_of G) = ( the_Vertices_of H) by GLIB_012: 80;

        hence thesis by Th18;

      end;

      cluster -> c -vertex for GraphComplement of G;

      coherence

      proof

        let H be GraphComplement of G;

        ( the_Vertices_of G) = ( the_Vertices_of H) by GLIB_012: 98;

        hence thesis by Th18;

      end;

      let E be set;

      cluster -> c -vertex for reverseEdgeDirections of G, E;

      coherence

      proof

        let G2 be reverseEdgeDirections of G, E;

        ( the_Vertices_of G) = ( the_Vertices_of G2) by GLIB_007: 4;

        hence thesis by Th18;

      end;

    end

    registration

      let c be non zero Cardinal, G be c -vertex _Graph, V be set;

      cluster -> c -vertex for addLoops of G, V;

      coherence

      proof

        let G1 be addLoops of G, V;

        ( the_Vertices_of G) = ( the_Vertices_of G1) by GLIB_012: 15;

        hence thesis by Th18;

      end;

    end

    registration

      let c be non zero Cardinal, G be c -vertex _Graph, v,e,w be object;

      cluster -> c -vertex for addEdge of G, v, e, w;

      coherence

      proof

        let G1 be addEdge of G, v, e, w;

        per cases ;

          suppose v is Vertex of G & w is Vertex of G;

          then ( the_Vertices_of G) = ( the_Vertices_of G1) by GLIB_006: 102;

          hence thesis by Th18;

        end;

          suppose not (v is Vertex of G & w is Vertex of G);

          then G1 == G by GLIB_006:def 11;

          hence thesis by Th20;

        end;

      end;

    end

    registration

      cluster edgeless -> 0 -edge for _Graph;

      coherence ;

      cluster 0 -edge -> edgeless for _Graph;

      coherence ;

      let n be Nat;

      cluster n -edge -> edge-finite for _Graph;

      coherence ;

    end

    registration

      let c be Cardinal, G be c -edge _Graph, E be set;

      cluster -> c -edge for reverseEdgeDirections of G, E;

      coherence

      proof

        let G2 be reverseEdgeDirections of G, E;

        ( the_Edges_of G) = ( the_Edges_of G2) by GLIB_007: 4;

        hence thesis by Th19;

      end;

    end

    registration

      let c be Cardinal, G be c -edge _Graph, V be set;

      cluster -> c -edge for addVertices of G, V;

      coherence

      proof

        let G1 be addVertices of G, V;

        ( the_Edges_of G) = ( the_Edges_of G1) by GLIB_006:def 10;

        hence thesis by Th19;

      end;

    end

    theorem :: GLIB_013:22

    for G1,G2 be _Graph, F be PGraphMapping of G1, G2, c be Cardinal st F is isomorphism holds (G1 is c -vertex iff G2 is c -vertex) & (G1 is c -edge iff G2 is c -edge) by GLIB_010: 84;

    begin

    definition

      let G be _Graph;

      :: GLIB_013:def5

      attr G is locally-finite means

      : Def5: for v be Vertex of G holds (v .edgesInOut() ) is finite;

    end

    theorem :: GLIB_013:23

    

     Th23: for G be _Graph holds G is locally-finite iff for v be Vertex of G holds (v .degree() ) is finite

    proof

      let G be _Graph;

      hereby

        assume

         A1: G is locally-finite;

        let v be Vertex of G;

        (v .edgesInOut() ) is finite by A1;

        then (v .edgesIn() ) is finite & (v .edgesOut() ) is finite;

        hence (v .degree() ) is finite;

      end;

      assume

       A2: for v be Vertex of G holds (v .degree() ) is finite;

      let v be Vertex of G;

      (v .degree() ) is finite by A2;

      then (v .edgesIn() ) is finite & (v .edgesOut() ) is finite;

      hence thesis;

    end;

    theorem :: GLIB_013:24

    

     Th24: for G1,G2 be _Graph st G1 == G2 holds G1 is locally-finite implies G2 is locally-finite

    proof

      let G1,G2 be _Graph;

      assume

       A1: G1 == G2 & G1 is locally-finite;

      let v be Vertex of G2;

      reconsider w = v as Vertex of G1 by A1, GLIB_000:def 34;

      (v .edgesInOut() ) = (w .edgesInOut() ) by A1, GLIB_000: 96;

      hence thesis by A1;

    end;

    theorem :: GLIB_013:25

    

     Th25: for G be _Graph holds G is locally-finite iff for v be Vertex of G holds (v .edgesIn() ) is finite & (v .edgesOut() ) is finite

    proof

      let G be _Graph;

      hereby

        assume

         A1: G is locally-finite;

        let v be Vertex of G;

        (v .edgesInOut() ) is finite by A1;

        hence (v .edgesIn() ) is finite & (v .edgesOut() ) is finite;

      end;

      assume

       A2: for v be Vertex of G holds (v .edgesIn() ) is finite & (v .edgesOut() ) is finite;

      let v be Vertex of G;

      (v .edgesIn() ) is finite & (v .edgesOut() ) is finite by A2;

      hence (v .edgesInOut() ) is finite;

    end;

    theorem :: GLIB_013:26

    for G be _Graph holds G is locally-finite iff for v be Vertex of G holds (v .inDegree() ) is finite & (v .outDegree() ) is finite

    proof

      let G be _Graph;

      hereby

        assume

         A1: G is locally-finite;

        let v be Vertex of G;

        (v .degree() ) is finite by A1, Th23;

        hence (v .inDegree() ) is finite & (v .outDegree() ) is finite;

      end;

      assume

       A2: for v be Vertex of G holds (v .inDegree() ) is finite & (v .outDegree() ) is finite;

      now

        let v be Vertex of G;

        (v .inDegree() ) is finite & (v .outDegree() ) is finite by A2;

        hence (v .degree() ) is finite;

      end;

      hence thesis by Th23;

    end;

    theorem :: GLIB_013:27

    for V be non empty set, E be set, S,T be Function of E, V st for v be Element of V holds (S " {v}) is finite & (T " {v}) is finite holds ( createGraph (V,E,S,T)) is locally-finite

    proof

      let V be non empty set, E be set, S,T be Function of E, V;

      assume

       A1: for v be Element of V holds (S " {v}) is finite & (T " {v}) is finite;

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

      now

        let v be Vertex of G;

        ( the_Vertices_of G) = V by GLIB_000: 6;

        then (S " {v}) is finite & (T " {v}) is finite by A1;

        then (( the_Source_of G) " {v}) is finite & (( the_Target_of G) " {v}) is finite by GLIB_000: 6;

        hence (v .edgesIn() ) is finite & (v .edgesOut() ) is finite by GLIBPRE0: 25;

      end;

      hence thesis by Th25;

    end;

    theorem :: GLIB_013:28

    for V be non empty set, E be set, S,T be Function of E, V st ex v be Element of V st (S " {v}) is infinite or (T " {v}) is infinite holds ( createGraph (V,E,S,T)) is non locally-finite

    proof

      let V be non empty set, E be set, S,T be Function of E, V;

      given v be Element of V such that

       A1: (S " {v}) is infinite or (T " {v}) is infinite;

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

      reconsider v as Vertex of G by GLIB_000: 6;

      per cases by A1;

        suppose (S " {v}) is infinite;

        then (( the_Source_of G) " {v}) is infinite by GLIB_000: 6;

        then (v .edgesOut() ) is infinite by GLIBPRE0: 25;

        hence thesis by Th25;

      end;

        suppose (T " {v}) is infinite;

        then (( the_Target_of G) " {v}) is infinite by GLIB_000: 6;

        then (v .edgesIn() ) is infinite by GLIBPRE0: 25;

        hence thesis by Th25;

      end;

    end;

    registration

      let G be non vertex-finite _Graph;

      let V be infinite Subset of ( the_Vertices_of G);

      cluster -> non locally-finite for addAdjVertexAll of G, ( the_Vertices_of G), V;

      coherence

      proof

        let G1 be addAdjVertexAll of G, ( the_Vertices_of G), V;

        

         A1: not ( the_Vertices_of G) in ( the_Vertices_of G);

        then

        reconsider v = ( the_Vertices_of G) as Vertex of G1 by GLIB_007: 50;

        (v .degree() ) = ( card V) by A1, GLIBPRE0: 57;

        hence thesis by Th23;

      end;

    end

    registration

      cluster edge-finite -> locally-finite for _Graph;

      coherence ;

      cluster locally-finite for _Graph;

      existence

      proof

        take the edge-finite _Graph;

        thus thesis;

      end;

      cluster non locally-finite for _Graph;

      existence

      proof

        set G0 = the non vertex-finite _Graph;

        take G = the addAdjVertexAll of G0, ( the_Vertices_of G0), ( the_Vertices_of G0);

        ( the_Vertices_of G0) is infinite & ( the_Vertices_of G0) c= ( the_Vertices_of G0);

        hence thesis;

      end;

    end

    registration

      let G be locally-finite _Graph;

      cluster -> locally-finite for Subgraph of G;

      coherence

      proof

        let G2 be Subgraph of G;

        let v2 be Vertex of G2;

        ( the_Vertices_of G2) c= ( the_Vertices_of G);

        then

        reconsider v1 = v2 as Vertex of G by TARSKI:def 3;

        

         A1: (v2 .edgesInOut() ) c= (v1 .edgesInOut() ) by GLIB_000: 78;

        (v1 .edgesInOut() ) is finite by Def5;

        hence thesis by A1;

      end;

      let X be finite set;

      cluster (G .edgesInto X) -> finite;

      coherence

      proof

        set S = { (v .edgesIn() ) where v be Vertex of G : v in X };

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

        

         A2: for x,y1,y2 be object st x in (X /\ ( the_Vertices_of G)) & P[x, y1] & P[x, y2] holds y1 = y2;

        

         A3: for x be object st x in (X /\ ( the_Vertices_of G)) holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in (X /\ ( the_Vertices_of G));

          then

          reconsider v = x as Vertex of G by XBOOLE_0:def 4;

          take (v .edgesIn() ), v;

          thus thesis;

        end;

        consider f be Function such that

         A4: ( dom f) = (X /\ ( the_Vertices_of G)) and

         A5: for x be object st x in (X /\ ( the_Vertices_of G)) holds P[x, (f . x)] from FUNCT_1:sch 2( A2, A3);

        

         A6: ( rng f) is finite by A4, FINSET_1: 8;

        now

          let E be object;

          assume E in S;

          then

          consider v be Vertex of G such that

           A7: E = (v .edgesIn() ) & v in X;

          

           A8: v in (X /\ ( the_Vertices_of G)) by A7, XBOOLE_0:def 4;

          then

          consider v0 be Vertex of G such that

           A9: v = v0 & (f . v) = (v0 .edgesIn() ) by A5;

          thus E in ( rng f) by A4, A7, A8, A9, FUNCT_1: 3;

        end;

        then S c= ( rng f) by TARSKI:def 3;

        then

         A10: S is finite by A6;

        for E be set st E in S holds E is finite

        proof

          let E be set;

          assume E in S;

          then

          consider v be Vertex of G such that

           A11: E = (v .edgesIn() ) & v in X;

          thus E is finite by A11, Th25;

        end;

        then ( union S) is finite by A10, FINSET_1: 7;

        hence thesis by GLIBPRE0: 36;

      end;

      cluster (G .edgesOutOf X) -> finite;

      coherence

      proof

        set S = { (v .edgesOut() ) where v be Vertex of G : v in X };

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

        

         A12: for x,y1,y2 be object st x in (X /\ ( the_Vertices_of G)) & P[x, y1] & P[x, y2] holds y1 = y2;

        

         A13: for x be object st x in (X /\ ( the_Vertices_of G)) holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in (X /\ ( the_Vertices_of G));

          then

          reconsider v = x as Vertex of G by XBOOLE_0:def 4;

          take (v .edgesOut() ), v;

          thus thesis;

        end;

        consider f be Function such that

         A14: ( dom f) = (X /\ ( the_Vertices_of G)) and

         A15: for x be object st x in (X /\ ( the_Vertices_of G)) holds P[x, (f . x)] from FUNCT_1:sch 2( A12, A13);

        

         A16: ( rng f) is finite by A14, FINSET_1: 8;

        now

          let E be object;

          assume E in S;

          then

          consider v be Vertex of G such that

           A17: E = (v .edgesOut() ) & v in X;

          

           A18: v in (X /\ ( the_Vertices_of G)) by A17, XBOOLE_0:def 4;

          then

          consider v0 be Vertex of G such that

           A19: v = v0 & (f . v) = (v0 .edgesOut() ) by A15;

          thus E in ( rng f) by A14, A17, A18, A19, FUNCT_1: 3;

        end;

        then S c= ( rng f) by TARSKI:def 3;

        then

         A20: S is finite by A16;

        for E be set st E in S holds E is finite

        proof

          let E be set;

          assume E in S;

          then

          consider v be Vertex of G such that

           A21: E = (v .edgesOut() ) & v in X;

          thus E is finite by A21, Th25;

        end;

        then ( union S) is finite by A20, FINSET_1: 7;

        hence thesis by GLIBPRE0: 37;

      end;

      cluster (G .edgesInOut X) -> finite;

      coherence ;

      cluster (G .edgesBetween X) -> finite;

      coherence ;

      let Y be finite set;

      cluster (G .edgesBetween (X,Y)) -> finite;

      coherence

      proof

        set V = ( the_Vertices_of G);

        set S = { ((v .edgesInOut() ) /\ (w .edgesInOut() )) where v,w be Vertex of G : v in X & w in Y };

        defpred P[ object, object] means ex v,w be Vertex of G st $1 = [v, w] & $2 = ((v .edgesInOut() ) /\ (w .edgesInOut() ));

        

         A22: for x,y1,y2 be object st x in ( [:X, Y:] /\ [:V, V:]) & P[x, y1] & P[x, y2] holds y1 = y2

        proof

          let x,y1,y2 be object;

          assume

           A23: x in ( [:X, Y:] /\ [:V, V:]) & P[x, y1] & P[x, y2];

          then

          consider v1,w1 be Vertex of G such that

           A24: x = [v1, w1] & y1 = ((v1 .edgesInOut() ) /\ (w1 .edgesInOut() ));

          consider v2,w2 be Vertex of G such that

           A25: x = [v2, w2] & y2 = ((v2 .edgesInOut() ) /\ (w2 .edgesInOut() )) by A23;

          v1 = v2 & w1 = w2 by A24, A25, XTUPLE_0: 1;

          hence thesis by A24, A25;

        end;

        

         A26: for x be object st x in ( [:X, Y:] /\ [:V, V:]) holds ex y be object st P[x, y]

        proof

          let x be object;

          assume

           A27: x in ( [:X, Y:] /\ [:V, V:]);

          then x in [:X, Y:] by XBOOLE_0:def 4;

          then

          consider v,w be object such that

           A28: v in X & w in Y & x = [v, w] by ZFMISC_1:def 2;

          x in [:V, V:] by A27, XBOOLE_0:def 4;

          then

          consider v9,w9 be object such that

           A29: v9 in V & w9 in V & x = [v9, w9] by ZFMISC_1:def 2;

          reconsider v, w as Vertex of G by A28, A29, XTUPLE_0: 1;

          take ((v .edgesInOut() ) /\ (w .edgesInOut() )), v, w;

          thus thesis by A28;

        end;

        consider f be Function such that

         A30: ( dom f) = ( [:X, Y:] /\ [:V, V:]) and

         A31: for x be object st x in ( [:X, Y:] /\ [:V, V:]) holds P[x, (f . x)] from FUNCT_1:sch 2( A22, A26);

        

         A32: ( rng f) is finite by A30, FINSET_1: 8;

        now

          let E be object;

          assume E in S;

          then

          consider v,w be Vertex of G such that

           A33: E = ((v .edgesInOut() ) /\ (w .edgesInOut() )) & v in X & w in Y;

          

           A34: [v, w] in [:X, Y:] by A33, ZFMISC_1:def 2;

           [v, w] in [:V, V:] by ZFMISC_1:def 2;

          then

           A35: [v, w] in ( [:X, Y:] /\ [:V, V:]) by A34, XBOOLE_0:def 4;

          then

          consider v0,w0 be Vertex of G such that

           A36: [v, w] = [v0, w0] & (f . [v, w]) = ((v0 .edgesInOut() ) /\ (w0 .edgesInOut() )) by A31;

          v = v0 & w = w0 by A36, XTUPLE_0: 1;

          hence E in ( rng f) by A30, A33, A35, A36, FUNCT_1: 3;

        end;

        then S c= ( rng f) by TARSKI:def 3;

        then

         A37: S is finite by A32;

        for E be set st E in S holds E is finite

        proof

          let E be set;

          assume E in S;

          then

          consider v,w be Vertex of G such that

           A38: E = ((v .edgesInOut() ) /\ (w .edgesInOut() )) & v in X & w in Y;

          thus E is finite by A38;

        end;

        then

         A39: ( union S) is finite by A37, FINSET_1: 7;

        (G .edgesBetween (X,Y)) c= ( union S) by GLIBPRE0: 40;

        hence thesis by A39;

      end;

      cluster (G .edgesDBetween (X,Y)) -> finite;

      coherence

      proof

        (G .edgesDBetween (X,Y)) c= (G .edgesBetween (X,Y)) by GLIBPRE0: 31;

        hence thesis;

      end;

    end

    registration

      let G be locally-finite _Graph, v be Vertex of G;

      cluster (v .edgesIn() ) -> finite;

      coherence ;

      cluster (v .edgesOut() ) -> finite;

      coherence ;

      cluster (v .edgesInOut() ) -> finite;

      coherence ;

      cluster (v .inDegree() ) -> finite;

      coherence ;

      cluster (v .outDegree() ) -> finite;

      coherence ;

      cluster (v .degree() ) -> finite;

      coherence ;

    end

    definition

      let G be locally-finite _Graph, v be Vertex of G;

      :: original: .inDegree()

      redefine

      func v .inDegree() -> Nat ;

      coherence ;

      :: original: .outDegree()

      redefine

      func v .outDegree() -> Nat ;

      coherence ;

      :: original: .degree()

      redefine

      func v .degree() -> Nat ;

      coherence ;

    end

    registration

      let G be locally-finite _Graph, V be set;

      cluster -> locally-finite for addVertices of G, V;

      coherence

      proof

        let G1 be addVertices of G, V;

        let v be Vertex of G1;

        ( the_Vertices_of G1) = (( the_Vertices_of G) \/ V) by GLIB_006:def 10;

        per cases by XBOOLE_0:def 3;

          suppose v in ( the_Vertices_of G);

          then

          reconsider v0 = v as Vertex of G;

          (v0 .edgesInOut() ) is finite;

          hence (v .edgesInOut() ) is finite by GLIBPRE0: 47;

        end;

          suppose v in V & not v in ( the_Vertices_of G);

          then v in (V \ ( the_Vertices_of G)) by XBOOLE_0:def 5;

          hence (v .edgesInOut() ) is finite by GLIB_006: 88, GLIB_000:def 49;

        end;

      end;

      cluster -> locally-finite for addLoops of G, V;

      coherence

      proof

        let G1 be addLoops of G, V;

        per cases ;

          suppose

           A1: V c= ( the_Vertices_of G);

          let v1 be Vertex of G1;

          reconsider v2 = v1 as Vertex of G by A1, GLIB_012:def 5;

          per cases ;

            suppose v1 in V;

            then

            consider e be object such that e DJoins (v1,v1,G1) & not e in ( the_Edges_of G) and (v1 .edgesIn() ) = ((v2 .edgesIn() ) \/ {e}) and (v1 .edgesOut() ) = ((v2 .edgesOut() ) \/ {e}) and

             A2: (v1 .edgesInOut() ) = ((v2 .edgesInOut() ) \/ {e}) by A1, GLIB_012: 42;

            thus thesis by A2;

          end;

            suppose not v1 in V;

            then (v1 .edgesInOut() ) = (v2 .edgesInOut() ) by A1, GLIB_012: 44;

            hence thesis;

          end;

        end;

          suppose not V c= ( the_Vertices_of G);

          then G1 == G by GLIB_012:def 5;

          hence thesis by Th24;

        end;

      end;

    end

    registration

      let G be locally-finite _Graph, E be set;

      cluster -> locally-finite for reverseEdgeDirections of G, E;

      coherence

      proof

        let G2 be reverseEdgeDirections of G, E;

        let v2 be Vertex of G2;

        reconsider v1 = v2 as Vertex of G by GLIB_007: 4;

        (v1 .edgesInOut() ) = (v2 .edgesInOut() ) by GLIB_007: 12;

        hence thesis;

      end;

    end

    registration

      let G be locally-finite _Graph;

      let v,e,w be object;

      cluster -> locally-finite for addEdge of G, v, e, w;

      coherence

      proof

        let G1 be addEdge of G, v, e, w;

        per cases ;

          suppose

           A1: v is Vertex of G & w is Vertex of G & not e in ( the_Edges_of G);

          then

          reconsider v0 = v, w0 = w as Vertex of G;

          let v1 be Vertex of G1;

          reconsider v2 = v1 as Vertex of G by A1, GLIB_006:def 11;

          per cases ;

            suppose v2 <> v & v2 <> w;

            then (v1 .edgesInOut() ) = (v2 .edgesInOut() ) by GLIBPRE0: 48;

            hence thesis;

          end;

            suppose v2 = v & v <> w;

            then (v1 .edgesInOut() ) = ((v0 .edgesInOut() ) \/ {e}) by A1, GLIBPRE0: 49;

            hence thesis;

          end;

            suppose v2 = w & v <> w;

            then (v1 .edgesInOut() ) = ((w0 .edgesInOut() ) \/ {e}) by A1, GLIBPRE0: 50;

            hence thesis;

          end;

            suppose v2 = v & v = w;

            then (v1 .edgesInOut() ) = ((v0 .edgesInOut() ) \/ {e}) by A1, GLIBPRE0: 51;

            hence thesis;

          end;

        end;

          suppose not (v is Vertex of G & w is Vertex of G & not e in ( the_Edges_of G));

          then G1 == G by GLIB_006:def 11;

          hence thesis by Th24;

        end;

      end;

      cluster -> locally-finite for addAdjVertex of G, v, e, w;

      coherence

      proof

        let G1 be addAdjVertex of G, v, e, w;

        per cases ;

          suppose v in ( the_Vertices_of G) & not w in ( the_Vertices_of G) & not e in ( the_Edges_of G);

          then

          consider G3 be addVertex of G, w such that

           A2: G1 is addEdge of G3, v, e, w by GLIB_006: 125;

          thus thesis by A2;

        end;

          suppose not v in ( the_Vertices_of G) & w in ( the_Vertices_of G) & not e in ( the_Edges_of G);

          then

          consider G3 be addVertex of G, v such that

           A3: G1 is addEdge of G3, v, e, w by GLIB_006: 126;

          thus thesis by A3;

        end;

          suppose not ((v in ( the_Vertices_of G) & not w in ( the_Vertices_of G) & not e in ( the_Edges_of G)) or ( not v in ( the_Vertices_of G) & w in ( the_Vertices_of G) & not e in ( the_Edges_of G)));

          then G1 == G by GLIB_006:def 12;

          hence thesis by Th24;

        end;

      end;

    end

    theorem :: GLIB_013:29

    

     Th29: for G2 be _Graph, v be object, V be Subset of ( the_Vertices_of G2) holds for G1 be addAdjVertexAll of G2, v, V st not v in ( the_Vertices_of G2) holds (G2 is locally-finite & V is finite) iff G1 is locally-finite

    proof

      let G2 be _Graph, v be object, V be Subset of ( the_Vertices_of G2);

      let G1 be addAdjVertexAll of G2, v, V;

      assume

       A1: not v in ( the_Vertices_of G2);

      hereby

        assume

         A2: G2 is locally-finite & V is finite;

        now

          let v1 be Vertex of G1;

          per cases ;

            suppose v1 = v;

            then (v1 .degree() ) = ( card V) by A1, GLIBPRE0: 57;

            hence (v1 .degree() ) is finite by A2;

          end;

            suppose v1 <> v;

            then

             A3: not v1 in {v} by TARSKI:def 1;

            ( the_Vertices_of G1) = (( the_Vertices_of G2) \/ {v}) by A1, GLIB_007:def 4;

            then

            reconsider v2 = v1 as Vertex of G2 by A3, XBOOLE_0:def 3;

            per cases ;

              suppose not v2 in V;

              then (v1 .degree() ) = (v2 .degree() ) by GLIBPRE0: 58;

              hence (v1 .degree() ) is finite by A2;

            end;

              suppose v2 in V;

              then (v1 .degree() ) = ((v2 .degree() ) +` 1) by A1, GLIBPRE0: 59;

              hence (v1 .degree() ) is finite by A2;

            end;

          end;

        end;

        hence G1 is locally-finite by Th23;

      end;

      assume

       A4: G1 is locally-finite;

      G2 is Subgraph of G1 by GLIB_006: 57;

      hence G2 is locally-finite by A4;

      reconsider w = v as Vertex of G1 by A1, GLIB_007: 50;

      (w .degree() ) is finite by A4;

      then ( card V) is finite by A1, GLIBPRE0: 57;

      hence V is finite;

    end;

    registration

      let G be locally-finite _Graph;

      let v be object, V be finite set;

      cluster -> locally-finite for addAdjVertexAll of G, v, V;

      coherence

      proof

        let G1 be addAdjVertexAll of G, v, V;

        per cases ;

          suppose V c= ( the_Vertices_of G) & not v in ( the_Vertices_of G);

          hence thesis by Th29;

        end;

          suppose not (V c= ( the_Vertices_of G) & not v in ( the_Vertices_of G));

          then G1 == G by GLIB_007:def 4;

          hence thesis by Th24;

        end;

      end;

    end

    registration

      let G be non locally-finite _Graph;

      cluster -> non locally-finite for Supergraph of G;

      coherence

      proof

        let G1 be Supergraph of G;

        G is Subgraph of G1 by GLIB_006: 57;

        hence thesis;

      end;

      let E be finite set;

      cluster -> non locally-finite for removeEdges of G, E;

      coherence

      proof

        let G2 be removeEdges of G, E;

        consider v1 be Vertex of G such that

         A1: (v1 .edgesInOut() ) is infinite by Def5;

        reconsider v2 = v1 as Vertex of G2 by GLIB_000: 53;

        (v2 .edgesInOut() ) = ((v1 .edgesInOut() ) \ E) by GLIBPRE0: 42;

        hence thesis by A1;

      end;

    end

    registration

      let G be non locally-finite _Graph, e be set;

      cluster -> non locally-finite for removeEdge of G, e;

      coherence ;

    end

    theorem :: GLIB_013:30

    

     Th30: for G1 be non locally-finite _Graph holds for V be finite Subset of ( the_Vertices_of G1) holds for G2 be removeVertices of G1, V st for v be Vertex of G1 st v in V holds (v .edgesInOut() ) is finite holds G2 is non locally-finite

    proof

      let G1 be non locally-finite _Graph;

      let V be finite Subset of ( the_Vertices_of G1);

      let G2 be removeVertices of G1, V;

      assume

       A1: for v be Vertex of G1 st v in V holds (v .edgesInOut() ) is finite;

      per cases ;

        suppose

         A2: (( the_Vertices_of G1) \ V) is non empty Subset of ( the_Vertices_of G1);

        consider v1 be Vertex of G1 such that

         A3: (v1 .edgesInOut() ) is infinite by Def5;

        

         A4: ( the_Vertices_of G2) = (( the_Vertices_of G1) \ V) by A2, GLIB_000:def 37;

         not v1 in V by A1, A3;

        then

        reconsider v2 = v1 as Vertex of G2 by A4, XBOOLE_0:def 5;

         not ( the_Vertices_of G1) c= V by A2, XBOOLE_1: 37;

        then V c< ( the_Vertices_of G1) by XBOOLE_0:def 8;

        then

         A5: (v2 .edgesInOut() ) = ((v1 .edgesInOut() ) \ (G1 .edgesInOut V)) by GLIBPRE0: 44;

        deffunc F( Vertex of G1) = ($1 .edgesInOut() );

        set S = { F(v) where v be Vertex of G1 : v in V };

        

         A6: V is finite;

        

         A7: S is finite from FRAENKEL:sch 21( A6);

        now

          let X be set;

          assume X in S;

          then

          consider v be Vertex of G1 such that

           A8: X = F(v) & v in V;

          thus X is finite by A1, A8;

        end;

        then ( union S) is finite by A7, FINSET_1: 7;

        then (G1 .edgesInOut V) is finite by GLIBPRE0: 38;

        hence thesis by A3, A5;

      end;

        suppose not ((( the_Vertices_of G1) \ V) is non empty Subset of ( the_Vertices_of G1));

        then G1 == G2 by GLIB_000:def 37;

        hence thesis by Th24;

      end;

    end;

    theorem :: GLIB_013:31

    for G1 be non locally-finite _Graph, v be Vertex of G1 holds for G2 be removeVertex of G1, v st (v .edgesInOut() ) is finite holds G2 is non locally-finite

    proof

      let G1 be non locally-finite _Graph, v be Vertex of G1;

      let G2 be removeVertex of G1, v;

      assume

       A1: (v .edgesInOut() ) is finite;

      for w be Vertex of G1 st w in {v} holds (w .edgesInOut() ) is finite by A1, TARSKI:def 1;

      hence thesis by Th30;

    end;

    theorem :: GLIB_013:32

    

     Th32: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is weak_SG-embedding & G2 is locally-finite holds G1 is locally-finite

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is weak_SG-embedding & G2 is locally-finite;

      now

        let v be Vertex of G1;

        (v .degree() ) c= (((F _V ) /. v) .degree() ) by A1, GLIBPRE0: 91;

        hence (v .degree() ) is finite by A1;

      end;

      hence thesis by Th23;

    end;

    theorem :: GLIB_013:33

    for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is onto semi-Dcontinuous & G1 is locally-finite holds G2 is locally-finite

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is onto semi-Dcontinuous & G1 is locally-finite;

      now

        let v be Vertex of G2;

        ( rng (F _V )) = ( the_Vertices_of G2) by A1, GLIB_010:def 12;

        then

        consider v0 be object such that

         A2: v0 in ( dom (F _V )) & ((F _V ) . v0) = v by FUNCT_1:def 3;

        reconsider v0 as Vertex of G1 by A2;

        (((F _V ) /. v0) .degree() ) c= (v0 .degree() ) by A1, A2, GLIBPRE0: 93;

        hence (v .degree() ) is finite by A1, A2, PARTFUN1:def 6;

      end;

      hence thesis by Th23;

    end;

    theorem :: GLIB_013:34

    for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is isomorphism holds G1 is locally-finite iff G2 is locally-finite

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is isomorphism;

      hereby

        assume

         A2: G1 is locally-finite;

        now

          let v be Vertex of G2;

          ( rng (F _V )) = ( the_Vertices_of G2) by A1, GLIB_010:def 12;

          then

          consider v0 be object such that

           A3: v0 in ( dom (F _V )) & ((F _V ) . v0) = v by FUNCT_1:def 3;

          reconsider v0 as Vertex of G1 by A3;

          (((F _V ) /. v0) .degree() ) = (v0 .degree() ) by A1, GLIBPRE0: 95;

          hence (v .degree() ) is finite by A2, A3, PARTFUN1:def 6;

        end;

        hence G2 is locally-finite by Th23;

      end;

      thus thesis by A1, Th32;

    end;

    begin

    definition

      let G be _Graph;

      :: GLIB_013:def6

      func G .supDegree() -> Cardinal equals ( union the set of all (v .degree() ) where v be Vertex of G);

      coherence

      proof

        now

          let x be set;

          assume x in the set of all (v .degree() ) where v be Vertex of G;

          then

          consider v be Vertex of G such that

           A1: x = (v .degree() );

          thus x is cardinal number by A1;

        end;

        hence thesis by TOPGEN_2: 3;

      end;

      :: GLIB_013:def7

      func G .supInDegree() -> Cardinal equals ( union the set of all (v .inDegree() ) where v be Vertex of G);

      coherence

      proof

        now

          let x be set;

          assume x in the set of all (v .inDegree() ) where v be Vertex of G;

          then

          consider v be Vertex of G such that

           A2: x = (v .inDegree() );

          thus x is cardinal number by A2;

        end;

        hence thesis by TOPGEN_2: 3;

      end;

      :: GLIB_013:def8

      func G .supOutDegree() -> Cardinal equals ( union the set of all (v .outDegree() ) where v be Vertex of G);

      coherence

      proof

        now

          let x be set;

          assume x in the set of all (v .outDegree() ) where v be Vertex of G;

          then

          consider v be Vertex of G such that

           A3: x = (v .outDegree() );

          thus x is cardinal number by A3;

        end;

        hence thesis by TOPGEN_2: 3;

      end;

      :: GLIB_013:def9

      func G .minDegree() -> Cardinal equals ( meet the set of all (v .degree() ) where v be Vertex of G);

      coherence

      proof

        now

          let x be set;

          assume x in the set of all (v .degree() ) where v be Vertex of G;

          then

          consider v be Vertex of G such that

           A4: x = (v .degree() );

          thus x is cardinal number by A4;

        end;

        hence thesis by GLIBPRE0: 15;

      end;

      :: GLIB_013:def10

      func G .minInDegree() -> Cardinal equals ( meet the set of all (v .inDegree() ) where v be Vertex of G);

      coherence

      proof

        now

          let x be set;

          assume x in the set of all (v .inDegree() ) where v be Vertex of G;

          then

          consider v be Vertex of G such that

           A5: x = (v .inDegree() );

          thus x is cardinal number by A5;

        end;

        hence thesis by GLIBPRE0: 15;

      end;

      :: GLIB_013:def11

      func G .minOutDegree() -> Cardinal equals ( meet the set of all (v .outDegree() ) where v be Vertex of G);

      coherence

      proof

        now

          let x be set;

          assume x in the set of all (v .outDegree() ) where v be Vertex of G;

          then

          consider v be Vertex of G such that

           A6: x = (v .outDegree() );

          thus x is cardinal number by A6;

        end;

        hence thesis by GLIBPRE0: 15;

      end;

    end

    theorem :: GLIB_013:35

    

     Th35: for G be _Graph, v be Vertex of G holds (G .minDegree() ) c= (v .degree() ) & (v .degree() ) c= (G .supDegree() ) & (G .minInDegree() ) c= (v .inDegree() ) & (v .inDegree() ) c= (G .supInDegree() ) & (G .minOutDegree() ) c= (v .outDegree() ) & (v .outDegree() ) c= (G .supOutDegree() )

    proof

      let G be _Graph, v be Vertex of G;

      (v .degree() ) in the set of all (w .degree() ) where w be Vertex of G;

      hence (G .minDegree() ) c= (v .degree() ) & (v .degree() ) c= (G .supDegree() ) by ZFMISC_1: 74, SETFAM_1: 3;

      (v .inDegree() ) in the set of all (w .inDegree() ) where w be Vertex of G;

      hence (G .minInDegree() ) c= (v .inDegree() ) & (v .inDegree() ) c= (G .supInDegree() ) by ZFMISC_1: 74, SETFAM_1: 3;

      (v .outDegree() ) in the set of all (w .outDegree() ) where w be Vertex of G;

      hence (G .minOutDegree() ) c= (v .outDegree() ) & (v .outDegree() ) c= (G .supOutDegree() ) by ZFMISC_1: 74, SETFAM_1: 3;

    end;

    theorem :: GLIB_013:36

    

     Th36: for G be _Graph, c be Cardinal holds (G .minDegree() ) = c iff ex v be Vertex of G st (v .degree() ) = c & for w be Vertex of G holds (v .degree() ) c= (w .degree() )

    proof

      let G be _Graph, c be Cardinal;

      set S = the set of all (v .degree() ) where v be Vertex of G;

      ( the Vertex of G .degree() ) in S;

      then

       A1: S <> {} ;

      now

        let x be set;

        assume x in S;

        then

        consider v be Vertex of G such that

         A2: x = (v .degree() );

        thus x is cardinal number by A2;

      end;

      then

      consider A be Cardinal such that

       A3: A in S & A = (G .minDegree() ) by A1, GLIBPRE0: 14;

      hereby

        assume

         A4: (G .minDegree() ) = c;

        consider v be Vertex of G such that

         A5: A = (v .degree() ) by A3;

        take v;

        thus (v .degree() ) = c by A4, A3, A5;

        let w be Vertex of G;

        (w .degree() ) in S;

        hence (v .degree() ) c= (w .degree() ) by A3, A5, SETFAM_1: 3;

      end;

      given v be Vertex of G such that

       A6: (v .degree() ) = c and

       A7: for w be Vertex of G holds (v .degree() ) c= (w .degree() );

      c in S by A6;

      then

       A8: (G .minDegree() ) c= c by SETFAM_1: 3;

      now

        let x be object;

        assume

         A9: x in c;

        now

          let X be set;

          assume X in S;

          then

          consider w be Vertex of G such that

           A10: X = (w .degree() );

          c c= X by A6, A7, A10;

          hence x in X by A9;

        end;

        hence x in ( meet S) by A1, SETFAM_1:def 1;

      end;

      then c c= (G .minDegree() ) by TARSKI:def 3;

      hence (G .minDegree() ) = c by A8, XBOOLE_0:def 10;

    end;

    theorem :: GLIB_013:37

    

     Th37: for G be _Graph, c be Cardinal holds (G .minInDegree() ) = c iff ex v be Vertex of G st (v .inDegree() ) = c & for w be Vertex of G holds (v .inDegree() ) c= (w .inDegree() )

    proof

      let G be _Graph, c be Cardinal;

      set S = the set of all (v .inDegree() ) where v be Vertex of G;

      ( the Vertex of G .inDegree() ) in S;

      then

       A1: S <> {} ;

      now

        let x be set;

        assume x in S;

        then

        consider v be Vertex of G such that

         A2: x = (v .inDegree() );

        thus x is cardinal number by A2;

      end;

      then

      consider A be Cardinal such that

       A3: A in S & A = (G .minInDegree() ) by A1, GLIBPRE0: 14;

      hereby

        assume

         A4: (G .minInDegree() ) = c;

        consider v be Vertex of G such that

         A5: A = (v .inDegree() ) by A3;

        take v;

        thus (v .inDegree() ) = c by A4, A3, A5;

        let w be Vertex of G;

        (w .inDegree() ) in S;

        hence (v .inDegree() ) c= (w .inDegree() ) by A3, A5, SETFAM_1: 3;

      end;

      given v be Vertex of G such that

       A6: (v .inDegree() ) = c and

       A7: for w be Vertex of G holds (v .inDegree() ) c= (w .inDegree() );

      c in S by A6;

      then

       A8: (G .minInDegree() ) c= c by SETFAM_1: 3;

      now

        let x be object;

        assume

         A9: x in c;

        now

          let X be set;

          assume X in S;

          then

          consider w be Vertex of G such that

           A10: X = (w .inDegree() );

          c c= X by A6, A7, A10;

          hence x in X by A9;

        end;

        hence x in ( meet S) by A1, SETFAM_1:def 1;

      end;

      then c c= (G .minInDegree() ) by TARSKI:def 3;

      hence (G .minInDegree() ) = c by A8, XBOOLE_0:def 10;

    end;

    theorem :: GLIB_013:38

    

     Th38: for G be _Graph, c be Cardinal holds (G .minOutDegree() ) = c iff ex v be Vertex of G st (v .outDegree() ) = c & for w be Vertex of G holds (v .outDegree() ) c= (w .outDegree() )

    proof

      let G be _Graph, c be Cardinal;

      set S = the set of all (v .outDegree() ) where v be Vertex of G;

      ( the Vertex of G .outDegree() ) in S;

      then

       A1: S <> {} ;

      now

        let x be set;

        assume x in S;

        then

        consider v be Vertex of G such that

         A2: x = (v .outDegree() );

        thus x is cardinal number by A2;

      end;

      then

      consider A be Cardinal such that

       A3: A in S & A = (G .minOutDegree() ) by A1, GLIBPRE0: 14;

      hereby

        assume

         A4: (G .minOutDegree() ) = c;

        consider v be Vertex of G such that

         A5: A = (v .outDegree() ) by A3;

        take v;

        thus (v .outDegree() ) = c by A4, A3, A5;

        let w be Vertex of G;

        (w .outDegree() ) in S;

        hence (v .outDegree() ) c= (w .outDegree() ) by A3, A5, SETFAM_1: 3;

      end;

      given v be Vertex of G such that

       A6: (v .outDegree() ) = c and

       A7: for w be Vertex of G holds (v .outDegree() ) c= (w .outDegree() );

      c in S by A6;

      then

       A8: (G .minOutDegree() ) c= c by SETFAM_1: 3;

      now

        let x be object;

        assume

         A9: x in c;

        now

          let X be set;

          assume X in S;

          then

          consider w be Vertex of G such that

           A10: X = (w .outDegree() );

          c c= X by A6, A7, A10;

          hence x in X by A9;

        end;

        hence x in ( meet S) by A1, SETFAM_1:def 1;

      end;

      then c c= (G .minOutDegree() ) by TARSKI:def 3;

      hence (G .minOutDegree() ) = c by A8, XBOOLE_0:def 10;

    end;

    theorem :: GLIB_013:39

    

     Th39: for G be _Graph holds (G .supInDegree() ) c= (G .supDegree() )

    proof

      let G be _Graph;

      now

        let x be object;

        assume x in (G .supInDegree() );

        then

        consider X be set such that

         A1: x in X & X in the set of all (v .inDegree() ) where v be Vertex of G by TARSKI:def 4;

        consider v be Vertex of G such that

         A2: X = (v .inDegree() ) by A1;

        (v .inDegree() ) c= (v .degree() ) by CARD_2: 94;

        then

         A3: x in (v .degree() ) by A1, A2;

        (v .degree() ) in the set of all (w .degree() ) where w be Vertex of G;

        hence x in (G .supDegree() ) by A3, TARSKI:def 4;

      end;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: GLIB_013:40

    

     Th40: for G be _Graph holds (G .supOutDegree() ) c= (G .supDegree() )

    proof

      let G be _Graph;

      now

        let x be object;

        assume x in (G .supOutDegree() );

        then

        consider X be set such that

         A1: x in X & X in the set of all (v .outDegree() ) where v be Vertex of G by TARSKI:def 4;

        consider v be Vertex of G such that

         A2: X = (v .outDegree() ) by A1;

        (v .outDegree() ) c= (v .degree() ) by CARD_2: 94;

        then

         A3: x in (v .degree() ) by A1, A2;

        (v .degree() ) in the set of all (w .degree() ) where w be Vertex of G;

        hence x in (G .supDegree() ) by A3, TARSKI:def 4;

      end;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: GLIB_013:41

    for G be _Graph holds (G .minInDegree() ) c= (G .minDegree() )

    proof

      let G be _Graph;

      consider v1 be Vertex of G such that

       A1: (v1 .inDegree() ) = (G .minInDegree() ) and

       A2: for w be Vertex of G holds (v1 .inDegree() ) c= (w .inDegree() ) by Th37;

      consider v2 be Vertex of G such that

       A3: (v2 .degree() ) = (G .minDegree() ) and for w be Vertex of G holds (v2 .degree() ) c= (w .degree() ) by Th36;

      

       A4: (v2 .inDegree() ) c= (G .minDegree() ) by A3, CARD_2: 94;

      (v1 .inDegree() ) c= (v2 .inDegree() ) by A2;

      hence thesis by A1, A4, XBOOLE_1: 1;

    end;

    theorem :: GLIB_013:42

    for G be _Graph holds (G .minOutDegree() ) c= (G .minDegree() )

    proof

      let G be _Graph;

      consider v1 be Vertex of G such that

       A1: (v1 .outDegree() ) = (G .minOutDegree() ) and

       A2: for w be Vertex of G holds (v1 .outDegree() ) c= (w .outDegree() ) by Th38;

      consider v2 be Vertex of G such that

       A3: (v2 .degree() ) = (G .minDegree() ) and for w be Vertex of G holds (v2 .degree() ) c= (w .degree() ) by Th36;

      

       A4: (v2 .outDegree() ) c= (G .minDegree() ) by A3, CARD_2: 94;

      (v1 .outDegree() ) c= (v2 .outDegree() ) by A2;

      hence thesis by A1, A4, XBOOLE_1: 1;

    end;

    theorem :: GLIB_013:43

    for G be _Graph holds (G .minDegree() ) c= (G .supDegree() ) by SETFAM_1: 2;

    theorem :: GLIB_013:44

    for G be _Graph holds (G .minInDegree() ) c= (G .supInDegree() ) by SETFAM_1: 2;

    theorem :: GLIB_013:45

    for G be _Graph holds (G .minOutDegree() ) c= (G .supOutDegree() ) by SETFAM_1: 2;

    theorem :: GLIB_013:46

    

     Th46: for G be _Graph st ex v be Vertex of G st v is isolated holds (G .minDegree() ) = 0 & (G .minInDegree() ) = 0 & (G .minOutDegree() ) = 0

    proof

      let G be _Graph;

      given v be Vertex of G such that

       A1: v is isolated;

      

       A2: (v .degree() ) = 0 by A1, GLIBPRE0: 35;

      for w be Vertex of G holds (v .degree() ) c= (w .degree() ) by A2, XBOOLE_1: 2;

      hence (G .minDegree() ) = 0 by A2, Th36;

      

       A3: (v .inDegree() ) = 0 & (v .outDegree() ) = 0 by A1, GLIBPRE0: 34;

      for w be Vertex of G holds (v .inDegree() ) c= (w .inDegree() ) by A3, XBOOLE_1: 2;

      hence (G .minInDegree() ) = 0 by A3, Th37;

      for w be Vertex of G holds (v .outDegree() ) c= (w .outDegree() ) by A3, XBOOLE_1: 2;

      hence (G .minOutDegree() ) = 0 by A3, Th38;

    end;

    theorem :: GLIB_013:47

    for G be _Graph st (G .minDegree() ) = 0 holds ex v be Vertex of G st v is isolated

    proof

      let G be _Graph;

      assume (G .minDegree() ) = 0 ;

      then

      consider v be Vertex of G such that

       A1: (v .degree() ) = 0 and for w be Vertex of G holds (v .degree() ) c= (w .degree() ) by Th36;

      take v;

      thus thesis by A1, GLIBPRE0: 35;

    end;

    theorem :: GLIB_013:48

    

     Th48: for G be _Graph, c be Cardinal st ex v be Vertex of G st (v .degree() ) = c & for w be Vertex of G holds (w .degree() ) c= (v .degree() ) holds (G .supDegree() ) = c

    proof

      let G be _Graph, c be Cardinal;

      given v be Vertex of G such that

       A1: (v .degree() ) = c and

       A2: for w be Vertex of G holds (w .degree() ) c= (v .degree() );

      set S = the set of all (v .degree() ) where v be Vertex of G;

      c in S by A1;

      then

       A3: c c= (G .supDegree() ) by ZFMISC_1: 74;

      now

        let x be object;

        assume x in (G .supDegree() );

        then

        consider X be set such that

         A4: x in X & X in S by TARSKI:def 4;

        consider w be Vertex of G such that

         A5: X = (w .degree() ) by A4;

        X c= (v .degree() ) by A2, A5;

        hence x in c by A1, A4;

      end;

      then (G .supDegree() ) c= c by TARSKI:def 3;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: GLIB_013:49

    

     Th49: for G be _Graph, c be Cardinal st ex v be Vertex of G st (v .inDegree() ) = c & for w be Vertex of G holds (w .inDegree() ) c= (v .inDegree() ) holds (G .supInDegree() ) = c

    proof

      let G be _Graph, c be Cardinal;

      given v be Vertex of G such that

       A1: (v .inDegree() ) = c and

       A2: for w be Vertex of G holds (w .inDegree() ) c= (v .inDegree() );

      set S = the set of all (v .inDegree() ) where v be Vertex of G;

      c in S by A1;

      then

       A3: c c= (G .supInDegree() ) by ZFMISC_1: 74;

      now

        let x be object;

        assume x in (G .supInDegree() );

        then

        consider X be set such that

         A4: x in X & X in S by TARSKI:def 4;

        consider w be Vertex of G such that

         A5: X = (w .inDegree() ) by A4;

        X c= (v .inDegree() ) by A2, A5;

        hence x in c by A1, A4;

      end;

      then (G .supInDegree() ) c= c by TARSKI:def 3;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: GLIB_013:50

    

     Th50: for G be _Graph, c be Cardinal st ex v be Vertex of G st (v .outDegree() ) = c & for w be Vertex of G holds (w .outDegree() ) c= (v .outDegree() ) holds (G .supOutDegree() ) = c

    proof

      let G be _Graph, c be Cardinal;

      given v be Vertex of G such that

       A1: (v .outDegree() ) = c and

       A2: for w be Vertex of G holds (w .outDegree() ) c= (v .outDegree() );

      set S = the set of all (v .outDegree() ) where v be Vertex of G;

      c in S by A1;

      then

       A3: c c= (G .supOutDegree() ) by ZFMISC_1: 74;

      now

        let x be object;

        assume x in (G .supOutDegree() );

        then

        consider X be set such that

         A4: x in X & X in S by TARSKI:def 4;

        consider w be Vertex of G such that

         A5: X = (w .outDegree() ) by A4;

        X c= (v .outDegree() ) by A2, A5;

        hence x in c by A1, A4;

      end;

      then (G .supOutDegree() ) c= c by TARSKI:def 3;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: GLIB_013:51

    

     Th51: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is weak_SG-embedding holds (G1 .supDegree() ) c= (G2 .supDegree() )

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is weak_SG-embedding;

      set D1 = the set of all (v .degree() ) where v be Vertex of G1;

      set D2 = the set of all (w .degree() ) where w be Vertex of G2;

      now

        let x be object;

        assume x in (G1 .supDegree() );

        then

        consider d1 be set such that

         A2: x in d1 & d1 in D1 by TARSKI:def 4;

        consider v be Vertex of G1 such that

         A3: d1 = (v .degree() ) by A2;

        (v .degree() ) c= (((F _V ) /. v) .degree() ) by A1, GLIBPRE0: 91;

        then

         A4: x in (((F _V ) /. v) .degree() ) by A2, A3;

        (((F _V ) /. v) .degree() ) in D2;

        hence x in (G2 .supDegree() ) by A4, TARSKI:def 4;

      end;

      hence (G1 .supDegree() ) c= (G2 .supDegree() ) by TARSKI:def 3;

    end;

    theorem :: GLIB_013:52

    

     Th52: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is weak_SG-embedding & ( rng (F _V )) = ( the_Vertices_of G2) holds (G1 .minDegree() ) c= (G2 .minDegree() )

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is weak_SG-embedding & ( rng (F _V )) = ( the_Vertices_of G2);

      consider v1 be Vertex of G1 such that

       A2: (v1 .degree() ) = (G1 .minDegree() ) and

       A3: for w1 be Vertex of G1 holds (v1 .degree() ) c= (w1 .degree() ) by Th36;

      consider v2 be Vertex of G2 such that

       A4: (v2 .degree() ) = (G2 .minDegree() ) and for w2 be Vertex of G2 holds (v2 .degree() ) c= (w2 .degree() ) by Th36;

      consider v0 be object such that

       A5: v0 in ( dom (F _V )) & ((F _V ) . v0) = v2 by A1, FUNCT_1:def 3;

      reconsider v0 as Vertex of G1 by A5;

      (v0 .degree() ) c= (((F _V ) /. v0) .degree() ) by A1, GLIBPRE0: 91;

      then

       A6: (v0 .degree() ) c= (v2 .degree() ) by A5, PARTFUN1:def 6;

      (v1 .degree() ) c= (v0 .degree() ) by A3;

      hence thesis by A2, A4, A6, XBOOLE_1: 1;

    end;

    theorem :: GLIB_013:53

    for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is onto semi-Dcontinuous holds (G2 .supDegree() ) c= (G1 .supDegree() )

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is onto semi-Dcontinuous;

      set D1 = the set of all (v .degree() ) where v be Vertex of G1;

      set D2 = the set of all (w .degree() ) where w be Vertex of G2;

      now

        let x be object;

        assume x in (G2 .supDegree() );

        then

        consider d2 be set such that

         A2: x in d2 & d2 in D2 by TARSKI:def 4;

        consider w be Vertex of G2 such that

         A3: d2 = (w .degree() ) by A2;

        ( rng (F _V )) = ( the_Vertices_of G2) by A1, GLIB_010:def 12;

        then

        consider v be object such that

         A4: v in ( dom (F _V )) & ((F _V ) . v) = w by FUNCT_1:def 3;

        reconsider v as Vertex of G1 by A4;

        (((F _V ) /. v) .degree() ) c= (v .degree() ) by A1, A4, GLIBPRE0: 93;

        then (w .degree() ) c= (v .degree() ) by A4, PARTFUN1:def 6;

        then

         A5: x in (v .degree() ) by A2, A3;

        (v .degree() ) in D1;

        hence x in (G1 .supDegree() ) by A5, TARSKI:def 4;

      end;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: GLIB_013:54

    for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is onto semi-Dcontinuous & ( dom (F _V )) = ( the_Vertices_of G1) holds (G2 .minDegree() ) c= (G1 .minDegree() )

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is onto semi-Dcontinuous & ( dom (F _V )) = ( the_Vertices_of G1);

      consider v1 be Vertex of G1 such that

       A2: (v1 .degree() ) = (G1 .minDegree() ) and for w1 be Vertex of G1 holds (v1 .degree() ) c= (w1 .degree() ) by Th36;

      consider v2 be Vertex of G2 such that

       A3: (v2 .degree() ) = (G2 .minDegree() ) and

       A4: for w2 be Vertex of G2 holds (v2 .degree() ) c= (w2 .degree() ) by Th36;

      

       A5: (((F _V ) /. v1) .degree() ) c= (v1 .degree() ) by A1, GLIBPRE0: 93;

      (v2 .degree() ) c= (((F _V ) /. v1) .degree() ) by A4;

      hence thesis by A2, A3, A5, XBOOLE_1: 1;

    end;

    theorem :: GLIB_013:55

    

     Th55: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is isomorphism holds (G1 .supDegree() ) = (G2 .supDegree() ) & (G1 .minDegree() ) = (G2 .minDegree() )

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is isomorphism;

      then ( rng (F _V )) = ( the_Vertices_of G2) by GLIB_010:def 12;

      then

       A2: (G1 .supDegree() ) c= (G2 .supDegree() ) & (G1 .minDegree() ) c= (G2 .minDegree() ) by A1, Th51, Th52;

      reconsider F0 = F as one-to-one PGraphMapping of G1, G2 by A1;

      

       A3: (F0 " ) is isomorphism by A1, GLIB_010: 75;

      then ( rng ((F0 " ) _V )) = ( the_Vertices_of G1) by GLIB_010:def 12;

      then (G2 .supDegree() ) c= (G1 .supDegree() ) & (G2 .minDegree() ) c= (G1 .minDegree() ) by A3, Th51, Th52;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: GLIB_013:56

    

     Th56: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is directed weak_SG-embedding holds (G1 .supInDegree() ) c= (G2 .supInDegree() ) & (G1 .supOutDegree() ) c= (G2 .supOutDegree() )

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is directed weak_SG-embedding;

      set D1 = the set of all (v .inDegree() ) where v be Vertex of G1;

      set D2 = the set of all (w .inDegree() ) where w be Vertex of G2;

      now

        let x be object;

        assume x in (G1 .supInDegree() );

        then

        consider d1 be set such that

         A2: x in d1 & d1 in D1 by TARSKI:def 4;

        consider v be Vertex of G1 such that

         A3: d1 = (v .inDegree() ) by A2;

        (v .inDegree() ) c= (((F _V ) /. v) .inDegree() ) by A1, GLIBPRE0: 90;

        then

         A4: x in (((F _V ) /. v) .inDegree() ) by A2, A3;

        (((F _V ) /. v) .inDegree() ) in D2;

        hence x in (G2 .supInDegree() ) by A4, TARSKI:def 4;

      end;

      hence (G1 .supInDegree() ) c= (G2 .supInDegree() ) by TARSKI:def 3;

      set D3 = the set of all (v .outDegree() ) where v be Vertex of G1;

      set D4 = the set of all (w .outDegree() ) where w be Vertex of G2;

      now

        let x be object;

        assume x in (G1 .supOutDegree() );

        then

        consider d1 be set such that

         A5: x in d1 & d1 in D3 by TARSKI:def 4;

        consider v be Vertex of G1 such that

         A6: d1 = (v .outDegree() ) by A5;

        (v .outDegree() ) c= (((F _V ) /. v) .outDegree() ) by A1, GLIBPRE0: 90;

        then

         A7: x in (((F _V ) /. v) .outDegree() ) by A5, A6;

        (((F _V ) /. v) .outDegree() ) in D4;

        hence x in (G2 .supOutDegree() ) by A7, TARSKI:def 4;

      end;

      hence (G1 .supOutDegree() ) c= (G2 .supOutDegree() ) by TARSKI:def 3;

    end;

    theorem :: GLIB_013:57

    

     Th57: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is directed weak_SG-embedding & ( rng (F _V )) = ( the_Vertices_of G2) holds (G1 .minInDegree() ) c= (G2 .minInDegree() ) & (G1 .minOutDegree() ) c= (G2 .minOutDegree() )

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is directed weak_SG-embedding & ( rng (F _V )) = ( the_Vertices_of G2);

      consider v1 be Vertex of G1 such that

       A2: (v1 .inDegree() ) = (G1 .minInDegree() ) and

       A3: for w1 be Vertex of G1 holds (v1 .inDegree() ) c= (w1 .inDegree() ) by Th37;

      consider v2 be Vertex of G2 such that

       A4: (v2 .inDegree() ) = (G2 .minInDegree() ) and for w2 be Vertex of G2 holds (v2 .inDegree() ) c= (w2 .inDegree() ) by Th37;

      consider v0 be object such that

       A5: v0 in ( dom (F _V )) & ((F _V ) . v0) = v2 by A1, FUNCT_1:def 3;

      reconsider v0 as Vertex of G1 by A5;

      (v0 .inDegree() ) c= (((F _V ) /. v0) .inDegree() ) by A1, GLIBPRE0: 90;

      then

       A6: (v0 .inDegree() ) c= (v2 .inDegree() ) by A5, PARTFUN1:def 6;

      (v1 .inDegree() ) c= (v0 .inDegree() ) by A3;

      hence (G1 .minInDegree() ) c= (G2 .minInDegree() ) by A2, A4, A6, XBOOLE_1: 1;

      consider v3 be Vertex of G1 such that

       A7: (v3 .outDegree() ) = (G1 .minOutDegree() ) and

       A8: for w3 be Vertex of G1 holds (v3 .outDegree() ) c= (w3 .outDegree() ) by Th38;

      consider v4 be Vertex of G2 such that

       A9: (v4 .outDegree() ) = (G2 .minOutDegree() ) and for w4 be Vertex of G2 holds (v4 .outDegree() ) c= (w4 .outDegree() ) by Th38;

      consider v9 be object such that

       A10: v9 in ( dom (F _V )) & ((F _V ) . v9) = v4 by A1, FUNCT_1:def 3;

      reconsider v9 as Vertex of G1 by A10;

      (v9 .outDegree() ) c= (((F _V ) /. v9) .outDegree() ) by A1, GLIBPRE0: 90;

      then

       A11: (v9 .outDegree() ) c= (v4 .outDegree() ) by A10, PARTFUN1:def 6;

      (v3 .outDegree() ) c= (v9 .outDegree() ) by A8;

      hence thesis by A7, A9, A11, XBOOLE_1: 1;

    end;

    theorem :: GLIB_013:58

    

     Th58: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is onto semi-Dcontinuous holds (G2 .supInDegree() ) c= (G1 .supInDegree() ) & (G2 .supOutDegree() ) c= (G1 .supOutDegree() )

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is onto semi-Dcontinuous;

      set D1 = the set of all (v .inDegree() ) where v be Vertex of G1;

      set D2 = the set of all (w .inDegree() ) where w be Vertex of G2;

      now

        let x be object;

        assume x in (G2 .supInDegree() );

        then

        consider d2 be set such that

         A2: x in d2 & d2 in D2 by TARSKI:def 4;

        consider w be Vertex of G2 such that

         A3: d2 = (w .inDegree() ) by A2;

        ( rng (F _V )) = ( the_Vertices_of G2) by A1, GLIB_010:def 12;

        then

        consider v be object such that

         A4: v in ( dom (F _V )) & ((F _V ) . v) = w by FUNCT_1:def 3;

        reconsider v as Vertex of G1 by A4;

        (((F _V ) /. v) .inDegree() ) c= (v .inDegree() ) by A1, A4, GLIBPRE0: 92;

        then (w .inDegree() ) c= (v .inDegree() ) by A4, PARTFUN1:def 6;

        then

         A5: x in (v .inDegree() ) by A2, A3;

        (v .inDegree() ) in D1;

        hence x in (G1 .supInDegree() ) by A5, TARSKI:def 4;

      end;

      hence (G2 .supInDegree() ) c= (G1 .supInDegree() ) by TARSKI:def 3;

      set D3 = the set of all (v .outDegree() ) where v be Vertex of G1;

      set D4 = the set of all (w .outDegree() ) where w be Vertex of G2;

      now

        let x be object;

        assume x in (G2 .supOutDegree() );

        then

        consider d2 be set such that

         A6: x in d2 & d2 in D4 by TARSKI:def 4;

        consider w be Vertex of G2 such that

         A7: d2 = (w .outDegree() ) by A6;

        ( rng (F _V )) = ( the_Vertices_of G2) by A1, GLIB_010:def 12;

        then

        consider v be object such that

         A8: v in ( dom (F _V )) & ((F _V ) . v) = w by FUNCT_1:def 3;

        reconsider v as Vertex of G1 by A8;

        (((F _V ) /. v) .outDegree() ) c= (v .outDegree() ) by A1, A8, GLIBPRE0: 92;

        then (w .outDegree() ) c= (v .outDegree() ) by A8, PARTFUN1:def 6;

        then

         A9: x in (v .outDegree() ) by A6, A7;

        (v .outDegree() ) in D3;

        hence x in (G1 .supOutDegree() ) by A9, TARSKI:def 4;

      end;

      hence (G2 .supOutDegree() ) c= (G1 .supOutDegree() ) by TARSKI:def 3;

    end;

    theorem :: GLIB_013:59

    

     Th59: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is onto semi-Dcontinuous & ( dom (F _V )) = ( the_Vertices_of G1) holds (G2 .minInDegree() ) c= (G1 .minInDegree() ) & (G2 .minOutDegree() ) c= (G1 .minOutDegree() )

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is onto semi-Dcontinuous & ( dom (F _V )) = ( the_Vertices_of G1);

      consider v1 be Vertex of G1 such that

       A2: (v1 .inDegree() ) = (G1 .minInDegree() ) and for w1 be Vertex of G1 holds (v1 .inDegree() ) c= (w1 .inDegree() ) by Th37;

      consider v2 be Vertex of G2 such that

       A3: (v2 .inDegree() ) = (G2 .minInDegree() ) and

       A4: for w2 be Vertex of G2 holds (v2 .inDegree() ) c= (w2 .inDegree() ) by Th37;

      

       A5: (((F _V ) /. v1) .inDegree() ) c= (v1 .inDegree() ) by A1, GLIBPRE0: 92;

      (v2 .inDegree() ) c= (((F _V ) /. v1) .inDegree() ) by A4;

      hence (G2 .minInDegree() ) c= (G1 .minInDegree() ) by A2, A3, A5, XBOOLE_1: 1;

      consider v3 be Vertex of G1 such that

       A6: (v3 .outDegree() ) = (G1 .minOutDegree() ) and for w3 be Vertex of G1 holds (v3 .outDegree() ) c= (w3 .outDegree() ) by Th38;

      consider v4 be Vertex of G2 such that

       A7: (v4 .outDegree() ) = (G2 .minOutDegree() ) and

       A8: for w4 be Vertex of G2 holds (v4 .outDegree() ) c= (w4 .outDegree() ) by Th38;

      

       A9: (((F _V ) /. v3) .outDegree() ) c= (v3 .outDegree() ) by A1, GLIBPRE0: 92;

      (v4 .outDegree() ) c= (((F _V ) /. v3) .outDegree() ) by A8;

      hence (G2 .minOutDegree() ) c= (G1 .minOutDegree() ) by A6, A7, A9, XBOOLE_1: 1;

    end;

    theorem :: GLIB_013:60

    

     Th60: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is Disomorphism holds (G1 .supInDegree() ) = (G2 .supInDegree() ) & (G1 .supOutDegree() ) = (G2 .supOutDegree() ) & (G1 .minInDegree() ) = (G2 .minInDegree() ) & (G1 .minOutDegree() ) = (G2 .minOutDegree() )

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is Disomorphism;

      then

       A2: ( dom (F _V )) = ( the_Vertices_of G1) & ( rng (F _V )) = ( the_Vertices_of G2) by GLIB_010:def 11, GLIB_010:def 12;

      

       A3: (G1 .supInDegree() ) c= (G2 .supInDegree() ) & (G1 .supOutDegree() ) c= (G2 .supOutDegree() ) by A1, Th56;

      

       A4: (G1 .minInDegree() ) c= (G2 .minInDegree() ) & (G1 .minOutDegree() ) c= (G2 .minOutDegree() ) by A1, A2, Th57;

      

       A5: (G2 .supInDegree() ) c= (G1 .supInDegree() ) & (G2 .supOutDegree() ) c= (G1 .supOutDegree() ) by A1, Th58;

      

       A6: (G2 .minInDegree() ) c= (G1 .minInDegree() ) & (G2 .minOutDegree() ) c= (G1 .minOutDegree() ) by A1, A2, Th59;

      thus thesis by A3, A4, A5, A6, XBOOLE_0:def 10;

    end;

    theorem :: GLIB_013:61

    for G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E holds (G1 .supDegree() ) = (G2 .supDegree() ) & (G1 .minDegree() ) = (G2 .minDegree() )

    proof

      let G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E;

      set S1 = the set of all (v .degree() ) where v be Vertex of G1;

      set S2 = the set of all (v .degree() ) where v be Vertex of G2;

      now

        let x be object;

        hereby

          assume x in S1;

          then

          consider v1 be Vertex of G1 such that

           A1: x = (v1 .degree() );

          reconsider v2 = v1 as Vertex of G2 by GLIB_007: 4;

          x = (v2 .degree() ) by A1, GLIBPRE0: 56;

          hence x in S2;

        end;

        assume x in S2;

        then

        consider v2 be Vertex of G2 such that

         A2: x = (v2 .degree() );

        reconsider v1 = v2 as Vertex of G1 by GLIB_007: 4;

        x = (v1 .degree() ) by A2, GLIBPRE0: 56;

        hence x in S1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLIB_013:62

    

     Th62: for G1,G2 be _Graph st G1 == G2 holds (G1 .supDegree() ) = (G2 .supDegree() ) & (G1 .minDegree() ) = (G2 .minDegree() ) & (G1 .supInDegree() ) = (G2 .supInDegree() ) & (G1 .minInDegree() ) = (G2 .minInDegree() ) & (G1 .supOutDegree() ) = (G2 .supOutDegree() ) & (G1 .minOutDegree() ) = (G2 .minOutDegree() )

    proof

      let G1,G2 be _Graph;

      assume

       A1: G1 == G2;

      set S1 = the set of all (v .degree() ) where v be Vertex of G1;

      set S2 = the set of all (v .degree() ) where v be Vertex of G2;

      now

        let x be object;

        hereby

          assume x in S1;

          then

          consider v1 be Vertex of G1 such that

           A2: x = (v1 .degree() );

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

          x = (v2 .degree() ) by A1, A2, GLIB_000: 96;

          hence x in S2;

        end;

        assume x in S2;

        then

        consider v2 be Vertex of G2 such that

         A3: x = (v2 .degree() );

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

        x = (v1 .degree() ) by A1, A3, GLIB_000: 96;

        hence x in S1;

      end;

      hence (G1 .supDegree() ) = (G2 .supDegree() ) & (G1 .minDegree() ) = (G2 .minDegree() ) by TARSKI: 2;

      set S3 = the set of all (v .inDegree() ) where v be Vertex of G1;

      set S4 = the set of all (v .inDegree() ) where v be Vertex of G2;

      now

        let x be object;

        hereby

          assume x in S3;

          then

          consider v1 be Vertex of G1 such that

           A4: x = (v1 .inDegree() );

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

          x = (v2 .inDegree() ) by A1, A4, GLIB_000: 96;

          hence x in S4;

        end;

        assume x in S4;

        then

        consider v2 be Vertex of G2 such that

         A5: x = (v2 .inDegree() );

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

        x = (v1 .inDegree() ) by A1, A5, GLIB_000: 96;

        hence x in S3;

      end;

      hence (G1 .supInDegree() ) = (G2 .supInDegree() ) & (G1 .minInDegree() ) = (G2 .minInDegree() ) by TARSKI: 2;

      set S5 = the set of all (v .outDegree() ) where v be Vertex of G1;

      set S6 = the set of all (v .outDegree() ) where v be Vertex of G2;

      now

        let x be object;

        hereby

          assume x in S5;

          then

          consider v1 be Vertex of G1 such that

           A6: x = (v1 .outDegree() );

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

          x = (v2 .outDegree() ) by A1, A6, GLIB_000: 96;

          hence x in S6;

        end;

        assume x in S6;

        then

        consider v2 be Vertex of G2 such that

         A7: x = (v2 .outDegree() );

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

        x = (v1 .outDegree() ) by A1, A7, GLIB_000: 96;

        hence x in S5;

      end;

      hence (G1 .supOutDegree() ) = (G2 .supOutDegree() ) & (G1 .minOutDegree() ) = (G2 .minOutDegree() ) by TARSKI: 2;

    end;

    theorem :: GLIB_013:63

    

     Th63: for G1 be _Graph, G2 be Subgraph of G1 holds (G2 .supDegree() ) c= (G1 .supDegree() ) & (G2 .supInDegree() ) c= (G1 .supInDegree() ) & (G2 .supOutDegree() ) c= (G1 .supOutDegree() )

    proof

      let G1 be _Graph, G2 be Subgraph of G1;

      set F = (( id G1) | G2);

      F is directed weak_SG-embedding by GLIB_010: 57;

      hence thesis by Th51, Th56;

    end;

    theorem :: GLIB_013:64

    for G1 be _Graph, G2 be spanning Subgraph of G1 holds (G2 .minDegree() ) c= (G1 .minDegree() ) & (G2 .minInDegree() ) c= (G1 .minInDegree() ) & (G2 .minOutDegree() ) c= (G1 .minOutDegree() )

    proof

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

      set F = (( id G1) | G2);

      

       A1: F is directed weak_SG-embedding by GLIB_010: 57;

      ( rng (F _V )) = ( rng ((( id G1) _V ) | ( the_Vertices_of G1))) by GLIB_000:def 33

      .= ( the_Vertices_of G1);

      hence thesis by A1, Th52, Th57;

    end;

    theorem :: GLIB_013:65

    for G2 be _Graph, V be set, G1 be addVertices of G2, V holds (G1 .supDegree() ) = (G2 .supDegree() ) & (G1 .supInDegree() ) = (G2 .supInDegree() ) & (G1 .supOutDegree() ) = (G2 .supOutDegree() )

    proof

      let G2 be _Graph, V be set, G1 be addVertices of G2, V;

      G2 is Subgraph of G1 by GLIB_006: 57;

      then

       A1: (G2 .supDegree() ) c= (G1 .supDegree() ) & (G2 .supInDegree() ) c= (G1 .supInDegree() ) & (G2 .supOutDegree() ) c= (G1 .supOutDegree() ) by Th63;

      

       A2: ( the_Vertices_of G1) = (( the_Vertices_of G2) \/ V) by GLIB_006:def 10;

      set D1 = the set of all (v .degree() ) where v be Vertex of G1;

      set D2 = the set of all (v .degree() ) where v be Vertex of G2;

      now

        let x be object;

        assume x in (G1 .supDegree() );

        then

        consider d1 be set such that

         A3: x in d1 & d1 in D1 by TARSKI:def 4;

        consider v1 be Vertex of G1 such that

         A4: d1 = (v1 .degree() ) by A3;

         not v1 in (V \ ( the_Vertices_of G2)) by A3, A4, GLIBPRE0: 35, GLIB_006: 88;

        then v1 in ( the_Vertices_of G2) or not v1 in V by XBOOLE_0:def 5;

        then

        reconsider v2 = v1 as Vertex of G2 by A2, XBOOLE_0:def 3;

        d1 = (v2 .degree() ) & (v2 .degree() ) in D2 by A4, GLIBPRE0: 47;

        hence x in (G2 .supDegree() ) by A3, TARSKI:def 4;

      end;

      then (G1 .supDegree() ) c= (G2 .supDegree() ) by TARSKI:def 3;

      hence (G1 .supDegree() ) = (G2 .supDegree() ) by A1, XBOOLE_0:def 10;

      set D3 = the set of all (v .inDegree() ) where v be Vertex of G1;

      set D4 = the set of all (v .inDegree() ) where v be Vertex of G2;

      now

        let x be object;

        assume x in (G1 .supInDegree() );

        then

        consider d1 be set such that

         A5: x in d1 & d1 in D3 by TARSKI:def 4;

        consider v1 be Vertex of G1 such that

         A6: d1 = (v1 .inDegree() ) by A5;

        v1 is non isolated by A5, A6, GLIBPRE0: 34;

        then not v1 in (V \ ( the_Vertices_of G2)) by GLIB_006: 88;

        then v1 in ( the_Vertices_of G2) or not v1 in V by XBOOLE_0:def 5;

        then

        reconsider v2 = v1 as Vertex of G2 by A2, XBOOLE_0:def 3;

        d1 = (v2 .inDegree() ) & (v2 .inDegree() ) in D4 by A6, GLIBPRE0: 47;

        hence x in (G2 .supInDegree() ) by A5, TARSKI:def 4;

      end;

      then (G1 .supInDegree() ) c= (G2 .supInDegree() ) by TARSKI:def 3;

      hence (G1 .supInDegree() ) = (G2 .supInDegree() ) by A1, XBOOLE_0:def 10;

      set D5 = the set of all (v .outDegree() ) where v be Vertex of G1;

      set D6 = the set of all (v .outDegree() ) where v be Vertex of G2;

      now

        let x be object;

        assume x in (G1 .supOutDegree() );

        then

        consider d1 be set such that

         A7: x in d1 & d1 in D5 by TARSKI:def 4;

        consider v1 be Vertex of G1 such that

         A8: d1 = (v1 .outDegree() ) by A7;

        v1 is non isolated by A7, A8, GLIBPRE0: 34;

        then not v1 in (V \ ( the_Vertices_of G2)) by GLIB_006: 88;

        then v1 in ( the_Vertices_of G2) or not v1 in V by XBOOLE_0:def 5;

        then

        reconsider v2 = v1 as Vertex of G2 by A2, XBOOLE_0:def 3;

        d1 = (v2 .outDegree() ) & (v2 .outDegree() ) in D6 by A8, GLIBPRE0: 47;

        hence x in (G2 .supOutDegree() ) by A7, TARSKI:def 4;

      end;

      then (G1 .supOutDegree() ) c= (G2 .supOutDegree() ) by TARSKI:def 3;

      hence (G1 .supOutDegree() ) = (G2 .supOutDegree() ) by A1, XBOOLE_0:def 10;

    end;

    theorem :: GLIB_013:66

    for G2 be _Graph, V be set, G1 be addVertices of G2, V st (V \ ( the_Vertices_of G2)) <> {} holds (G1 .minDegree() ) = 0 & (G1 .minInDegree() ) = 0 & (G1 .minOutDegree() ) = 0

    proof

      let G2 be _Graph, V be set, G1 be addVertices of G2, V;

      assume (V \ ( the_Vertices_of G2)) <> {} ;

      then

      consider v be object such that

       A1: v in (V \ ( the_Vertices_of G2)) by XBOOLE_0:def 1;

      reconsider v as Vertex of G1 by A1, GLIB_006: 86;

      v is isolated by A1, GLIB_006: 88;

      hence thesis by Th46;

    end;

    registration

      let G be non edgeless _Graph;

      cluster (G .supDegree() ) -> non empty;

      coherence

      proof

        consider e be object such that

         A1: e in ( the_Edges_of G) by XBOOLE_0:def 1;

        set v = (( the_Source_of G) . e), w = (( the_Target_of G) . e);

        reconsider v as Vertex of G by A1, FUNCT_2: 5;

        e in (v .edgesOut() ) by A1, GLIB_000: 58;

        then (v .outDegree() ) <> 0 & 0 c= (v .outDegree() ) by XBOOLE_1: 2;

        then 0 in (v .outDegree() ) by XBOOLE_0:def 8, ORDINAL1: 11;

        then

         A2: 0 in (v .degree() ) by CARD_2: 94, TARSKI:def 3;

        (v .degree() ) in the set of all (u .degree() ) where u be Vertex of G;

        then (v .degree() ) c= (G .supDegree() ) by ZFMISC_1: 74;

        hence thesis by A2;

      end;

      cluster (G .supInDegree() ) -> non empty;

      coherence

      proof

        consider e be object such that

         A3: e in ( the_Edges_of G) by XBOOLE_0:def 1;

        set v = (( the_Source_of G) . e), w = (( the_Target_of G) . e);

        reconsider w as Vertex of G by A3, FUNCT_2: 5;

        e in (w .edgesIn() ) by A3, GLIB_000: 56;

        then (w .inDegree() ) <> 0 & 0 c= (w .inDegree() ) by XBOOLE_1: 2;

        then

         A4: 0 in (w .inDegree() ) by XBOOLE_0:def 8, ORDINAL1: 11;

        (w .inDegree() ) in the set of all (u .inDegree() ) where u be Vertex of G;

        then (w .inDegree() ) c= (G .supInDegree() ) by ZFMISC_1: 74;

        hence thesis by A4;

      end;

      cluster (G .supOutDegree() ) -> non empty;

      coherence

      proof

        consider e be object such that

         A5: e in ( the_Edges_of G) by XBOOLE_0:def 1;

        set v = (( the_Source_of G) . e), w = (( the_Target_of G) . e);

        reconsider v as Vertex of G by A5, FUNCT_2: 5;

        e in (v .edgesOut() ) by A5, GLIB_000: 58;

        then (v .outDegree() ) <> 0 & 0 c= (v .outDegree() ) by XBOOLE_1: 2;

        then

         A6: 0 in (v .outDegree() ) by XBOOLE_0:def 8, ORDINAL1: 11;

        (v .outDegree() ) in the set of all (u .outDegree() ) where u be Vertex of G;

        then (v .outDegree() ) c= (G .supOutDegree() ) by ZFMISC_1: 74;

        hence thesis by A6;

      end;

    end

    registration

      let G be locally-finite _Graph;

      cluster (G .minDegree() ) -> natural;

      coherence

      proof

        consider v be Vertex of G such that

         A1: (v .degree() ) = (G .minDegree() ) and for w be Vertex of G holds (v .degree() ) c= (w .degree() ) by Th36;

        thus thesis by A1;

      end;

      cluster (G .minInDegree() ) -> natural;

      coherence

      proof

        consider v be Vertex of G such that

         A2: (v .inDegree() ) = (G .minInDegree() ) and for w be Vertex of G holds (v .inDegree() ) c= (w .inDegree() ) by Th37;

        thus thesis by A2;

      end;

      cluster (G .minOutDegree() ) -> natural;

      coherence

      proof

        consider v be Vertex of G such that

         A3: (v .outDegree() ) = (G .minOutDegree() ) and for w be Vertex of G holds (v .outDegree() ) c= (w .outDegree() ) by Th38;

        thus thesis by A3;

      end;

    end

    definition

      let G be locally-finite _Graph;

      :: original: .minDegree()

      redefine

      func G .minDegree() -> Nat ;

      coherence ;

      :: original: .minInDegree()

      redefine

      func G .minInDegree() -> Nat ;

      coherence ;

      :: original: .minOutDegree()

      redefine

      func G .minOutDegree() -> Nat ;

      coherence ;

    end

    theorem :: GLIB_013:67

    for G be locally-finite _Graph, n be Nat holds (G .minDegree() ) = n iff ex v be Vertex of G st (v .degree() ) = n & for w be Vertex of G holds (v .degree() ) <= (w .degree() )

    proof

      let G be locally-finite _Graph, n be Nat;

      hereby

        assume (G .minDegree() ) = n;

        then

        consider v be Vertex of G such that

         A1: (v .degree() ) = n and

         A2: for w be Vertex of G holds (v .degree() ) c= (w .degree() ) by Th36;

        take v;

        thus (v .degree() ) = n by A1;

        let w be Vertex of G;

        ( Segm (v .degree() )) c= ( Segm (w .degree() )) by A2;

        hence (v .degree() ) <= (w .degree() ) by NAT_1: 39;

      end;

      given v be Vertex of G such that

       A3: (v .degree() ) = n and

       A4: for w be Vertex of G holds (v .degree() ) <= (w .degree() );

      now

        let w be Vertex of G;

        ( Segm (v .degree() )) c= ( Segm (w .degree() )) by A4, NAT_1: 39;

        hence (v .degree() ) c= (w .degree() );

      end;

      hence thesis by A3, Th36;

    end;

    theorem :: GLIB_013:68

    for G be locally-finite _Graph, n be Nat holds (G .minInDegree() ) = n iff ex v be Vertex of G st (v .inDegree() ) = n & for w be Vertex of G holds (v .inDegree() ) <= (w .inDegree() )

    proof

      let G be locally-finite _Graph, n be Nat;

      hereby

        assume (G .minInDegree() ) = n;

        then

        consider v be Vertex of G such that

         A1: (v .inDegree() ) = n and

         A2: for w be Vertex of G holds (v .inDegree() ) c= (w .inDegree() ) by Th37;

        take v;

        thus (v .inDegree() ) = n by A1;

        let w be Vertex of G;

        ( Segm (v .inDegree() )) c= ( Segm (w .inDegree() )) by A2;

        hence (v .inDegree() ) <= (w .inDegree() ) by NAT_1: 39;

      end;

      given v be Vertex of G such that

       A3: (v .inDegree() ) = n and

       A4: for w be Vertex of G holds (v .inDegree() ) <= (w .inDegree() );

      now

        let w be Vertex of G;

        ( Segm (v .inDegree() )) c= ( Segm (w .inDegree() )) by A4, NAT_1: 39;

        hence (v .inDegree() ) c= (w .inDegree() );

      end;

      hence thesis by A3, Th37;

    end;

    theorem :: GLIB_013:69

    for G be locally-finite _Graph, n be Nat holds (G .minOutDegree() ) = n iff ex v be Vertex of G st (v .outDegree() ) = n & for w be Vertex of G holds (v .outDegree() ) <= (w .outDegree() )

    proof

      let G be locally-finite _Graph, n be Nat;

      hereby

        assume (G .minOutDegree() ) = n;

        then

        consider v be Vertex of G such that

         A1: (v .outDegree() ) = n and

         A2: for w be Vertex of G holds (v .outDegree() ) c= (w .outDegree() ) by Th38;

        take v;

        thus (v .outDegree() ) = n by A1;

        let w be Vertex of G;

        ( Segm (v .outDegree() )) c= ( Segm (w .outDegree() )) by A2;

        hence (v .outDegree() ) <= (w .outDegree() ) by NAT_1: 39;

      end;

      given v be Vertex of G such that

       A3: (v .outDegree() ) = n and

       A4: for w be Vertex of G holds (v .outDegree() ) <= (w .outDegree() );

      now

        let w be Vertex of G;

        ( Segm (v .outDegree() )) c= ( Segm (w .outDegree() )) by A4, NAT_1: 39;

        hence (v .outDegree() ) c= (w .outDegree() );

      end;

      hence thesis by A3, Th38;

    end;

    

     Lm1: for a,b be Cardinal st a c= b & a <> b holds (a +` 1) c= b

    proof

      let a,b be Cardinal;

      assume

       A1: a c= b & a <> b;

      then a c< b by XBOOLE_0:def 8;

      then

       A2: ( succ a) c= b by ORDINAL1: 11, ORDINAL1: 21;

      per cases ;

        suppose a is finite;

        then

        reconsider n = a as Nat;

        (a +` 1) = (n +` 1)

        .= ( Segm (n + 1))

        .= ( succ ( Segm n)) by NAT_1: 38

        .= ( succ a);

        hence thesis by A2;

      end;

        suppose

         A3: a is infinite;

        then 1 c= a;

        hence thesis by A1, A3, CARD_2: 76;

      end;

    end;

    theorem :: GLIB_013:70

    

     Th70: for G2 be _Graph, v,w be Vertex of G2, e be object holds for G1 be addEdge of G2, v, e, w st v <> w holds (G1 .minDegree() ) = (G2 .minDegree() ) or (G1 .minDegree() ) = (((v .degree() ) /\ (w .degree() )) +` 1)

    proof

      let G2 be _Graph, v,w be Vertex of G2, e be object;

      let G1 be addEdge of G2, v, e, w;

      assume

       A1: v <> w;

      per cases ;

        suppose

         A2: not e in ( the_Edges_of G2);

        then

         A3: ( the_Vertices_of G1) = ( the_Vertices_of G2) by GLIB_006:def 11;

        then

        reconsider v9 = v, w9 = w as Vertex of G1;

        consider v1 be Vertex of G1 such that

         A4: (v1 .degree() ) = (G1 .minDegree() ) and

         A5: for w1 be Vertex of G1 holds (v1 .degree() ) c= (w1 .degree() ) by Th36;

        reconsider v4 = v1 as Vertex of G2 by A3;

        consider v2 be Vertex of G2 such that

         A6: (v2 .degree() ) = (G2 .minDegree() ) and

         A7: for w2 be Vertex of G2 holds (v2 .degree() ) c= (w2 .degree() ) by Th36;

        reconsider v3 = v2 as Vertex of G1 by A3;

        

         A8: (v2 .degree() ) c= (v4 .degree() ) & (v1 .degree() ) c= (v3 .degree() ) by A5, A7;

        

         A9: G2 is Subgraph of G1 by GLIB_006: 57;

        then

         A10: (v4 .inDegree() ) c= (v1 .inDegree() ) & (v2 .inDegree() ) c= (v3 .inDegree() ) by GLIB_000: 78, CARD_1: 11;

        (v4 .outDegree() ) c= (v1 .outDegree() ) & (v2 .outDegree() ) c= (v3 .outDegree() ) by A9, GLIB_000: 78, CARD_1: 11;

        then (v4 .degree() ) c= (v1 .degree() ) & (v2 .degree() ) c= (v3 .degree() ) by A10, CARD_2: 83;

        then

         A11: (v2 .degree() ) c= (v1 .degree() ) & (v4 .degree() ) c= (v3 .degree() ) by A8, XBOOLE_1: 1;

        assume (G1 .minDegree() ) <> (G2 .minDegree() );

        then

         A12: (v1 .degree() ) <> (v2 .degree() ) by A4, A6;

        then

         A13: ((v2 .degree() ) +` 1) c= (v1 .degree() ) by A11, Lm1;

        

         A14: v2 = v or v2 = w

        proof

          assume v2 <> v & v2 <> w;

          then

           A15: (v2 .degree() ) = (v3 .degree() ) by GLIBPRE0: 48;

          then

           A16: ((v3 .degree() ) +` 1) c= (v3 .degree() ) by A8, A13, XBOOLE_1: 1;

          (v3 .degree() ) c= ((v3 .degree() ) +` 1) by CARD_2: 94;

          then (v3 .degree() ) = ((v3 .degree() ) +` 1) by A16, XBOOLE_0:def 10;

          hence contradiction by A8, A12, A13, A15, XBOOLE_0:def 10;

        end;

        then (v3 .degree() ) = ((v2 .degree() ) +` 1) by A1, A2, GLIBPRE0: 50, GLIBPRE0: 49;

        then (v1 .degree() ) = ((v2 .degree() ) +` 1) by A8, A13, XBOOLE_0:def 10;

        hence thesis by A4, A7, A14, XBOOLE_1: 28;

      end;

        suppose e in ( the_Edges_of G2);

        then G1 == G2 by GLIB_006:def 11;

        hence thesis by Th62;

      end;

    end;

    theorem :: GLIB_013:71

    

     Th71: for G2 be _Graph, v,w be Vertex of G2, e be object holds for G1 be addEdge of G2, v, e, w st v <> w holds (G1 .minInDegree() ) = (G2 .minInDegree() ) or (G1 .minInDegree() ) = ((w .inDegree() ) +` 1)

    proof

      let G2 be _Graph, v,w be Vertex of G2, e be object;

      let G1 be addEdge of G2, v, e, w;

      assume

       A1: v <> w;

      per cases ;

        suppose

         A2: not e in ( the_Edges_of G2);

        then

         A3: ( the_Vertices_of G1) = ( the_Vertices_of G2) by GLIB_006:def 11;

        then

        reconsider v9 = v, w9 = w as Vertex of G1;

        consider v1 be Vertex of G1 such that

         A4: (v1 .inDegree() ) = (G1 .minInDegree() ) and

         A5: for w1 be Vertex of G1 holds (v1 .inDegree() ) c= (w1 .inDegree() ) by Th37;

        reconsider v4 = v1 as Vertex of G2 by A3;

        consider v2 be Vertex of G2 such that

         A6: (v2 .inDegree() ) = (G2 .minInDegree() ) and

         A7: for w2 be Vertex of G2 holds (v2 .inDegree() ) c= (w2 .inDegree() ) by Th37;

        reconsider v3 = v2 as Vertex of G1 by A3;

        

         A8: (v2 .inDegree() ) c= (v4 .inDegree() ) & (v1 .inDegree() ) c= (v3 .inDegree() ) by A5, A7;

        G2 is Subgraph of G1 by GLIB_006: 57;

        then (v4 .inDegree() ) c= (v1 .inDegree() ) & (v2 .inDegree() ) c= (v3 .inDegree() ) by CARD_1: 11, GLIB_000: 78;

        then

         A9: (v2 .inDegree() ) c= (v1 .inDegree() ) & (v4 .inDegree() ) c= (v3 .inDegree() ) by A8, XBOOLE_1: 1;

        assume (G1 .minInDegree() ) <> (G2 .minInDegree() );

        then

         A10: (v1 .inDegree() ) <> (v2 .inDegree() ) by A4, A6;

        then

         A11: ((v2 .inDegree() ) +` 1) c= (v1 .inDegree() ) by A9, Lm1;

        

         A12: v2 = w

        proof

          assume

           A13: v2 <> w;

          

           A14: (v2 .inDegree() ) = (v3 .inDegree() )

          proof

            per cases ;

              suppose v2 = v;

              hence thesis by A1, A2, GLIBPRE0: 49;

            end;

              suppose v2 <> v;

              hence thesis by A13, GLIBPRE0: 48;

            end;

          end;

          then

           A15: ((v3 .inDegree() ) +` 1) c= (v3 .inDegree() ) by A8, A11, XBOOLE_1: 1;

          (v3 .inDegree() ) c= ((v3 .inDegree() ) +` 1) by CARD_2: 94;

          then (v3 .inDegree() ) = ((v3 .inDegree() ) +` 1) by A15, XBOOLE_0:def 10;

          hence contradiction by A8, A10, A11, A14, XBOOLE_0:def 10;

        end;

        then (v3 .inDegree() ) = ((v2 .inDegree() ) +` 1) by A1, A2, GLIBPRE0: 50;

        hence thesis by A4, A8, A11, A12, XBOOLE_0:def 10;

      end;

        suppose e in ( the_Edges_of G2);

        then G1 == G2 by GLIB_006:def 11;

        hence thesis by Th62;

      end;

    end;

    theorem :: GLIB_013:72

    

     Th72: for G2 be _Graph, v,w be Vertex of G2, e be object holds for G1 be addEdge of G2, v, e, w st v <> w holds (G1 .minOutDegree() ) = (G2 .minOutDegree() ) or (G1 .minOutDegree() ) = ((v .outDegree() ) +` 1)

    proof

      let G2 be _Graph, v,w be Vertex of G2, e be object;

      let G1 be addEdge of G2, v, e, w;

      assume

       A1: v <> w;

      per cases ;

        suppose

         A2: not e in ( the_Edges_of G2);

        then

         A3: ( the_Vertices_of G1) = ( the_Vertices_of G2) by GLIB_006:def 11;

        then

        reconsider v9 = v, w9 = w as Vertex of G1;

        consider v1 be Vertex of G1 such that

         A4: (v1 .outDegree() ) = (G1 .minOutDegree() ) and

         A5: for w1 be Vertex of G1 holds (v1 .outDegree() ) c= (w1 .outDegree() ) by Th38;

        reconsider v4 = v1 as Vertex of G2 by A3;

        consider v2 be Vertex of G2 such that

         A6: (v2 .outDegree() ) = (G2 .minOutDegree() ) and

         A7: for w2 be Vertex of G2 holds (v2 .outDegree() ) c= (w2 .outDegree() ) by Th38;

        reconsider v3 = v2 as Vertex of G1 by A3;

        

         A8: (v2 .outDegree() ) c= (v4 .outDegree() ) & (v1 .outDegree() ) c= (v3 .outDegree() ) by A5, A7;

        G2 is Subgraph of G1 by GLIB_006: 57;

        then (v4 .outDegree() ) c= (v1 .outDegree() ) & (v2 .outDegree() ) c= (v3 .outDegree() ) by CARD_1: 11, GLIB_000: 78;

        then

         A9: (v2 .outDegree() ) c= (v1 .outDegree() ) & (v4 .outDegree() ) c= (v3 .outDegree() ) by A8, XBOOLE_1: 1;

        assume (G1 .minOutDegree() ) <> (G2 .minOutDegree() );

        then

         A10: (v1 .outDegree() ) <> (v2 .outDegree() ) by A4, A6;

        then

         A11: ((v2 .outDegree() ) +` 1) c= (v1 .outDegree() ) by A9, Lm1;

        

         A12: v2 = v

        proof

          assume

           A13: v2 <> v;

          

           A14: (v2 .outDegree() ) = (v3 .outDegree() )

          proof

            per cases ;

              suppose v2 = w;

              hence thesis by A1, A2, GLIBPRE0: 50;

            end;

              suppose v2 <> w;

              hence thesis by A13, GLIBPRE0: 48;

            end;

          end;

          then

           A15: ((v3 .outDegree() ) +` 1) c= (v3 .outDegree() ) by A8, A11, XBOOLE_1: 1;

          (v3 .outDegree() ) c= ((v3 .outDegree() ) +` 1) by CARD_2: 94;

          then (v3 .outDegree() ) = ((v3 .outDegree() ) +` 1) by A15, XBOOLE_0:def 10;

          hence contradiction by A8, A10, A11, A14, XBOOLE_0:def 10;

        end;

        then (v3 .outDegree() ) = ((v2 .outDegree() ) +` 1) by A1, A2, GLIBPRE0: 49;

        hence thesis by A4, A8, A11, A12, XBOOLE_0:def 10;

      end;

        suppose e in ( the_Edges_of G2);

        then G1 == G2 by GLIB_006:def 11;

        hence thesis by Th62;

      end;

    end;

    theorem :: GLIB_013:73

    for G2 be locally-finite _Graph, v,w be Vertex of G2, e be object holds for G1 be addEdge of G2, v, e, w st v <> w holds (G1 .minDegree() ) = (G2 .minDegree() ) or (G1 .minDegree() ) = (( min ((v .degree() ),(w .degree() ))) + 1)

    proof

      let G2 be locally-finite _Graph, v,w be Vertex of G2, e be object;

      let G1 be addEdge of G2, v, e, w;

      (( min ((v .degree() ),(w .degree() ))) + 1) = (((v .degree() ) /\ (w .degree() )) +` 1);

      hence thesis by Th70;

    end;

    theorem :: GLIB_013:74

    for G2 be locally-finite _Graph, v,w be Vertex of G2, e be object holds for G1 be addEdge of G2, v, e, w st v <> w holds (G1 .minInDegree() ) = (G2 .minInDegree() ) or (G1 .minInDegree() ) = ((w .inDegree() ) + 1)

    proof

      let G2 be locally-finite _Graph, v,w be Vertex of G2, e be object;

      let G1 be addEdge of G2, v, e, w;

      ((w .inDegree() ) +` 1) = ((w .inDegree() ) +` 1);

      hence thesis by Th71;

    end;

    theorem :: GLIB_013:75

    for G2 be locally-finite _Graph, v,w be Vertex of G2, e be object holds for G1 be addEdge of G2, v, e, w st v <> w holds (G1 .minOutDegree() ) = (G2 .minOutDegree() ) or (G1 .minOutDegree() ) = ((v .outDegree() ) + 1)

    proof

      let G2 be locally-finite _Graph, v,w be Vertex of G2, e be object;

      let G1 be addEdge of G2, v, e, w;

      ((v .outDegree() ) +` 1) = ((v .outDegree() ) +` 1);

      hence thesis by Th72;

    end;

    theorem :: GLIB_013:76

    

     Th76: for G2 be _Graph, v be object holds for G1 be addAdjVertexAll of G2, v st not v in ( the_Vertices_of G2) holds (G1 .minDegree() ) = (((G2 .minDegree() ) +` 1) /\ (G2 .order() ))

    proof

      let G2 be _Graph, v be object;

      let G1 be addAdjVertexAll of G2, v;

      assume

       A1: not v in ( the_Vertices_of G2);

      then

      reconsider v9 = v as Vertex of G1 by GLIB_007: 50;

      consider v0 be Vertex of G2 such that

       A2: (G2 .minDegree() ) = (v0 .degree() ) and

       A3: for w0 be Vertex of G2 holds (v0 .degree() ) c= (w0 .degree() ) by Th36;

      

       A4: ( the_Vertices_of G1) = (( the_Vertices_of G2) \/ {v}) by A1, GLIB_007:def 4;

      then

      reconsider v1 = v0 as Vertex of G1 by XBOOLE_0:def 3;

      

       A5: ( the_Vertices_of G2) c= ( the_Vertices_of G2);

      

       A6: (v9 .degree() ) = (G2 .order() ) by A1, GLIBPRE0: 57;

      

       A7: (v1 .degree() ) = ((v0 .degree() ) +` 1) by A1, A5, GLIBPRE0: 59;

      per cases ;

        suppose

         A8: ((v0 .degree() ) +` 1) c= (v9 .degree() );

        then

         A9: (((G2 .minDegree() ) +` 1) /\ (G2 .order() )) = ((v0 .degree() ) +` 1) by A2, A6, XBOOLE_1: 28;

        now

          let w be Vertex of G1;

          per cases by A4, XBOOLE_0:def 3;

            suppose w in ( the_Vertices_of G2);

            then

            reconsider w0 = w as Vertex of G2;

            (v0 .degree() ) c= (w0 .degree() ) & 1 c= 1 by A3;

            then (v1 .degree() ) c= ((w0 .degree() ) +` 1) by A7, CARD_2: 83;

            hence (v1 .degree() ) c= (w .degree() ) by A1, A5, GLIBPRE0: 59;

          end;

            suppose w in {v};

            hence (v1 .degree() ) c= (w .degree() ) by A7, A8, TARSKI:def 1;

          end;

        end;

        hence thesis by A7, A9, Th36;

      end;

        suppose

         A10: (v9 .degree() ) c= ((v0 .degree() ) +` 1);

        then

         A11: (((G2 .minDegree() ) +` 1) /\ (G2 .order() )) = (v9 .degree() ) by A2, A6, XBOOLE_1: 28;

        now

          let w be Vertex of G1;

          per cases by A4, XBOOLE_0:def 3;

            suppose w in ( the_Vertices_of G2);

            then

            reconsider w0 = w as Vertex of G2;

            (v0 .degree() ) c= (w0 .degree() ) & 1 c= 1 by A3;

            then ((v0 .degree() ) +` 1) c= ((w0 .degree() ) +` 1) by CARD_2: 83;

            then (v9 .degree() ) c= ((w0 .degree() ) +` 1) by A10, XBOOLE_1: 1;

            hence (v9 .degree() ) c= (w .degree() ) by A1, A5, GLIBPRE0: 59;

          end;

            suppose w in {v};

            hence (v9 .degree() ) c= (w .degree() ) by TARSKI:def 1;

          end;

        end;

        hence thesis by A11, Th36;

      end;

    end;

    theorem :: GLIB_013:77

    for G2 be _finite _Graph, v be object holds for G1 be addAdjVertexAll of G2, v st not v in ( the_Vertices_of G2) holds (G1 .minDegree() ) = ( min (((G2 .minDegree() ) + 1),(G2 .order() )))

    proof

      let G2 be _finite _Graph, v be object;

      let G1 be addAdjVertexAll of G2, v;

      ( min (((G2 .minDegree() ) + 1),(G2 .order() ))) = (((G2 .minDegree() ) +` 1) /\ (G2 .order() ));

      hence thesis by Th76;

    end;

    

     Lm2: for a,b,c be Cardinal st c c= a & c c= b & a in (c +` 2) & not a c= b holds b = c

    proof

      let a,b,c be Cardinal;

      assume

       A1: c c= a & c c= b & a in (c +` 2) & not a c= b;

      

       A2: a is finite

      proof

        assume

         A3: a is infinite;

        a c= (c +` 2) by A1, ORDINAL1:def 2;

        then

         A4: c is infinite by A3;

        then 2 c= c;

        then (c +` 2) = c by A4, CARD_2: 76;

        then a in a by A1;

        hence contradiction;

      end;

      then

      reconsider k = a as Nat;

      reconsider n = c as Nat by A1, A2;

      

       A5: b in a by A1, ORDINAL1: 16;

      then b c= a by ORDINAL1:def 2;

      then

      reconsider m = b as Nat by A2;

      ( Segm c) c= ( Segm b) by A1;

      then

       A6: n <= m by NAT_1: 39;

      a in ( Segm (n +` 2)) by A1;

      then

       A7: k < (n + 2) by NAT_1: 44;

      b in ( Segm a) by A5;

      then m < k by NAT_1: 44;

      then

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

      k < ((n + 1) + 1) by A7;

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

      then (m + 1) <= (n + 1) by A8, XXREAL_0: 2;

      then m <= n by XREAL_1: 6;

      hence thesis by A6, XXREAL_0: 1;

    end;

    theorem :: GLIB_013:78

    for G2 be _Graph, V be set, G1 be addLoops of G2, V holds (G1 .minDegree() ) c= ((G2 .minDegree() ) +` 2)

    proof

      let G2 be _Graph, V be set, G1 be addLoops of G2, V;

      per cases ;

        suppose

         A1: V c= ( the_Vertices_of G2);

        consider v2 be Vertex of G2 such that

         A2: (G2 .minDegree() ) = (v2 .degree() ) and

         A3: for w2 be Vertex of G2 holds (v2 .degree() ) c= (w2 .degree() ) by Th36;

        

         A4: ( the_Vertices_of G1) = ( the_Vertices_of G2) by A1, GLIB_012:def 5;

        then

        reconsider v1 = v2 as Vertex of G1;

        per cases ;

          suppose not v2 in V;

          then

           A5: (v1 .degree() ) = (v2 .degree() ) by A1, GLIB_012: 44;

          now

            let w1 be Vertex of G1;

            reconsider w2 = w1 as Vertex of G2 by A4;

            per cases ;

              suppose w1 in V;

              then

               A6: (w1 .degree() ) = ((w2 .degree() ) +` 2) by A1, GLIB_012: 43;

              

               A7: (v1 .degree() ) c= (w2 .degree() ) by A3, A5;

              (w2 .degree() ) c= (w1 .degree() ) by A6, CARD_2: 94;

              hence (v1 .degree() ) c= (w1 .degree() ) by A7, XBOOLE_1: 1;

            end;

              suppose not w1 in V;

              then (w1 .degree() ) = (w2 .degree() ) by A1, GLIB_012: 44;

              hence (v1 .degree() ) c= (w1 .degree() ) by A3, A5;

            end;

          end;

          then (G1 .minDegree() ) = (v1 .degree() ) by Th36;

          hence thesis by A2, A5, CARD_2: 94;

        end;

          suppose

           A8: v2 in V & for w2 be Vertex of G2 st not w2 in V holds ((v2 .degree() ) +` 2) c= (w2 .degree() );

          then

           A9: (v1 .degree() ) = ((v2 .degree() ) +` 2) by A1, GLIB_012: 43;

          now

            let w1 be Vertex of G1;

            reconsider w2 = w1 as Vertex of G2 by A4;

            per cases ;

              suppose w1 in V;

              then

               A10: (w1 .degree() ) = ((w2 .degree() ) +` 2) by A1, GLIB_012: 43;

              (v2 .degree() ) c= (w2 .degree() ) & 2 c= 2 by A3;

              hence (v1 .degree() ) c= (w1 .degree() ) by A9, A10, CARD_2: 83;

            end;

              suppose

               A11: not w1 in V;

              then (w1 .degree() ) = (w2 .degree() ) by A1, GLIB_012: 44;

              hence (v1 .degree() ) c= (w1 .degree() ) by A8, A9, A11;

            end;

          end;

          hence thesis by A2, A9, Th36;

        end;

          suppose v2 in V & ex w2 be Vertex of G2 st not w2 in V & not ((v2 .degree() ) +` 2) c= (w2 .degree() );

          then

          consider w2 be Vertex of G2 such that

           A12: not w2 in V & not ((v2 .degree() ) +` 2) c= (w2 .degree() );

          

           A13: (w2 .degree() ) in ((v2 .degree() ) +` 2) by A12, ORDINAL1: 16;

          reconsider w1 = w2 as Vertex of G1 by A4;

          

           A14: (w1 .degree() ) = (w2 .degree() ) by A1, A12, GLIB_012: 44;

          per cases ;

            suppose

             A15: for u2 be Vertex of G2 holds not u2 in V implies (w2 .degree() ) c= (u2 .degree() );

            now

              let u1 be Vertex of G1;

              reconsider u2 = u1 as Vertex of G2 by A4;

              per cases ;

                suppose u1 in V;

                then

                 A16: (u1 .degree() ) = ((u2 .degree() ) +` 2) by A1, GLIB_012: 43;

                (v2 .degree() ) c= (u2 .degree() ) & 2 c= 2 by A3;

                then ((v2 .degree() ) +` 2) c= ((u2 .degree() ) +` 2) by CARD_2: 83;

                hence (w1 .degree() ) c= (u1 .degree() ) by A13, A14, A16, ORDINAL1:def 2;

              end;

                suppose not u1 in V;

                then (u1 .degree() ) = (u2 .degree() ) & (w2 .degree() ) c= (u2 .degree() ) by A1, A15, GLIB_012: 44;

                hence (w1 .degree() ) c= (u1 .degree() ) by A14;

              end;

            end;

            then (G1 .minDegree() ) = (w1 .degree() ) by Th36;

            hence thesis by A2, A13, A14, ORDINAL1:def 2;

          end;

            suppose ex u2 be Vertex of G2 st not u2 in V & not (w2 .degree() ) c= (u2 .degree() );

            then

            consider u2 be Vertex of G2 such that

             A17: not u2 in V & not (w2 .degree() ) c= (u2 .degree() );

            (v2 .degree() ) c= (w2 .degree() ) & (v2 .degree() ) c= (u2 .degree() ) by A3;

            then

             A18: (u2 .degree() ) = (v2 .degree() ) by A13, A17, Lm2;

            reconsider u1 = u2 as Vertex of G1 by A4;

            

             A19: (u1 .degree() ) = (u2 .degree() ) by A1, A17, GLIB_012: 44;

            now

              let x1 be Vertex of G1;

              reconsider x2 = x1 as Vertex of G2 by A4;

              

               A20: (u1 .degree() ) c= (x2 .degree() ) by A3, A18, A19;

              per cases ;

                suppose x1 in V;

                then (x1 .degree() ) = ((x2 .degree() ) +` 2) by A1, GLIB_012: 43;

                then (x2 .degree() ) c= (x1 .degree() ) by CARD_2: 94;

                hence (u1 .degree() ) c= (x1 .degree() ) by A20, XBOOLE_1: 1;

              end;

                suppose not x1 in V;

                hence (u1 .degree() ) c= (x1 .degree() ) by A1, A20, GLIB_012: 44;

              end;

            end;

            then

             A21: (G1 .minDegree() ) = (u1 .degree() ) by Th36;

            (u1 .degree() ) in (w2 .degree() ) by A17, A19, ORDINAL1: 16;

            hence thesis by A2, A13, A21;

          end;

        end;

      end;

        suppose not (V c= ( the_Vertices_of G2));

        then G1 == G2 by GLIB_012:def 5;

        then (G1 .minDegree() ) = (G2 .minDegree() ) by Th62;

        hence thesis by CARD_2: 94;

      end;

    end;

    registration

      let G be edge-finite _Graph;

      cluster (G .supDegree() ) -> natural;

      coherence

      proof

        now

          let d be set;

          assume d in the set of all (v .degree() ) where v be Vertex of G;

          then

          consider v be Vertex of G such that

           A1: d = (v .degree() );

          ( card (v .edgesIn() )) c= ( card ( the_Edges_of G)) & ( card (v .edgesOut() )) c= ( card ( the_Edges_of G)) by CARD_1: 11;

          hence d c= ((G .size() ) +` (G .size() )) by A1, CARD_2: 83;

        end;

        then (G .supDegree() ) c= ((G .size() ) +` (G .size() )) by ZFMISC_1: 76;

        hence thesis;

      end;

      cluster (G .supInDegree() ) -> natural;

      coherence

      proof

        now

          let d be set;

          assume d in the set of all (v .inDegree() ) where v be Vertex of G;

          then

          consider v be Vertex of G such that

           A2: d = (v .inDegree() );

          thus d c= (G .size() ) by A2, CARD_1: 11;

        end;

        then (G .supInDegree() ) c= (G .size() ) by ZFMISC_1: 76;

        hence thesis;

      end;

      cluster (G .supOutDegree() ) -> natural;

      coherence

      proof

        now

          let d be set;

          assume d in the set of all (v .outDegree() ) where v be Vertex of G;

          then

          consider v be Vertex of G such that

           A3: d = (v .outDegree() );

          thus d c= (G .size() ) by A3, CARD_1: 11;

        end;

        then (G .supOutDegree() ) c= (G .size() ) by ZFMISC_1: 76;

        hence thesis;

      end;

    end

    definition

      let G be edge-finite _Graph;

      :: original: .supDegree()

      redefine

      func G .supDegree() -> Nat ;

      coherence ;

      :: original: .supInDegree()

      redefine

      func G .supInDegree() -> Nat ;

      coherence ;

      :: original: .supOutDegree()

      redefine

      func G .supOutDegree() -> Nat ;

      coherence ;

    end

    definition

      let G be _Graph;

      :: GLIB_013:def12

      attr G is with_max_degree means

      : Def12: ex v be Vertex of G st for w be Vertex of G holds (w .degree() ) c= (v .degree() );

      :: GLIB_013:def13

      attr G is with_max_in_degree means

      : Def13: ex v be Vertex of G st for w be Vertex of G holds (w .inDegree() ) c= (v .inDegree() );

      :: GLIB_013:def14

      attr G is with_max_out_degree means

      : Def14: ex v be Vertex of G st for w be Vertex of G holds (w .outDegree() ) c= (v .outDegree() );

    end

    theorem :: GLIB_013:79

    

     Th79: for G be _Graph st G is with_max_degree holds ex v be Vertex of G st (v .degree() ) = (G .supDegree() ) & for w be Vertex of G holds (w .degree() ) c= (v .degree() )

    proof

      let G be _Graph;

      assume G is with_max_degree;

      then

      consider v be Vertex of G such that

       A1: for w be Vertex of G holds (w .degree() ) c= (v .degree() );

      take v;

      set D = the set of all (w .degree() ) where w be Vertex of G;

      now

        let X be set;

        assume X in D;

        then

        consider w be Vertex of G such that

         A2: X = (w .degree() );

        thus X c= (v .degree() ) by A1, A2;

      end;

      then

       A3: ( union D) c= (v .degree() ) by ZFMISC_1: 76;

      (v .degree() ) c= (G .supDegree() ) by Th35;

      hence thesis by A1, A3, XBOOLE_0:def 10;

    end;

    theorem :: GLIB_013:80

    

     Th80: for G be _Graph st G is with_max_in_degree holds ex v be Vertex of G st (v .inDegree() ) = (G .supInDegree() ) & for w be Vertex of G holds (w .inDegree() ) c= (v .inDegree() )

    proof

      let G be _Graph;

      assume G is with_max_in_degree;

      then

      consider v be Vertex of G such that

       A1: for w be Vertex of G holds (w .inDegree() ) c= (v .inDegree() );

      take v;

      set D = the set of all (w .inDegree() ) where w be Vertex of G;

      now

        let X be set;

        assume X in D;

        then

        consider w be Vertex of G such that

         A2: X = (w .inDegree() );

        thus X c= (v .inDegree() ) by A1, A2;

      end;

      then

       A3: ( union D) c= (v .inDegree() ) by ZFMISC_1: 76;

      (v .inDegree() ) c= (G .supInDegree() ) by Th35;

      hence thesis by A1, A3, XBOOLE_0:def 10;

    end;

    theorem :: GLIB_013:81

    

     Th81: for G be _Graph st G is with_max_out_degree holds ex v be Vertex of G st (v .outDegree() ) = (G .supOutDegree() ) & for w be Vertex of G holds (w .outDegree() ) c= (v .outDegree() )

    proof

      let G be _Graph;

      assume G is with_max_out_degree;

      then

      consider v be Vertex of G such that

       A1: for w be Vertex of G holds (w .outDegree() ) c= (v .outDegree() );

      take v;

      set D = the set of all (w .outDegree() ) where w be Vertex of G;

      now

        let X be set;

        assume X in D;

        then

        consider w be Vertex of G such that

         A2: X = (w .outDegree() );

        thus X c= (v .outDegree() ) by A1, A2;

      end;

      then

       A3: ( union D) c= (v .outDegree() ) by ZFMISC_1: 76;

      (v .outDegree() ) c= (G .supOutDegree() ) by Th35;

      hence thesis by A1, A3, XBOOLE_0:def 10;

    end;

    

     Lm3: for G be _Graph st ex v be Vertex of G st (v .degree() ) = (G .supDegree() ) holds G is with_max_degree

    proof

      let G be _Graph;

      given v be Vertex of G such that

       A1: (v .degree() ) = (G .supDegree() );

      for w be Vertex of G holds (w .degree() ) c= (v .degree() ) by A1, Th35;

      hence thesis;

    end;

    

     Lm4: for G be _Graph st ex v be Vertex of G st (v .inDegree() ) = (G .supInDegree() ) holds G is with_max_in_degree

    proof

      let G be _Graph;

      given v be Vertex of G such that

       A1: (v .inDegree() ) = (G .supInDegree() );

      for w be Vertex of G holds (w .inDegree() ) c= (v .inDegree() ) by A1, Th35;

      hence thesis;

    end;

    

     Lm5: for G be _Graph st ex v be Vertex of G st (v .outDegree() ) = (G .supOutDegree() ) holds G is with_max_out_degree

    proof

      let G be _Graph;

      given v be Vertex of G such that

       A1: (v .outDegree() ) = (G .supOutDegree() );

      for w be Vertex of G holds (w .outDegree() ) c= (v .outDegree() ) by A1, Th35;

      hence thesis;

    end;

    notation

      let G be _Graph;

      antonym G is without_max_degree for G is with_max_degree;

      antonym G is without_max_in_degree for G is with_max_in_degree;

      antonym G is without_max_out_degree for G is with_max_out_degree;

    end

    registration

      cluster with_max_in_degree with_max_out_degree -> with_max_degree for _Graph;

      coherence

      proof

        let G be _Graph;

        assume G is with_max_in_degree;

        then

        consider v be Vertex of G such that

         A1: (v .inDegree() ) = (G .supInDegree() ) and

         A2: for u be Vertex of G holds (u .inDegree() ) c= (v .inDegree() ) by Th80;

        assume G is with_max_out_degree;

        then

        consider w be Vertex of G such that

         A3: (w .outDegree() ) = (G .supOutDegree() ) and

         A4: for u be Vertex of G holds (u .outDegree() ) c= (w .outDegree() ) by Th81;

        set c = (G .supInDegree() ), d = (G .supOutDegree() );

        per cases ;

          suppose

           A5: d is infinite & c c= d;

          (w .inDegree() ) c= c by A1, A2;

          then ((w .inDegree() ) +` (w .outDegree() )) c= (c +` (w .outDegree() )) by CARD_2: 83;

          then

           A6: (w .degree() ) c= d by A3, A5, CARD_2: 76;

          d c= (w .degree() ) by A3, CARD_2: 94;

          then

           A7: (w .degree() ) = d by A6, XBOOLE_0:def 10;

          now

            let u be Vertex of G;

            (u .inDegree() ) c= (v .inDegree() ) by A2;

            then

             A8: (u .inDegree() ) c= d by A1, A5, XBOOLE_1: 1;

            (u .outDegree() ) c= d by A3, A4;

            then (u .degree() ) c= (d +` d) by A8, CARD_2: 83;

            hence (u .degree() ) c= (w .degree() ) by A5, A7, CARD_2: 75;

          end;

          hence thesis;

        end;

          suppose

           A9: c is infinite & d c= c;

          (v .outDegree() ) c= d by A3, A4;

          then ((v .inDegree() ) +` (v .outDegree() )) c= (d +` (v .inDegree() )) by CARD_2: 83;

          then

           A10: (v .degree() ) c= c by A1, A9, CARD_2: 76;

          c c= (v .degree() ) by A1, CARD_2: 94;

          then

           A11: (v .degree() ) = c by A10, XBOOLE_0:def 10;

          now

            let u be Vertex of G;

            

             A12: (u .inDegree() ) c= (v .inDegree() ) by A2;

            (u .outDegree() ) c= d by A3, A4;

            then (u .outDegree() ) c= c by A9, XBOOLE_1: 1;

            then (u .degree() ) c= (c +` c) by A1, A12, CARD_2: 83;

            hence (u .degree() ) c= (v .degree() ) by A9, A11, CARD_2: 75;

          end;

          hence thesis;

        end;

          suppose c is finite & d is finite;

          then

          reconsider c, d as Nat;

          defpred P[ Nat] means ex u be Vertex of G st (u .degree() ) = $1;

          

           A13: for k be Nat st P[k] holds k <= (c + d)

          proof

            let k be Nat;

            given u be Vertex of G such that

             A14: (u .degree() ) = k;

            (u .inDegree() ) c= c & (u .outDegree() ) c= d by A1, A2, A3, A4;

            then (u .degree() ) c= (c +` d) by CARD_2: 83;

            then ( Segm (u .degree() )) c= ( Segm (c + d));

            hence thesis by A14, NAT_1: 39;

          end;

          

           A15: ex k be Nat st P[k]

          proof

            (w .inDegree() ) c= c by A1, A2;

            then

            reconsider e = (w .inDegree() ) as Nat;

            take (e + d), w;

            

            thus (w .degree() ) = (e +` d) by A3

            .= (e + d);

          end;

          consider k be Nat such that

           A16: P[k] & for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A13, A15);

          consider u be Vertex of G such that

           A17: (u .degree() ) = k by A16;

          now

            let u9 be Vertex of G;

            (u9 .inDegree() ) c= c & (u9 .outDegree() ) c= d by A1, A2, A3, A4;

            then

            reconsider n = (u9 .degree() ) as Nat;

            ( Segm n) c= ( Segm k) by A16, NAT_1: 39;

            hence (u9 .degree() ) c= (u .degree() ) by A17;

          end;

          hence thesis;

        end;

      end;

      cluster vertex-finite -> with_max_degree with_max_in_degree with_max_out_degree for _Graph;

      coherence

      proof

        let G be _Graph;

        assume

         A18: G is vertex-finite;

        thus G is with_max_degree

        proof

          set D = the set of all (v .degree() ) where v be Vertex of G;

          deffunc F( object) = (( In ($1,( the_Vertices_of G))) .degree() );

          consider f be Function such that

           A19: ( dom f) = ( the_Vertices_of G) and

           A20: for x be object st x in ( the_Vertices_of G) holds (f . x) = F(x) from FUNCT_1:sch 3;

          now

            let y be object;

            hereby

              assume y in ( rng f);

              then

              consider x be object such that

               A21: x in ( dom f) & (f . x) = y by FUNCT_1:def 3;

              reconsider v = x as Vertex of G by A19, A21;

              y = (( In (x,( the_Vertices_of G))) .degree() ) by A19, A20, A21

              .= (v .degree() ) by SUBSET_1:def 8;

              hence y in D;

            end;

            assume y in D;

            then

            consider v be Vertex of G such that

             A22: y = (v .degree() );

            y = (( In (v,( the_Vertices_of G))) .degree() ) by A22, SUBSET_1:def 8

            .= (f . v) by A20;

            hence y in ( rng f) by A19, FUNCT_1: 3;

          end;

          then ( rng f) = D by TARSKI: 2;

          then

           A23: D is finite by A18, A19, FINSET_1: 8;

          now

            let x,y be set;

            assume

             A24: x in D & y in D;

            then

            consider v be Vertex of G such that

             A25: x = (v .degree() );

            consider w be Vertex of G such that

             A26: y = (w .degree() ) by A24;

            thus (x,y) are_c=-comparable by A25, A26, ORDINAL1: 15;

          end;

          then

           A27: D is finite c=-linear by A23, ORDINAL1:def 8;

          then

           A28: ( InclPoset D) is connected transitive;

          set B = ( [#] ( InclPoset D));

          ( the Vertex of G .degree() ) in D;

          then

           A29: B is non empty finite by A27;

          then

          consider x be Element of ( InclPoset D) such that x in B and

           A30: for y be Element of ( InclPoset D) st y in B & x <> y holds y <= x by A28, ORDERS_5: 25;

          

           A31: x in D by A29;

          then

          consider v be Vertex of G such that

           A32: x = (v .degree() );

          now

            let w be Vertex of G;

            (w .degree() ) in the carrier of ( InclPoset D);

            then

            reconsider y = (w .degree() ) as Element of ( InclPoset D);

            per cases ;

              suppose

               A33: x <> y;

              y in B;

              then [y, x] in ( RelIncl D) by A30, A33, ORDERS_2:def 5;

              hence (w .degree() ) c= (v .degree() ) by A31, A32, WELLORD2:def 1;

            end;

              suppose x = y;

              hence (w .degree() ) c= (v .degree() ) by A32;

            end;

          end;

          hence G is with_max_degree;

        end;

        thus G is with_max_in_degree

        proof

          set D = the set of all (v .inDegree() ) where v be Vertex of G;

          deffunc F( object) = (( In ($1,( the_Vertices_of G))) .inDegree() );

          consider f be Function such that

           A34: ( dom f) = ( the_Vertices_of G) and

           A35: for x be object st x in ( the_Vertices_of G) holds (f . x) = F(x) from FUNCT_1:sch 3;

          now

            let y be object;

            hereby

              assume y in ( rng f);

              then

              consider x be object such that

               A36: x in ( dom f) & (f . x) = y by FUNCT_1:def 3;

              reconsider v = x as Vertex of G by A34, A36;

              y = (( In (x,( the_Vertices_of G))) .inDegree() ) by A34, A35, A36

              .= (v .inDegree() ) by SUBSET_1:def 8;

              hence y in D;

            end;

            assume y in D;

            then

            consider v be Vertex of G such that

             A37: y = (v .inDegree() );

            y = (( In (v,( the_Vertices_of G))) .inDegree() ) by A37, SUBSET_1:def 8

            .= (f . v) by A35;

            hence y in ( rng f) by A34, FUNCT_1: 3;

          end;

          then ( rng f) = D by TARSKI: 2;

          then

           A38: D is finite by A18, A34, FINSET_1: 8;

          now

            let x,y be set;

            assume

             A39: x in D & y in D;

            then

            consider v be Vertex of G such that

             A40: x = (v .inDegree() );

            consider w be Vertex of G such that

             A41: y = (w .inDegree() ) by A39;

            thus (x,y) are_c=-comparable by A40, A41, ORDINAL1: 15;

          end;

          then

           A42: D is finite c=-linear by A38, ORDINAL1:def 8;

          then

           A43: ( InclPoset D) is connected transitive;

          set B = ( [#] ( InclPoset D));

          ( the Vertex of G .inDegree() ) in D;

          then

           A44: B is non empty finite by A42;

          then

          consider x be Element of ( InclPoset D) such that x in B and

           A45: for y be Element of ( InclPoset D) st y in B & x <> y holds y <= x by A43, ORDERS_5: 25;

          

           A46: x in D by A44;

          then

          consider v be Vertex of G such that

           A47: x = (v .inDegree() );

          now

            let w be Vertex of G;

            (w .inDegree() ) in the carrier of ( InclPoset D);

            then

            reconsider y = (w .inDegree() ) as Element of ( InclPoset D);

            per cases ;

              suppose

               A48: x <> y;

              y in B;

              then [y, x] in ( RelIncl D) by A45, A48, ORDERS_2:def 5;

              hence (w .inDegree() ) c= (v .inDegree() ) by A46, A47, WELLORD2:def 1;

            end;

              suppose x = y;

              hence (w .inDegree() ) c= (v .inDegree() ) by A47;

            end;

          end;

          hence G is with_max_in_degree;

        end;

        thus G is with_max_out_degree

        proof

          set D = the set of all (v .outDegree() ) where v be Vertex of G;

          deffunc F( object) = (( In ($1,( the_Vertices_of G))) .outDegree() );

          consider f be Function such that

           A49: ( dom f) = ( the_Vertices_of G) and

           A50: for x be object st x in ( the_Vertices_of G) holds (f . x) = F(x) from FUNCT_1:sch 3;

          now

            let y be object;

            hereby

              assume y in ( rng f);

              then

              consider x be object such that

               A51: x in ( dom f) & (f . x) = y by FUNCT_1:def 3;

              reconsider v = x as Vertex of G by A49, A51;

              y = (( In (x,( the_Vertices_of G))) .outDegree() ) by A49, A50, A51

              .= (v .outDegree() ) by SUBSET_1:def 8;

              hence y in D;

            end;

            assume y in D;

            then

            consider v be Vertex of G such that

             A52: y = (v .outDegree() );

            y = (( In (v,( the_Vertices_of G))) .outDegree() ) by A52, SUBSET_1:def 8

            .= (f . v) by A50;

            hence y in ( rng f) by A49, FUNCT_1: 3;

          end;

          then ( rng f) = D by TARSKI: 2;

          then

           A53: D is finite by A18, A49, FINSET_1: 8;

          now

            let x,y be set;

            assume

             A54: x in D & y in D;

            then

            consider v be Vertex of G such that

             A55: x = (v .outDegree() );

            consider w be Vertex of G such that

             A56: y = (w .outDegree() ) by A54;

            thus (x,y) are_c=-comparable by A55, A56, ORDINAL1: 15;

          end;

          then

           A57: D is finite c=-linear by A53, ORDINAL1:def 8;

          then

           A58: ( InclPoset D) is connected transitive;

          set B = ( [#] ( InclPoset D));

          ( the Vertex of G .outDegree() ) in D;

          then

           A59: B is non empty finite by A57;

          then

          consider x be Element of ( InclPoset D) such that x in B and

           A60: for y be Element of ( InclPoset D) st y in B & x <> y holds y <= x by A58, ORDERS_5: 25;

          

           A61: x in D by A59;

          then

          consider v be Vertex of G such that

           A62: x = (v .outDegree() );

          now

            let w be Vertex of G;

            (w .outDegree() ) in the carrier of ( InclPoset D);

            then

            reconsider y = (w .outDegree() ) as Element of ( InclPoset D);

            per cases ;

              suppose

               A63: x <> y;

              y in B;

              then [y, x] in ( RelIncl D) by A60, A63, ORDERS_2:def 5;

              hence (w .outDegree() ) c= (v .outDegree() ) by A61, A62, WELLORD2:def 1;

            end;

              suppose x = y;

              hence (w .outDegree() ) c= (v .outDegree() ) by A62;

            end;

          end;

          hence G is with_max_out_degree;

        end;

      end;

      cluster edge-finite -> with_max_degree with_max_in_degree with_max_out_degree for _Graph;

      coherence

      proof

        let G be _Graph;

        assume

         A64: G is edge-finite;

        then

        reconsider m = (G .size() ) as Nat;

        now

          defpred P[ Nat] means ex u be Vertex of G st (u .degree() ) = $1;

          

           A65: for k be Nat st P[k] holds k <= (2 * m)

          proof

            let k be Nat;

            given u be Vertex of G such that

             A66: (u .degree() ) = k;

            (u .inDegree() ) c= (G .size() ) & (u .outDegree() ) c= (G .size() ) by CARD_1: 11;

            then ( Segm (u .degree() )) c= (m +` m) by CARD_2: 83;

            then ( Segm (u .degree() )) c= ( Segm (2 * m));

            hence thesis by A66, NAT_1: 39;

          end;

          

           A67: ex k be Nat st P[k]

          proof

            set v = the Vertex of G;

            reconsider d = (v .degree() ) as Nat by A64;

            take d, v;

            thus thesis;

          end;

          consider k be Nat such that

           A68: P[k] & for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A65, A67);

          consider u be Vertex of G such that

           A69: (u .degree() ) = k by A68;

          take u;

          let w be Vertex of G;

          reconsider d = (w .degree() ) as Nat by A64;

          ( Segm d) c= ( Segm k) by A68, NAT_1: 39;

          hence (w .degree() ) c= (u .degree() ) by A69;

        end;

        hence G is with_max_degree;

        now

          defpred P[ Nat] means ex u be Vertex of G st (u .inDegree() ) = $1;

          

           A70: for k be Nat st P[k] holds k <= m

          proof

            let k be Nat;

            given u be Vertex of G such that

             A71: (u .inDegree() ) = k;

            ( Segm (u .inDegree() )) c= ( Segm m) by CARD_1: 11;

            hence thesis by A71, NAT_1: 39;

          end;

          

           A72: ex k be Nat st P[k]

          proof

            set v = the Vertex of G;

            reconsider d = (v .inDegree() ) as Nat by A64;

            take d, v;

            thus thesis;

          end;

          consider k be Nat such that

           A73: P[k] & for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A70, A72);

          consider u be Vertex of G such that

           A74: (u .inDegree() ) = k by A73;

          take u;

          let w be Vertex of G;

          reconsider d = (w .inDegree() ) as Nat by A64;

          ( Segm d) c= ( Segm k) by A73, NAT_1: 39;

          hence (w .inDegree() ) c= (u .inDegree() ) by A74;

        end;

        hence G is with_max_in_degree;

        now

          defpred P[ Nat] means ex u be Vertex of G st (u .outDegree() ) = $1;

          

           A75: for k be Nat st P[k] holds k <= m

          proof

            let k be Nat;

            given u be Vertex of G such that

             A76: (u .outDegree() ) = k;

            ( Segm (u .outDegree() )) c= ( Segm m) by CARD_1: 11;

            hence thesis by A76, NAT_1: 39;

          end;

          

           A77: ex k be Nat st P[k]

          proof

            set v = the Vertex of G;

            reconsider d = (v .outDegree() ) as Nat by A64;

            take d, v;

            thus thesis;

          end;

          consider k be Nat such that

           A78: P[k] & for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A75, A77);

          consider u be Vertex of G such that

           A79: (u .outDegree() ) = k by A78;

          take u;

          let w be Vertex of G;

          reconsider d = (w .outDegree() ) as Nat by A64;

          ( Segm d) c= ( Segm k) by A78, NAT_1: 39;

          hence (w .outDegree() ) c= (u .outDegree() ) by A79;

        end;

        hence G is with_max_out_degree;

      end;

    end

    theorem :: GLIB_013:82

    for G be with_max_degree _Graph holds G is with_max_in_degree or G is with_max_out_degree

    proof

      let G be with_max_degree _Graph;

      consider v be Vertex of G such that

       A1: (v .degree() ) = (G .supDegree() ) and for w be Vertex of G holds (w .degree() ) c= (v .degree() ) by Th79;

      set a = (v .inDegree() ), b = (v .outDegree() );

      per cases ;

        suppose a c= b & b is infinite;

        then (v .degree() ) = b by CARD_2: 76;

        then

         A2: (G .supOutDegree() ) c= (v .outDegree() ) by A1, Th40;

        (v .outDegree() ) c= (G .supOutDegree() ) by Th35;

        hence thesis by A2, Lm5, XBOOLE_0:def 10;

      end;

        suppose b c= a & a is infinite;

        then (v .degree() ) = a by CARD_2: 76;

        then

         A3: (G .supInDegree() ) c= (v .inDegree() ) by A1, Th39;

        (v .inDegree() ) c= (G .supInDegree() ) by Th35;

        hence thesis by A3, Lm4, XBOOLE_0:def 10;

      end;

        suppose a is finite & b is finite;

        then

        reconsider a, b as Nat;

        now

          defpred P[ Nat] means ex u be Vertex of G st (u .inDegree() ) = $1;

          

           A4: for k be Nat st P[k] holds k <= (a + b)

          proof

            let k be Nat;

            given u be Vertex of G such that

             A5: (u .inDegree() ) = k;

            

             A6: (u .inDegree() ) c= (G .supInDegree() ) by Th35;

            (G .supInDegree() ) c= (G .supDegree() ) by Th39;

            then ( Segm (u .inDegree() )) c= ( Segm (a +` b)) by A1, A6, XBOOLE_1: 1;

            hence thesis by A5, NAT_1: 39;

          end;

          

           A7: ex k be Nat st P[k]

          proof

            take a, v;

            thus thesis;

          end;

          consider k be Nat such that

           A8: P[k] & for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A4, A7);

          consider u be Vertex of G such that

           A9: (u .inDegree() ) = k by A8;

          take u;

          let w be Vertex of G;

          

           A10: (w .inDegree() ) c= (G .supInDegree() ) by Th35;

          (G .supInDegree() ) c= (G .supDegree() ) by Th39;

          then (w .inDegree() ) c= (a +` b) by A1, A10, XBOOLE_1: 1;

          then

          reconsider d = (w .inDegree() ) as Nat;

          ( Segm d) c= ( Segm k) by A8, NAT_1: 39;

          hence (w .inDegree() ) c= (u .inDegree() ) by A9;

        end;

        hence thesis;

      end;

    end;

    notation

      let G be with_max_degree _Graph;

      synonym G .maxDegree() for G .supDegree() ;

    end

    notation

      let G be with_max_in_degree _Graph;

      synonym G .maxInDegree() for G .supInDegree() ;

    end

    notation

      let G be with_max_out_degree _Graph;

      synonym G .maxOutDegree() for G .supOutDegree() ;

    end

    registration

      let G be locally-finite with_max_degree _Graph;

      cluster (G .maxDegree() ) -> natural;

      coherence

      proof

        consider v be Vertex of G such that

         A1: (v .degree() ) = (G .supDegree() ) and for w be Vertex of G holds (w .degree() ) c= (v .degree() ) by Th79;

        thus thesis by A1;

      end;

    end

    definition

      let G be locally-finite with_max_degree _Graph;

      :: original: .maxDegree()

      redefine

      func G .maxDegree() -> Nat ;

      coherence ;

    end

    registration

      let G be locally-finite with_max_in_degree _Graph;

      cluster (G .maxInDegree() ) -> natural;

      coherence

      proof

        consider v be Vertex of G such that

         A1: (v .inDegree() ) = (G .supInDegree() ) and for w be Vertex of G holds (w .inDegree() ) c= (v .inDegree() ) by Th80;

        thus thesis by A1;

      end;

    end

    definition

      let G be locally-finite with_max_in_degree _Graph;

      :: original: .maxInDegree()

      redefine

      func G .maxInDegree() -> Nat ;

      coherence ;

    end

    registration

      let G be locally-finite with_max_out_degree _Graph;

      cluster (G .maxOutDegree() ) -> natural;

      coherence

      proof

        consider v be Vertex of G such that

         A1: (v .outDegree() ) = (G .supOutDegree() ) and for w be Vertex of G holds (w .outDegree() ) c= (v .outDegree() ) by Th81;

        thus thesis by A1;

      end;

    end

    definition

      let G be locally-finite with_max_out_degree _Graph;

      :: original: .maxOutDegree()

      redefine

      func G .maxOutDegree() -> Nat ;

      coherence ;

    end

    theorem :: GLIB_013:83

    

     Th83: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is isomorphism holds G1 is with_max_degree iff G2 is with_max_degree

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is isomorphism;

      hereby

        assume G1 is with_max_degree;

        then

        consider v be Vertex of G1 such that

         A2: (v .degree() ) = (G1 .supDegree() ) and for w be Vertex of G1 holds (w .degree() ) c= (v .degree() ) by Th79;

        (v .degree() ) = (((F _V ) /. v) .degree() ) by A1, GLIBPRE0: 95;

        then (((F _V ) /. v) .degree() ) = (G2 .supDegree() ) by A1, A2, Th55;

        hence G2 is with_max_degree by Lm3;

      end;

      assume G2 is with_max_degree;

      then

      consider v be Vertex of G2 such that

       A3: (v .degree() ) = (G2 .supDegree() ) and for w be Vertex of G2 holds (w .degree() ) c= (v .degree() ) by Th79;

      ( rng (F _V )) = ( the_Vertices_of G2) by A1, GLIB_010:def 12;

      then

      consider v0 be object such that

       A4: v0 in ( dom (F _V )) & ((F _V ) . v0) = v by FUNCT_1:def 3;

      reconsider v0 as Vertex of G1 by A4;

      ((F _V ) /. v0) = v by A4, PARTFUN1:def 6;

      then (v .degree() ) = (v0 .degree() ) by A1, GLIBPRE0: 95;

      then (v0 .degree() ) = (G1 .supDegree() ) by A1, A3, Th55;

      hence thesis by Lm3;

    end;

    theorem :: GLIB_013:84

    

     Th84: for G1,G2 be _Graph, F be PGraphMapping of G1, G2 st F is Disomorphism holds (G1 is with_max_in_degree iff G2 is with_max_in_degree) & (G1 is with_max_out_degree iff G2 is with_max_out_degree)

    proof

      let G1,G2 be _Graph, F be PGraphMapping of G1, G2;

      assume

       A1: F is Disomorphism;

      hereby

        assume G1 is with_max_in_degree;

        then

        consider v be Vertex of G1 such that

         A2: (v .inDegree() ) = (G1 .supInDegree() ) and for w be Vertex of G1 holds (w .inDegree() ) c= (v .inDegree() ) by Th80;

        (v .inDegree() ) = (((F _V ) /. v) .inDegree() ) by A1, GLIBPRE0: 94;

        then (((F _V ) /. v) .inDegree() ) = (G2 .supInDegree() ) by A1, A2, Th60;

        hence G2 is with_max_in_degree by Lm4;

      end;

      hereby

        assume G2 is with_max_in_degree;

        then

        consider v be Vertex of G2 such that

         A3: (v .inDegree() ) = (G2 .supInDegree() ) and for w be Vertex of G2 holds (w .inDegree() ) c= (v .inDegree() ) by Th80;

        ( rng (F _V )) = ( the_Vertices_of G2) by A1, GLIB_010:def 12;

        then

        consider v0 be object such that

         A4: v0 in ( dom (F _V )) & ((F _V ) . v0) = v by FUNCT_1:def 3;

        reconsider v0 as Vertex of G1 by A4;

        ((F _V ) /. v0) = v by A4, PARTFUN1:def 6;

        then (v .inDegree() ) = (v0 .inDegree() ) by A1, GLIBPRE0: 94;

        then (v0 .inDegree() ) = (G1 .supInDegree() ) by A1, A3, Th60;

        hence G1 is with_max_in_degree by Lm4;

      end;

      hereby

        assume G1 is with_max_out_degree;

        then

        consider v be Vertex of G1 such that

         A5: (v .outDegree() ) = (G1 .supOutDegree() ) and for w be Vertex of G1 holds (w .outDegree() ) c= (v .outDegree() ) by Th81;

        (v .outDegree() ) = (((F _V ) /. v) .outDegree() ) by A1, GLIBPRE0: 94;

        then (((F _V ) /. v) .outDegree() ) = (G2 .supOutDegree() ) by A1, A5, Th60;

        hence G2 is with_max_out_degree by Lm5;

      end;

      hereby

        assume G2 is with_max_out_degree;

        then

        consider v be Vertex of G2 such that

         A6: (v .outDegree() ) = (G2 .supOutDegree() ) and for w be Vertex of G2 holds (w .outDegree() ) c= (v .outDegree() ) by Th81;

        ( rng (F _V )) = ( the_Vertices_of G2) by A1, GLIB_010:def 12;

        then

        consider v0 be object such that

         A7: v0 in ( dom (F _V )) & ((F _V ) . v0) = v by FUNCT_1:def 3;

        reconsider v0 as Vertex of G1 by A7;

        ((F _V ) /. v0) = v by A7, PARTFUN1:def 6;

        then (v .outDegree() ) = (v0 .outDegree() ) by A1, GLIBPRE0: 94;

        then (v0 .outDegree() ) = (G1 .supOutDegree() ) by A1, A6, Th60;

        hence G1 is with_max_out_degree by Lm5;

      end;

    end;

    theorem :: GLIB_013:85

    

     Th85: for G1,G2 be _Graph st G1 == G2 holds (G1 is with_max_degree implies G2 is with_max_degree) & (G1 is with_max_in_degree implies G2 is with_max_in_degree) & (G1 is with_max_out_degree implies G2 is with_max_out_degree)

    proof

      let G1,G2 be _Graph;

      assume G1 == G2;

      then

      consider F be PGraphMapping of G1, G2 such that

       A1: F = ( id G1) & F is Disomorphism by GLIBPRE0: 77;

      thus thesis by A1, Th83, Th84;

    end;

    theorem :: GLIB_013:86

    

     Th86: for G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E holds G1 is with_max_degree iff G2 is with_max_degree

    proof

      let G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E;

      consider F be PGraphMapping of G1, G2 such that

       A1: F = ( id G1) & F is isomorphism by GLIBPRE0: 79;

      thus thesis by A1, Th83;

    end;

    registration

      let G be with_max_degree _Graph, E be set;

      cluster -> with_max_degree for reverseEdgeDirections of G, E;

      coherence by Th86;

    end

    

     Lm6: for a,b,c be Cardinal st a c= c & b c= c & c c< (a +` 2) & not b c= a holds b = c

    proof

      let a,b,c be Cardinal;

      assume

       A1: a c= c & b c= c & c c< (a +` 2) & not b c= a;

      

       A2: c is finite

      proof

        assume c is infinite;

        then

         A3: a is infinite by A1, XBOOLE_0:def 8, FINSET_1: 1;

        then 2 c= a;

        then (a +` 2) = a by A3, CARD_2: 76;

        then c in a by A1, ORDINAL1: 11;

        then c in c by A1;

        hence contradiction;

      end;

      then

      reconsider n = c as Nat;

      reconsider k = a as Nat by A1, A2;

      

       A4: a in b by A1, ORDINAL1: 16;

      reconsider m = b as Nat by A1, A2;

      ( Segm b) c= ( Segm c) by A1;

      then

       A5: m <= n by NAT_1: 39;

      c in ( Segm (k +` 2)) by A1, ORDINAL1: 11;

      then

       A6: n < (k + 2) by NAT_1: 44;

      a in ( Segm b) by A4;

      then k < m by NAT_1: 44;

      then

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

      n < ((k + 1) + 1) by A6;

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

      then n <= m by A7, XXREAL_0: 2;

      hence thesis by A5, XXREAL_0: 1;

    end;

    registration

      let G be with_max_degree _Graph, V be set;

      cluster -> with_max_degree for addVertices of G, V;

      coherence

      proof

        let H be addVertices of G, V;

        consider v0 be Vertex of G such that

         A1: for w0 be Vertex of G holds (w0 .degree() ) c= (v0 .degree() ) by Def12;

        ( the_Vertices_of G) c= ( the_Vertices_of H) by GLIB_006:def 9;

        then

        reconsider v = v0 as Vertex of H by TARSKI:def 3;

        now

          let w be Vertex of H;

          per cases ;

            suppose w in ( the_Vertices_of G);

            then

            reconsider w0 = w as Vertex of G;

            (w .degree() ) = (w0 .degree() ) & (v .degree() ) = (v0 .degree() ) by GLIBPRE0: 47;

            hence (w .degree() ) c= (v .degree() ) by A1;

          end;

            suppose

             A2: not w in ( the_Vertices_of G);

            ( the_Vertices_of H) = (( the_Vertices_of G) \/ V) by GLIB_006:def 10;

            then w in V by A2, XBOOLE_0:def 3;

            then w in (V \ ( the_Vertices_of G)) by A2, XBOOLE_0:def 5;

            then (w .degree() ) = 0 by GLIB_006: 88, GLIBPRE0: 35;

            hence (w .degree() ) c= (v .degree() ) by XBOOLE_1: 2;

          end;

        end;

        hence thesis;

      end;

      cluster -> with_max_degree for addLoops of G, V;

      coherence

      proof

        let H be addLoops of G, V;

        per cases ;

          suppose

           A3: V c= ( the_Vertices_of G);

          consider v0 be Vertex of G such that

           A4: for w0 be Vertex of G holds (w0 .degree() ) c= (v0 .degree() ) by Def12;

          

           A5: ( the_Vertices_of G) = ( the_Vertices_of H) by A3, GLIB_012:def 5;

          then

          reconsider v = v0 as Vertex of H;

          per cases ;

            suppose v0 in V;

            then

             A6: (v .degree() ) = ((v0 .degree() ) +` 2) by A3, GLIB_012: 43;

            now

              let w be Vertex of H;

              reconsider w0 = w as Vertex of G by A5;

              per cases ;

                suppose w0 in V;

                then

                 A7: (w .degree() ) = ((w0 .degree() ) +` 2) by A3, GLIB_012: 43;

                (w0 .degree() ) c= (v0 .degree() ) & 2 c= 2 by A4;

                hence (w .degree() ) c= (v .degree() ) by A6, A7, CARD_2: 83;

              end;

                suppose not w0 in V;

                

                then

                 A8: (w .degree() ) = (w0 .degree() ) by A3, GLIB_012: 44

                .= ((w0 .degree() ) +` 0 ) by CARD_2: 18;

                (w0 .degree() ) c= (v0 .degree() ) & 0 c= 2 by A4, XBOOLE_1: 2;

                hence (w .degree() ) c= (v .degree() ) by A6, A8, CARD_2: 83;

              end;

            end;

            hence thesis;

          end;

            suppose not v0 in V & ex w0 be Vertex of G st w0 in V & (v0 .degree() ) c< ((w0 .degree() ) +` 2);

            then

            consider w0 be Vertex of G such that

             A9: w0 in V & (v0 .degree() ) c< ((w0 .degree() ) +` 2);

            reconsider w = w0 as Vertex of H by A5;

            

             A10: (w .degree() ) = ((w0 .degree() ) +` 2) by A3, A9, GLIB_012: 43;

            per cases ;

              suppose

               A11: for u0 be Vertex of G st u0 in V holds (u0 .degree() ) c= (w0 .degree() );

              now

                let u be Vertex of H;

                reconsider u0 = u as Vertex of G by A5;

                per cases ;

                  suppose

                   A12: u0 in V;

                  then

                   A13: (u .degree() ) = ((u0 .degree() ) +` 2) by A3, GLIB_012: 43;

                  (u0 .degree() ) c= (w0 .degree() ) & 2 c= 2 by A11, A12;

                  hence (u .degree() ) c= (w .degree() ) by A10, A13, CARD_2: 83;

                end;

                  suppose not u0 in V;

                  then (u0 .degree() ) = (u .degree() ) by A3, GLIB_012: 44;

                  then (u .degree() ) c= (v0 .degree() ) by A4;

                  hence (u .degree() ) c= (w .degree() ) by A9, A10, XBOOLE_0:def 8, XBOOLE_1: 1;

                end;

              end;

              hence thesis;

            end;

              suppose ex u0 be Vertex of G st u0 in V & not (u0 .degree() ) c= (w0 .degree() );

              then

              consider u0 be Vertex of G such that

               A14: u0 in V & not (u0 .degree() ) c= (w0 .degree() );

              reconsider u = u0 as Vertex of H by A5;

              

               A15: (u .degree() ) = ((u0 .degree() ) +` 2) by A3, A14, GLIB_012: 43;

              (u0 .degree() ) c= (v0 .degree() ) & (w0 .degree() ) c= (v0 .degree() ) by A4;

              then

               A16: (u0 .degree() ) = (v0 .degree() ) by A9, A14, Lm6;

              now

                let x be Vertex of H;

                reconsider x0 = x as Vertex of G by A5;

                per cases ;

                  suppose x0 in V;

                  then

                   A17: (x .degree() ) = ((x0 .degree() ) +` 2) by A3, GLIB_012: 43;

                  (x0 .degree() ) c= (u0 .degree() ) & 2 c= 2 by A4, A16;

                  hence (x .degree() ) c= (u .degree() ) by A15, A17, CARD_2: 83;

                end;

                  suppose not x0 in V;

                  

                  then

                   A18: (x .degree() ) = (x0 .degree() ) by A3, GLIB_012: 44

                  .= ((x0 .degree() ) +` 0 ) by CARD_2: 18;

                  (x0 .degree() ) c= (u0 .degree() ) & 0 c= 2 by A4, A16, XBOOLE_1: 2;

                  hence (x .degree() ) c= (u .degree() ) by A15, A18, CARD_2: 83;

                end;

              end;

              hence thesis;

            end;

          end;

            suppose

             A19: not v0 in V & for w0 be Vertex of G holds not w0 in V or not (v0 .degree() ) c< ((w0 .degree() ) +` 2);

            then

             A20: (v .degree() ) = (v0 .degree() ) by A3, GLIB_012: 44;

            now

              let w be Vertex of H;

              reconsider w0 = w as Vertex of G by A5;

              per cases ;

                suppose

                 A21: w0 in V;

                then (w .degree() ) = ((w0 .degree() ) +` 2) by A3, GLIB_012: 43;

                hence (w .degree() ) c= (v .degree() ) by A19, A20, A21, XBOOLE_0:def 8;

              end;

                suppose not w0 in V;

                then (w .degree() ) = (w0 .degree() ) by A3, GLIB_012: 44;

                hence (w .degree() ) c= (v .degree() ) by A4, A20;

              end;

            end;

            hence thesis;

          end;

        end;

          suppose not V c= ( the_Vertices_of G);

          then G == H by GLIB_012:def 5;

          hence thesis by Th85;

        end;

      end;

    end

    registration

      let G be with_max_degree _Graph, v,e,w be object;

      cluster -> with_max_degree for addEdge of G, v, e, w;

      coherence

      proof

        let H be addEdge of G, v, e, w;

        per cases ;

          suppose

           A1: v is Vertex of G & w is Vertex of G & not e in ( the_Edges_of G);

          then

          reconsider v1 = v, w1 = w as Vertex of G;

          consider v0 be Vertex of G such that

           A2: for w0 be Vertex of G holds (w0 .degree() ) c= (v0 .degree() ) by Def12;

          

           A3: ( the_Vertices_of G) = ( the_Vertices_of H) by A1, GLIB_006:def 11;

          then

          reconsider v9 = v0, v2 = v1, w2 = w1 as Vertex of H;

          per cases ;

            suppose

             A4: v <> w & (v0 .degree() ) = (v1 .degree() );

            now

              let u be Vertex of H;

              reconsider u0 = u as Vertex of G by A3;

              per cases ;

                suppose u0 = v;

                hence (u .degree() ) c= (v2 .degree() );

              end;

                suppose u0 = w;

                then

                 A5: (u .degree() ) = ((w1 .degree() ) +` 1) by A1, A4, GLIBPRE0: 50;

                (w1 .degree() ) c= (v1 .degree() ) & 1 c= 1 by A2, A4;

                then ((w1 .degree() ) +` 1) c= ((v1 .degree() ) +` 1) by CARD_2: 83;

                hence (u .degree() ) c= (v2 .degree() ) by A1, A4, A5, GLIBPRE0: 49;

              end;

                suppose u0 <> v & u0 <> w;

                then

                 A6: (u .degree() ) = (u0 .degree() ) by GLIBPRE0: 48;

                (u0 .degree() ) c= (v1 .degree() ) & 0 c= 1 by A2, A4, XBOOLE_1: 2;

                then ((u0 .degree() ) +` 0 ) c= ((v1 .degree() ) +` 1) by CARD_2: 83;

                then (u .degree() ) c= ((v1 .degree() ) +` 1) by A6, CARD_2: 18;

                hence (u .degree() ) c= (v2 .degree() ) by A1, A4, GLIBPRE0: 49;

              end;

            end;

            hence thesis;

          end;

            suppose

             A7: v <> w & (v0 .degree() ) = (w1 .degree() );

            now

              let u be Vertex of H;

              reconsider u0 = u as Vertex of G by A3;

              per cases ;

                suppose u0 = w;

                hence (u .degree() ) c= (w2 .degree() );

              end;

                suppose u0 = v;

                then

                 A8: (u .degree() ) = ((v1 .degree() ) +` 1) by A1, A7, GLIBPRE0: 49;

                (v1 .degree() ) c= (w1 .degree() ) & 1 c= 1 by A2, A7;

                then ((v1 .degree() ) +` 1) c= ((w1 .degree() ) +` 1) by CARD_2: 83;

                hence (u .degree() ) c= (w2 .degree() ) by A1, A7, A8, GLIBPRE0: 50;

              end;

                suppose u0 <> v & u0 <> w;

                then

                 A9: (u .degree() ) = (u0 .degree() ) by GLIBPRE0: 48;

                (u0 .degree() ) c= (w1 .degree() ) & 0 c= 1 by A2, A7, XBOOLE_1: 2;

                then ((u0 .degree() ) +` 0 ) c= ((w1 .degree() ) +` 1) by CARD_2: 83;

                then (u .degree() ) c= ((w1 .degree() ) +` 1) by A9, CARD_2: 18;

                hence (u .degree() ) c= (w2 .degree() ) by A1, A7, GLIBPRE0: 50;

              end;

            end;

            hence thesis;

          end;

            suppose

             A10: v <> w & (v0 .degree() ) <> (v1 .degree() ) & (v0 .degree() ) <> (w1 .degree() );

            then ((v1 .degree() ) +` 1) c= (v0 .degree() ) & ((w1 .degree() ) +` 1) c= (v0 .degree() ) by A2, Lm1;

            then

             A11: ((v1 .degree() ) +` 1) c= (v9 .degree() ) & ((w1 .degree() ) +` 1) c= (v9 .degree() ) by A10, GLIBPRE0: 48;

            now

              let u be Vertex of H;

              reconsider u0 = u as Vertex of G by A3;

              per cases ;

                suppose u0 = v;

                hence (u .degree() ) c= (v9 .degree() ) by A1, A10, A11, GLIBPRE0: 49;

              end;

                suppose u0 = w;

                hence (u .degree() ) c= (v9 .degree() ) by A1, A10, A11, GLIBPRE0: 50;

              end;

                suppose u0 <> v & u0 <> w;

                then

                 A12: (u .degree() ) = (u0 .degree() ) by GLIBPRE0: 48;

                (u0 .degree() ) c= (v0 .degree() ) by A2;

                hence (u .degree() ) c= (v9 .degree() ) by A10, A12, GLIBPRE0: 48;

              end;

            end;

            hence thesis;

          end;

            suppose v = w;

            then H is addLoops of G, {v1} by A1, GLIB_012: 27;

            hence thesis;

          end;

        end;

          suppose not (v is Vertex of G & w is Vertex of G & not e in ( the_Edges_of G));

          then G == H by GLIB_006:def 11;

          hence thesis by Th85;

        end;

      end;

      cluster -> with_max_degree for addAdjVertex of G, v, e, w;

      coherence

      proof

        let H be addAdjVertex of G, v, e, w;

        per cases ;

          suppose v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & not w in ( the_Vertices_of G);

          then

          consider G9 be addVertex of G, w such that

           A13: H is addEdge of G9, v, e, w by GLIB_006: 125;

          thus thesis by A13;

        end;

          suppose not v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & w in ( the_Vertices_of G);

          then

          consider G9 be addVertex of G, v such that

           A14: H is addEdge of G9, v, e, w by GLIB_006: 126;

          thus thesis by A14;

        end;

          suppose not ((v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & not w in ( the_Vertices_of G)) or ( not v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & w in ( the_Vertices_of G)));

          then G == H by GLIB_006:def 12;

          hence thesis by Th85;

        end;

      end;

    end

    

     Lm7: for a,b be Cardinal st a in (b +` 1) holds a c= b

    proof

      let a,b be Cardinal;

      assume

       A1: a in (b +` 1);

      per cases ;

        suppose

         A2: b is infinite;

        then 1 c= b;

        then (b +` 1) = b by A2, CARD_2: 76;

        hence thesis by A1, ORDINAL1:def 2;

      end;

        suppose

         A3: b is finite;

        then

        reconsider m = b as Nat;

        (b +` 1) is finite & a c= (b +` 1) by A1, A3, ORDINAL1:def 2;

        then

        reconsider n = a as Nat;

        a in ( Segm (m +` 1)) by A1;

        then n < (m + 1) by NAT_1: 44;

        then n <= m by NAT_1: 13;

        then ( Segm n) c= ( Segm m) by NAT_1: 39;

        hence thesis;

      end;

    end;

    registration

      let G be with_max_degree _Graph, v be object, V be set;

      cluster -> with_max_degree for addAdjVertexAll of G, v, V;

      coherence

      proof

        let H be addAdjVertexAll of G, v, V;

        per cases ;

          suppose

           A1: not v in ( the_Vertices_of G) & V c= ( the_Vertices_of G);

          consider v0 be Vertex of G such that

           A2: for w0 be Vertex of G holds (w0 .degree() ) c= (v0 .degree() ) by Def12;

          

           A3: ( the_Vertices_of H) = (( the_Vertices_of G) \/ {v}) by A1, GLIB_007:def 4;

          then

          reconsider v9 = v0 as Vertex of H by XBOOLE_0:def 3;

          reconsider v1 = v as Vertex of H by A1, GLIB_007: 50;

          

           A4: for w be Vertex of H, w0 be Vertex of G st w = w0 & (w .degree() ) <> ((w0 .degree() ) +` 1) holds (w .degree() ) = (w0 .degree() )

          proof

            let w be Vertex of H, w0 be Vertex of G;

            assume

             A5: w = w0;

            assume

             A6: (w .degree() ) <> ((w0 .degree() ) +` 1);

            

             A7: (w .degree() ) c= ((w0 .degree() ) +` 1) by A5, GLIBPRE0: 60;

            then

             A8: ((w .degree() ) +` 1) c= ((w0 .degree() ) +` 1) by A6, Lm1;

            G is Subgraph of H by GLIB_006: 57;

            then (w0 .inDegree() ) c= (w .inDegree() ) & (w0 .outDegree() ) c= (w .outDegree() ) by A5, GLIB_000: 78, CARD_1: 11;

            then

             A9: (w0 .degree() ) c= (w .degree() ) by CARD_2: 83;

            then ((w0 .degree() ) +` 1) c= ((w .degree() ) +` 1) by CARD_2: 83;

            then

             A10: ((w .degree() ) +` 1) = ((w0 .degree() ) +` 1) by A8, XBOOLE_0:def 10;

            per cases by A7;

              suppose

               A11: (w0 .degree() ) is infinite;

              then

               A12: (w .degree() ) is infinite by A9;

              then 1 c= (w .degree() );

              then

               A13: ((w .degree() ) +` 1) = (w .degree() ) by A12, CARD_2: 76;

              1 c= (w0 .degree() ) by A11;

              hence thesis by A10, A11, A13, CARD_2: 76;

            end;

              suppose (w .degree() ) is finite;

              then

              reconsider m = (w0 .degree() ), n = (w .degree() ) as Nat by A9;

              (m + 1) = (m +` 1)

              .= (n +` 1) by A10

              .= (n + 1);

              hence thesis;

            end;

          end;

          per cases by ORDINAL1: 16;

            suppose

             A14: ((v0 .degree() ) +` 1) c= (v1 .degree() );

            now

              let w be Vertex of H;

              per cases by A3, XBOOLE_0:def 3;

                suppose w in ( the_Vertices_of G);

                then

                reconsider w0 = w as Vertex of G;

                

                 A15: (w .degree() ) c= ((w0 .degree() ) +` 1) by GLIBPRE0: 60;

                (w0 .degree() ) c= (v0 .degree() ) & 1 c= 1 by A2;

                then ((w0 .degree() ) +` 1) c= ((v0 .degree() ) +` 1) by CARD_2: 83;

                then (w .degree() ) c= ((v0 .degree() ) +` 1) by A15, XBOOLE_1: 1;

                hence (w .degree() ) c= (v1 .degree() ) by A14, XBOOLE_1: 1;

              end;

                suppose w in {v};

                hence (w .degree() ) c= (v1 .degree() ) by TARSKI:def 1;

              end;

            end;

            hence thesis;

          end;

            suppose

             A16: (v1 .degree() ) in ((v0 .degree() ) +` 1) & (v9 .degree() ) = ((v0 .degree() ) +` 1);

            now

              let w be Vertex of H;

              per cases by A3, XBOOLE_0:def 3;

                suppose w in ( the_Vertices_of G);

                then

                reconsider w0 = w as Vertex of G;

                

                 A17: (w .degree() ) c= ((w0 .degree() ) +` 1) by GLIBPRE0: 60;

                (w0 .degree() ) c= (v0 .degree() ) & 1 c= 1 by A2;

                then ((w0 .degree() ) +` 1) c= ((v0 .degree() ) +` 1) by CARD_2: 83;

                hence (w .degree() ) c= (v9 .degree() ) by A16, A17, XBOOLE_1: 1;

              end;

                suppose w in {v};

                then w = v1 by TARSKI:def 1;

                hence (w .degree() ) c= (v9 .degree() ) by A16, ORDINAL1:def 2;

              end;

            end;

            hence thesis;

          end;

            suppose

             A18: (v1 .degree() ) in ((v0 .degree() ) +` 1) & (v9 .degree() ) <> ((v0 .degree() ) +` 1) & for w0 be Vertex of G, w be Vertex of H st w0 = w & (w .degree() ) = ((w0 .degree() ) +` 1) holds ((w0 .degree() ) +` 1) c= (v0 .degree() );

            then

             A19: (v9 .degree() ) = (v0 .degree() ) by A4;

            now

              let w be Vertex of H;

              per cases by A3, XBOOLE_0:def 3;

                suppose w in ( the_Vertices_of G);

                then

                reconsider w0 = w as Vertex of G;

                per cases ;

                  suppose (w .degree() ) = ((w0 .degree() ) +` 1);

                  hence (w .degree() ) c= (v9 .degree() ) by A18, A19;

                end;

                  suppose (w .degree() ) <> ((w0 .degree() ) +` 1);

                  then (w .degree() ) = (w0 .degree() ) by A4;

                  hence (w .degree() ) c= (v9 .degree() ) by A2, A19;

                end;

              end;

                suppose w in {v};

                then w = v1 by TARSKI:def 1;

                hence (w .degree() ) c= (v9 .degree() ) by A18, A19, Lm7;

              end;

            end;

            hence thesis;

          end;

            suppose

             A20: (v1 .degree() ) c= ((v0 .degree() ) +` 1) & (v9 .degree() ) <> ((v0 .degree() ) +` 1) & not for w0 be Vertex of G, w be Vertex of H st w0 = w & (w .degree() ) = ((w0 .degree() ) +` 1) holds (w .degree() ) = ((w0 .degree() ) +` 1) & ((w0 .degree() ) +` 1) c= (v0 .degree() );

            consider w0 be Vertex of G, w be Vertex of H such that

             A21: w0 = w & (w .degree() ) = ((w0 .degree() ) +` 1) and

             A22: not ((w0 .degree() ) +` 1) c= (v0 .degree() ) by A20;

            (v0 .degree() ) in (w .degree() ) by A21, A22, ORDINAL1: 16;

            then (v0 .degree() ) c= (w .degree() ) & (v0 .degree() ) <> (w .degree() ) by ORDINAL1: 16;

            then

             A23: ((v0 .degree() ) +` 1) c= (w .degree() ) by Lm1;

            now

              let u be Vertex of H;

              per cases by A3, XBOOLE_0:def 3;

                suppose u in ( the_Vertices_of G);

                then

                reconsider u0 = u as Vertex of G;

                

                 A24: (u .degree() ) c= ((u0 .degree() ) +` 1) by GLIBPRE0: 60;

                (u0 .degree() ) c= (v0 .degree() ) & 1 c= 1 by A2;

                then ((u0 .degree() ) +` 1) c= ((v0 .degree() ) +` 1) by CARD_2: 83;

                then ((u0 .degree() ) +` 1) c= (w .degree() ) by A23, XBOOLE_1: 1;

                hence (u .degree() ) c= (w .degree() ) by A24, XBOOLE_1: 1;

              end;

                suppose u in {v};

                then u = v1 by TARSKI:def 1;

                hence (u .degree() ) c= (w .degree() ) by A20, A23, XBOOLE_1: 1;

              end;

            end;

            hence thesis;

          end;

        end;

          suppose not ( not v in ( the_Vertices_of G) & V c= ( the_Vertices_of G));

          then G == H by GLIB_007:def 4;

          hence thesis by Th85;

        end;

      end;

    end

    registration

      let G be with_max_in_degree _Graph;

      cluster -> with_max_out_degree for reverseEdgeDirections of G;

      coherence

      proof

        let H be reverseEdgeDirections of G;

        consider v1 be Vertex of G such that

         A1: for w1 be Vertex of G holds (w1 .inDegree() ) c= (v1 .inDegree() ) by Def13;

        

         A2: ( the_Vertices_of G) = ( the_Vertices_of H) by GLIB_007:def 1;

        then

        reconsider v2 = v1 as Vertex of H;

        now

          let w2 be Vertex of H;

          reconsider w1 = w2 as Vertex of G by A2;

          (w1 .inDegree() ) c= (v1 .inDegree() ) by A1;

          then (w1 .inDegree() ) c= (v2 .outDegree() ) by GLIBPRE0: 55;

          hence (w2 .outDegree() ) c= (v2 .outDegree() ) by GLIBPRE0: 55;

        end;

        hence thesis;

      end;

    end

    registration

      let G be with_max_in_degree _Graph, V be set;

      cluster -> with_max_in_degree for addVertices of G, V;

      coherence

      proof

        let H be addVertices of G, V;

        consider v0 be Vertex of G such that

         A1: for w0 be Vertex of G holds (w0 .inDegree() ) c= (v0 .inDegree() ) by Def13;

        ( the_Vertices_of G) c= ( the_Vertices_of H) by GLIB_006:def 9;

        then

        reconsider v = v0 as Vertex of H by TARSKI:def 3;

        now

          let w be Vertex of H;

          per cases ;

            suppose w in ( the_Vertices_of G);

            then

            reconsider w0 = w as Vertex of G;

            (w .inDegree() ) = (w0 .inDegree() ) & (v .inDegree() ) = (v0 .inDegree() ) by GLIBPRE0: 47;

            hence (w .inDegree() ) c= (v .inDegree() ) by A1;

          end;

            suppose

             A2: not w in ( the_Vertices_of G);

            ( the_Vertices_of H) = (( the_Vertices_of G) \/ V) by GLIB_006:def 10;

            then w in V by A2, XBOOLE_0:def 3;

            then w in (V \ ( the_Vertices_of G)) by A2, XBOOLE_0:def 5;

            then w is isolated by GLIB_006: 88;

            then (w .inDegree() ) = 0 by GLIBPRE0: 34;

            hence (w .inDegree() ) c= (v .inDegree() ) by XBOOLE_1: 2;

          end;

        end;

        hence thesis;

      end;

      cluster -> with_max_in_degree for addLoops of G, V;

      coherence

      proof

        let H be addLoops of G, V;

        per cases ;

          suppose

           A3: V c= ( the_Vertices_of G);

          consider v0 be Vertex of G such that

           A4: for w0 be Vertex of G holds (w0 .inDegree() ) c= (v0 .inDegree() ) by Def13;

          

           A5: ( the_Vertices_of G) = ( the_Vertices_of H) by A3, GLIB_012:def 5;

          then

          reconsider v = v0 as Vertex of H;

          per cases ;

            suppose v0 in V;

            then

             A6: (v .inDegree() ) = ((v0 .inDegree() ) +` 1) by A3, GLIB_012: 43;

            now

              let w be Vertex of H;

              reconsider w0 = w as Vertex of G by A5;

              per cases ;

                suppose w0 in V;

                then

                 A7: (w .inDegree() ) = ((w0 .inDegree() ) +` 1) by A3, GLIB_012: 43;

                (w0 .inDegree() ) c= (v0 .inDegree() ) & 1 c= 1 by A4;

                hence (w .inDegree() ) c= (v .inDegree() ) by A6, A7, CARD_2: 83;

              end;

                suppose not w0 in V;

                

                then

                 A8: (w .inDegree() ) = (w0 .inDegree() ) by A3, GLIB_012: 44

                .= ((w0 .inDegree() ) +` 0 ) by CARD_2: 18;

                (w0 .inDegree() ) c= (v0 .inDegree() ) & 0 c= 1 by A4, XBOOLE_1: 2;

                hence (w .inDegree() ) c= (v .inDegree() ) by A6, A8, CARD_2: 83;

              end;

            end;

            hence thesis;

          end;

            suppose not v0 in V & ex w0 be Vertex of G st w0 in V & (v0 .inDegree() ) c< ((w0 .inDegree() ) +` 1);

            then

            consider w0 be Vertex of G such that

             A9: w0 in V & (v0 .inDegree() ) c< ((w0 .inDegree() ) +` 1);

            reconsider w = w0 as Vertex of H by A5;

            

             A10: (w .inDegree() ) = ((w0 .inDegree() ) +` 1) by A3, A9, GLIB_012: 43;

             not ((w0 .inDegree() ) +` 1) c= (v0 .inDegree() ) by A9, XBOOLE_0:def 8;

            then

             A11: (w0 .inDegree() ) = (v0 .inDegree() ) by A4, Lm1;

            now

              let u be Vertex of H;

              reconsider u0 = u as Vertex of G by A5;

              per cases ;

                suppose u0 in V;

                then

                 A12: (u .inDegree() ) = ((u0 .inDegree() ) +` 1) by A3, GLIB_012: 43;

                (u0 .inDegree() ) c= (w0 .inDegree() ) & 1 c= 1 by A4, A11;

                hence (u .inDegree() ) c= (w .inDegree() ) by A10, A12, CARD_2: 83;

              end;

                suppose not u0 in V;

                

                then

                 A13: (u .inDegree() ) = (u0 .inDegree() ) by A3, GLIB_012: 44

                .= ((u0 .inDegree() ) +` 0 ) by CARD_2: 18;

                (u0 .inDegree() ) c= (w0 .inDegree() ) & 0 c= 1 by A4, A11, XBOOLE_1: 2;

                hence (u .inDegree() ) c= (w .inDegree() ) by A10, A13, CARD_2: 83;

              end;

            end;

            hence thesis;

          end;

            suppose

             A14: not v0 in V & for w0 be Vertex of G holds not w0 in V or not (v0 .inDegree() ) c< ((w0 .inDegree() ) +` 1);

            then

             A15: (v .inDegree() ) = (v0 .inDegree() ) by A3, GLIB_012: 44;

            now

              let w be Vertex of H;

              reconsider w0 = w as Vertex of G by A5;

              per cases ;

                suppose

                 A16: w0 in V;

                then (w .inDegree() ) = ((w0 .inDegree() ) +` 1) by A3, GLIB_012: 43;

                hence (w .inDegree() ) c= (v .inDegree() ) by A14, A15, A16, XBOOLE_0:def 8;

              end;

                suppose not w0 in V;

                then (w .inDegree() ) = (w0 .inDegree() ) by A3, GLIB_012: 44;

                hence (w .inDegree() ) c= (v .inDegree() ) by A4, A15;

              end;

            end;

            hence thesis;

          end;

        end;

          suppose not V c= ( the_Vertices_of G);

          then G == H by GLIB_012:def 5;

          hence thesis by Th85;

        end;

      end;

    end

    registration

      let G be with_max_in_degree _Graph, v,e,w be object;

      cluster -> with_max_in_degree for addEdge of G, v, e, w;

      coherence

      proof

        let H be addEdge of G, v, e, w;

        per cases ;

          suppose

           A1: v is Vertex of G & w is Vertex of G & not e in ( the_Edges_of G);

          then

          reconsider v1 = v, w1 = w as Vertex of G;

          consider v0 be Vertex of G such that

           A2: for w0 be Vertex of G holds (w0 .inDegree() ) c= (v0 .inDegree() ) by Def13;

          

           A3: ( the_Vertices_of G) = ( the_Vertices_of H) by A1, GLIB_006:def 11;

          then

          reconsider v9 = v0, v2 = v1, w2 = w1 as Vertex of H;

          per cases ;

            suppose

             A4: v <> w & (v0 .inDegree() ) = (w1 .inDegree() );

            now

              let u be Vertex of H;

              reconsider u0 = u as Vertex of G by A3;

              per cases ;

                suppose u0 = w;

                hence (u .inDegree() ) c= (w2 .inDegree() );

              end;

                suppose u0 = v;

                

                then

                 A5: (u .inDegree() ) = (v1 .inDegree() ) by A1, A4, GLIBPRE0: 49

                .= ((v1 .inDegree() ) +` 0 ) by CARD_2: 18;

                (v1 .inDegree() ) c= (w1 .inDegree() ) & 0 c= 1 by A2, A4, XBOOLE_1: 2;

                then ((v1 .inDegree() ) +` 0 ) c= ((w1 .inDegree() ) +` 1) by CARD_2: 83;

                hence (u .inDegree() ) c= (w2 .inDegree() ) by A1, A4, A5, GLIBPRE0: 50;

              end;

                suppose u0 <> v & u0 <> w;

                then

                 A6: (u .inDegree() ) = (u0 .inDegree() ) by GLIBPRE0: 48;

                (u0 .inDegree() ) c= (w1 .inDegree() ) & 0 c= 1 by A2, A4, XBOOLE_1: 2;

                then ((u0 .inDegree() ) +` 0 ) c= ((w1 .inDegree() ) +` 1) by CARD_2: 83;

                then (u .inDegree() ) c= ((w1 .inDegree() ) +` 1) by A6, CARD_2: 18;

                hence (u .inDegree() ) c= (w2 .inDegree() ) by A1, A4, GLIBPRE0: 50;

              end;

            end;

            hence thesis;

          end;

            suppose

             A7: v <> w & (v0 .inDegree() ) <> (w1 .inDegree() );

            

             A8: (v0 .inDegree() ) = (v9 .inDegree() )

            proof

              per cases ;

                suppose v0 <> v1;

                hence thesis by A7, GLIBPRE0: 48;

              end;

                suppose v0 = v1;

                hence thesis by A1, A7, GLIBPRE0: 49;

              end;

            end;

            then

             A9: ((w1 .inDegree() ) +` 1) c= (v9 .inDegree() ) by A2, A7, Lm1;

            now

              let u be Vertex of H;

              reconsider u0 = u as Vertex of G by A3;

              per cases ;

                suppose u0 = v;

                then (u .inDegree() ) = (v1 .inDegree() ) by A1, A7, GLIBPRE0: 49;

                hence (u .inDegree() ) c= (v9 .inDegree() ) by A2, A8;

              end;

                suppose u0 = w;

                hence (u .inDegree() ) c= (v9 .inDegree() ) by A1, A7, A9, GLIBPRE0: 50;

              end;

                suppose u0 <> v & u0 <> w;

                then (u .inDegree() ) = (u0 .inDegree() ) by GLIBPRE0: 48;

                hence (u .inDegree() ) c= (v9 .inDegree() ) by A2, A8;

              end;

            end;

            hence thesis;

          end;

            suppose v = w;

            then H is addLoops of G, {v1} by A1, GLIB_012: 27;

            hence thesis;

          end;

        end;

          suppose not (v is Vertex of G & w is Vertex of G & not e in ( the_Edges_of G));

          then G == H by GLIB_006:def 11;

          hence thesis by Th85;

        end;

      end;

      cluster -> with_max_in_degree for addAdjVertex of G, v, e, w;

      coherence

      proof

        let H be addAdjVertex of G, v, e, w;

        per cases ;

          suppose v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & not w in ( the_Vertices_of G);

          then

          consider G9 be addVertex of G, w such that

           A10: H is addEdge of G9, v, e, w by GLIB_006: 125;

          thus thesis by A10;

        end;

          suppose not v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & w in ( the_Vertices_of G);

          then

          consider G9 be addVertex of G, v such that

           A11: H is addEdge of G9, v, e, w by GLIB_006: 126;

          thus thesis by A11;

        end;

          suppose not ((v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & not w in ( the_Vertices_of G)) or ( not v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & w in ( the_Vertices_of G)));

          then G == H by GLIB_006:def 12;

          hence thesis by Th85;

        end;

      end;

    end

    registration

      let G be with_max_in_degree _Graph, v be object, V be set;

      cluster -> with_max_in_degree for addAdjVertexAll of G, v, V;

      coherence

      proof

        let H be addAdjVertexAll of G, v, V;

        per cases ;

          suppose

           A1: not v in ( the_Vertices_of G) & V c= ( the_Vertices_of G);

          consider v0 be Vertex of G such that

           A2: for w0 be Vertex of G holds (w0 .inDegree() ) c= (v0 .inDegree() ) by Def13;

          

           A3: ( the_Vertices_of H) = (( the_Vertices_of G) \/ {v}) by A1, GLIB_007:def 4;

          then

          reconsider v9 = v0 as Vertex of H by XBOOLE_0:def 3;

          reconsider v1 = v as Vertex of H by A1, GLIB_007: 50;

          

           A4: for w be Vertex of H, w0 be Vertex of G st w = w0 & (w .inDegree() ) <> ((w0 .inDegree() ) +` 1) holds (w .inDegree() ) = (w0 .inDegree() )

          proof

            let w be Vertex of H, w0 be Vertex of G;

            assume

             A5: w = w0;

            assume

             A6: (w .inDegree() ) <> ((w0 .inDegree() ) +` 1);

            

             A7: (w .inDegree() ) c= ((w0 .inDegree() ) +` 1) by A5, GLIBPRE0: 60;

            then

             A8: ((w .inDegree() ) +` 1) c= ((w0 .inDegree() ) +` 1) by A6, Lm1;

            G is Subgraph of H by GLIB_006: 57;

            then

             A9: (w0 .inDegree() ) c= (w .inDegree() ) by A5, GLIB_000: 78, CARD_1: 11;

            then ((w0 .inDegree() ) +` 1) c= ((w .inDegree() ) +` 1) by CARD_2: 83;

            then

             A10: ((w .inDegree() ) +` 1) = ((w0 .inDegree() ) +` 1) by A8, XBOOLE_0:def 10;

            per cases by A7;

              suppose

               A11: (w0 .inDegree() ) is infinite;

              then

               A12: (w .inDegree() ) is infinite by A9;

              then 1 c= (w .inDegree() );

              then

               A13: ((w .inDegree() ) +` 1) = (w .inDegree() ) by A12, CARD_2: 76;

              1 c= (w0 .inDegree() ) by A11;

              hence thesis by A10, A11, A13, CARD_2: 76;

            end;

              suppose (w .inDegree() ) is finite;

              then

              reconsider m = (w0 .inDegree() ), n = (w .inDegree() ) as Nat by A9;

              (m + 1) = (m +` 1)

              .= (n +` 1) by A10

              .= (n + 1);

              hence thesis;

            end;

          end;

          per cases by ORDINAL1: 16;

            suppose

             A14: ((v0 .inDegree() ) +` 1) c= (v1 .inDegree() );

            now

              let w be Vertex of H;

              per cases by A3, XBOOLE_0:def 3;

                suppose w in ( the_Vertices_of G);

                then

                reconsider w0 = w as Vertex of G;

                

                 A15: (w .inDegree() ) c= ((w0 .inDegree() ) +` 1) by GLIBPRE0: 60;

                (w0 .inDegree() ) c= (v0 .inDegree() ) & 1 c= 1 by A2;

                then ((w0 .inDegree() ) +` 1) c= ((v0 .inDegree() ) +` 1) by CARD_2: 83;

                then (w .inDegree() ) c= ((v0 .inDegree() ) +` 1) by A15, XBOOLE_1: 1;

                hence (w .inDegree() ) c= (v1 .inDegree() ) by A14, XBOOLE_1: 1;

              end;

                suppose w in {v};

                hence (w .inDegree() ) c= (v1 .inDegree() ) by TARSKI:def 1;

              end;

            end;

            hence thesis;

          end;

            suppose

             A16: (v1 .inDegree() ) in ((v0 .inDegree() ) +` 1) & (v9 .inDegree() ) = ((v0 .inDegree() ) +` 1);

            now

              let w be Vertex of H;

              per cases by A3, XBOOLE_0:def 3;

                suppose w in ( the_Vertices_of G);

                then

                reconsider w0 = w as Vertex of G;

                

                 A17: (w .inDegree() ) c= ((w0 .inDegree() ) +` 1) by GLIBPRE0: 60;

                (w0 .inDegree() ) c= (v0 .inDegree() ) & 1 c= 1 by A2;

                then ((w0 .inDegree() ) +` 1) c= ((v0 .inDegree() ) +` 1) by CARD_2: 83;

                hence (w .inDegree() ) c= (v9 .inDegree() ) by A16, A17, XBOOLE_1: 1;

              end;

                suppose w in {v};

                then w = v1 by TARSKI:def 1;

                hence (w .inDegree() ) c= (v9 .inDegree() ) by A16, ORDINAL1:def 2;

              end;

            end;

            hence thesis;

          end;

            suppose

             A18: (v1 .inDegree() ) in ((v0 .inDegree() ) +` 1) & (v9 .inDegree() ) <> ((v0 .inDegree() ) +` 1) & for w0 be Vertex of G, w be Vertex of H st w0 = w & (w .inDegree() ) = ((w0 .inDegree() ) +` 1) holds ((w0 .inDegree() ) +` 1) c= (v0 .inDegree() );

            then

             A19: (v9 .inDegree() ) = (v0 .inDegree() ) by A4;

            now

              let w be Vertex of H;

              per cases by A3, XBOOLE_0:def 3;

                suppose w in ( the_Vertices_of G);

                then

                reconsider w0 = w as Vertex of G;

                per cases ;

                  suppose (w .inDegree() ) = ((w0 .inDegree() ) +` 1);

                  hence (w .inDegree() ) c= (v9 .inDegree() ) by A18, A19;

                end;

                  suppose (w .inDegree() ) <> ((w0 .inDegree() ) +` 1);

                  then (w .inDegree() ) = (w0 .inDegree() ) by A4;

                  hence (w .inDegree() ) c= (v9 .inDegree() ) by A2, A19;

                end;

              end;

                suppose w in {v};

                then (w .inDegree() ) = (v1 .inDegree() ) by TARSKI:def 1;

                hence (w .inDegree() ) c= (v9 .inDegree() ) by A18, A19, Lm7;

              end;

            end;

            hence thesis;

          end;

            suppose

             A20: (v1 .inDegree() ) c= ((v0 .inDegree() ) +` 1) & (v9 .inDegree() ) <> ((v0 .inDegree() ) +` 1) & not for w0 be Vertex of G, w be Vertex of H st w0 = w & (w .inDegree() ) = ((w0 .inDegree() ) +` 1) holds (w .inDegree() ) = ((w0 .inDegree() ) +` 1) & ((w0 .inDegree() ) +` 1) c= (v0 .inDegree() );

            consider w0 be Vertex of G, w be Vertex of H such that

             A21: w0 = w & (w .inDegree() ) = ((w0 .inDegree() ) +` 1) and

             A22: not ((w0 .inDegree() ) +` 1) c= (v0 .inDegree() ) by A20;

            (v0 .inDegree() ) in (w .inDegree() ) by A21, A22, ORDINAL1: 16;

            then (v0 .inDegree() ) c= (w .inDegree() ) & (v0 .inDegree() ) <> (w .inDegree() ) by ORDINAL1: 16;

            then

             A23: ((v0 .inDegree() ) +` 1) c= (w .inDegree() ) by Lm1;

            now

              let u be Vertex of H;

              per cases by A3, XBOOLE_0:def 3;

                suppose u in ( the_Vertices_of G);

                then

                reconsider u0 = u as Vertex of G;

                

                 A24: (u .inDegree() ) c= ((u0 .inDegree() ) +` 1) by GLIBPRE0: 60;

                (u0 .inDegree() ) c= (v0 .inDegree() ) & 1 c= 1 by A2;

                then ((u0 .inDegree() ) +` 1) c= ((v0 .inDegree() ) +` 1) by CARD_2: 83;

                then ((u0 .inDegree() ) +` 1) c= (w .inDegree() ) by A23, XBOOLE_1: 1;

                hence (u .inDegree() ) c= (w .inDegree() ) by A24, XBOOLE_1: 1;

              end;

                suppose u in {v};

                then u = v1 by TARSKI:def 1;

                hence (u .inDegree() ) c= (w .inDegree() ) by A20, A23, XBOOLE_1: 1;

              end;

            end;

            hence thesis;

          end;

        end;

          suppose not ( not v in ( the_Vertices_of G) & V c= ( the_Vertices_of G));

          then G == H by GLIB_007:def 4;

          hence thesis by Th85;

        end;

      end;

    end

    registration

      let G be with_max_out_degree _Graph;

      cluster -> with_max_in_degree for reverseEdgeDirections of G;

      coherence

      proof

        let H be reverseEdgeDirections of G;

        consider v1 be Vertex of G such that

         A1: for w1 be Vertex of G holds (w1 .outDegree() ) c= (v1 .outDegree() ) by Def14;

        

         A2: ( the_Vertices_of G) = ( the_Vertices_of H) by GLIB_007:def 1;

        then

        reconsider v2 = v1 as Vertex of H;

        now

          let w2 be Vertex of H;

          reconsider w1 = w2 as Vertex of G by A2;

          (w1 .outDegree() ) c= (v1 .outDegree() ) by A1;

          then (w1 .outDegree() ) c= (v2 .inDegree() ) by GLIBPRE0: 55;

          hence (w2 .inDegree() ) c= (v2 .inDegree() ) by GLIBPRE0: 55;

        end;

        hence thesis;

      end;

    end

    registration

      let G be with_max_out_degree _Graph, V be set;

      cluster -> with_max_out_degree for addVertices of G, V;

      coherence

      proof

        let H be addVertices of G, V;

        consider v0 be Vertex of G such that

         A1: for w0 be Vertex of G holds (w0 .outDegree() ) c= (v0 .outDegree() ) by Def14;

        ( the_Vertices_of G) c= ( the_Vertices_of H) by GLIB_006:def 9;

        then

        reconsider v = v0 as Vertex of H by TARSKI:def 3;

        now

          let w be Vertex of H;

          per cases ;

            suppose w in ( the_Vertices_of G);

            then

            reconsider w0 = w as Vertex of G;

            (w .outDegree() ) = (w0 .outDegree() ) & (v .outDegree() ) = (v0 .outDegree() ) by GLIBPRE0: 47;

            hence (w .outDegree() ) c= (v .outDegree() ) by A1;

          end;

            suppose

             A2: not w in ( the_Vertices_of G);

            ( the_Vertices_of H) = (( the_Vertices_of G) \/ V) by GLIB_006:def 10;

            then w in V by A2, XBOOLE_0:def 3;

            then w in (V \ ( the_Vertices_of G)) by A2, XBOOLE_0:def 5;

            then w is isolated by GLIB_006: 88;

            then (w .outDegree() ) = 0 by GLIBPRE0: 34;

            hence (w .outDegree() ) c= (v .outDegree() ) by XBOOLE_1: 2;

          end;

        end;

        hence thesis;

      end;

      cluster -> with_max_out_degree for addLoops of G, V;

      coherence

      proof

        let H be addLoops of G, V;

        per cases ;

          suppose

           A3: V c= ( the_Vertices_of G);

          consider v0 be Vertex of G such that

           A4: for w0 be Vertex of G holds (w0 .outDegree() ) c= (v0 .outDegree() ) by Def14;

          

           A5: ( the_Vertices_of G) = ( the_Vertices_of H) by A3, GLIB_012:def 5;

          then

          reconsider v = v0 as Vertex of H;

          per cases ;

            suppose v0 in V;

            then

             A6: (v .outDegree() ) = ((v0 .outDegree() ) +` 1) by A3, GLIB_012: 43;

            now

              let w be Vertex of H;

              reconsider w0 = w as Vertex of G by A5;

              per cases ;

                suppose w0 in V;

                then

                 A7: (w .outDegree() ) = ((w0 .outDegree() ) +` 1) by A3, GLIB_012: 43;

                (w0 .outDegree() ) c= (v0 .outDegree() ) & 1 c= 1 by A4;

                hence (w .outDegree() ) c= (v .outDegree() ) by A6, A7, CARD_2: 83;

              end;

                suppose not w0 in V;

                

                then

                 A8: (w .outDegree() ) = (w0 .outDegree() ) by A3, GLIB_012: 44

                .= ((w0 .outDegree() ) +` 0 ) by CARD_2: 18;

                (w0 .outDegree() ) c= (v0 .outDegree() ) & 0 c= 1 by A4, XBOOLE_1: 2;

                hence (w .outDegree() ) c= (v .outDegree() ) by A6, A8, CARD_2: 83;

              end;

            end;

            hence thesis;

          end;

            suppose not v0 in V & ex w0 be Vertex of G st w0 in V & (v0 .outDegree() ) c< ((w0 .outDegree() ) +` 1);

            then

            consider w0 be Vertex of G such that

             A9: w0 in V & (v0 .outDegree() ) c< ((w0 .outDegree() ) +` 1);

            reconsider w = w0 as Vertex of H by A5;

            

             A10: (w .outDegree() ) = ((w0 .outDegree() ) +` 1) by A3, A9, GLIB_012: 43;

             not ((w0 .outDegree() ) +` 1) c= (v0 .outDegree() ) by A9, XBOOLE_0:def 8;

            then

             A11: (w0 .outDegree() ) = (v0 .outDegree() ) by A4, Lm1;

            now

              let u be Vertex of H;

              reconsider u0 = u as Vertex of G by A5;

              per cases ;

                suppose u0 in V;

                then

                 A12: (u .outDegree() ) = ((u0 .outDegree() ) +` 1) by A3, GLIB_012: 43;

                (u0 .outDegree() ) c= (w0 .outDegree() ) & 1 c= 1 by A4, A11;

                hence (u .outDegree() ) c= (w .outDegree() ) by A10, A12, CARD_2: 83;

              end;

                suppose not u0 in V;

                

                then

                 A13: (u .outDegree() ) = (u0 .outDegree() ) by A3, GLIB_012: 44

                .= ((u0 .outDegree() ) +` 0 ) by CARD_2: 18;

                (u0 .outDegree() ) c= (w0 .outDegree() ) & 0 c= 1 by A4, A11, XBOOLE_1: 2;

                hence (u .outDegree() ) c= (w .outDegree() ) by A10, A13, CARD_2: 83;

              end;

            end;

            hence thesis;

          end;

            suppose

             A14: not v0 in V & for w0 be Vertex of G holds not w0 in V or not (v0 .outDegree() ) c< ((w0 .outDegree() ) +` 1);

            then

             A15: (v .outDegree() ) = (v0 .outDegree() ) by A3, GLIB_012: 44;

            now

              let w be Vertex of H;

              reconsider w0 = w as Vertex of G by A5;

              per cases ;

                suppose

                 A16: w0 in V;

                then (w .outDegree() ) = ((w0 .outDegree() ) +` 1) by A3, GLIB_012: 43;

                hence (w .outDegree() ) c= (v .outDegree() ) by A14, A15, A16, XBOOLE_0:def 8;

              end;

                suppose not w0 in V;

                then (w .outDegree() ) = (w0 .outDegree() ) by A3, GLIB_012: 44;

                hence (w .outDegree() ) c= (v .outDegree() ) by A4, A15;

              end;

            end;

            hence thesis;

          end;

        end;

          suppose not V c= ( the_Vertices_of G);

          then G == H by GLIB_012:def 5;

          hence thesis by Th85;

        end;

      end;

    end

    registration

      let G be with_max_out_degree _Graph, v,e,w be object;

      cluster -> with_max_out_degree for addEdge of G, v, e, w;

      coherence

      proof

        let H be addEdge of G, v, e, w;

        per cases ;

          suppose

           A1: v is Vertex of G & w is Vertex of G & not e in ( the_Edges_of G);

          then

          reconsider v1 = v, w1 = w as Vertex of G;

          consider v0 be Vertex of G such that

           A2: for w0 be Vertex of G holds (w0 .outDegree() ) c= (v0 .outDegree() ) by Def14;

          

           A3: ( the_Vertices_of G) = ( the_Vertices_of H) by A1, GLIB_006:def 11;

          then

          reconsider v9 = v0, v2 = v1, w2 = w1 as Vertex of H;

          per cases ;

            suppose

             A4: v <> w & (v0 .outDegree() ) = (v1 .outDegree() );

            now

              let u be Vertex of H;

              reconsider u0 = u as Vertex of G by A3;

              per cases ;

                suppose u0 = v;

                hence (u .outDegree() ) c= (v2 .outDegree() );

              end;

                suppose u0 = w;

                

                then

                 A5: (u .outDegree() ) = (w1 .outDegree() ) by A1, A4, GLIBPRE0: 50

                .= ((w1 .outDegree() ) +` 0 ) by CARD_2: 18;

                (w1 .outDegree() ) c= (v1 .outDegree() ) & 0 c= 1 by A2, A4, XBOOLE_1: 2;

                then ((w1 .outDegree() ) +` 0 ) c= ((v1 .outDegree() ) +` 1) by CARD_2: 83;

                hence (u .outDegree() ) c= (v2 .outDegree() ) by A1, A4, A5, GLIBPRE0: 49;

              end;

                suppose u0 <> v & u0 <> w;

                then

                 A6: (u .outDegree() ) = (u0 .outDegree() ) by GLIBPRE0: 48;

                (u0 .outDegree() ) c= (v1 .outDegree() ) & 0 c= 1 by A2, A4, XBOOLE_1: 2;

                then ((u0 .outDegree() ) +` 0 ) c= ((v1 .outDegree() ) +` 1) by CARD_2: 83;

                then (u .outDegree() ) c= ((v1 .outDegree() ) +` 1) by A6, CARD_2: 18;

                hence (u .outDegree() ) c= (v2 .outDegree() ) by A1, A4, GLIBPRE0: 49;

              end;

            end;

            hence thesis;

          end;

            suppose

             A7: v <> w & (v0 .outDegree() ) <> (v1 .outDegree() );

            

             A8: (v0 .outDegree() ) = (v9 .outDegree() )

            proof

              per cases ;

                suppose v0 <> w1;

                hence thesis by A7, GLIBPRE0: 48;

              end;

                suppose v0 = w1;

                hence thesis by A1, A7, GLIBPRE0: 50;

              end;

            end;

            then

             A9: ((v1 .outDegree() ) +` 1) c= (v9 .outDegree() ) by A2, A7, Lm1;

            now

              let u be Vertex of H;

              reconsider u0 = u as Vertex of G by A3;

              per cases ;

                suppose u0 = w;

                then (u .outDegree() ) = (w1 .outDegree() ) by A1, A7, GLIBPRE0: 50;

                hence (u .outDegree() ) c= (v9 .outDegree() ) by A2, A8;

              end;

                suppose u0 = v;

                hence (u .outDegree() ) c= (v9 .outDegree() ) by A1, A7, A9, GLIBPRE0: 49;

              end;

                suppose u0 <> v & u0 <> w;

                then (u .outDegree() ) = (u0 .outDegree() ) by GLIBPRE0: 48;

                hence (u .outDegree() ) c= (v9 .outDegree() ) by A2, A8;

              end;

            end;

            hence thesis;

          end;

            suppose v = w;

            then H is addLoops of G, {v1} by A1, GLIB_012: 27;

            hence thesis;

          end;

        end;

          suppose not (v is Vertex of G & w is Vertex of G & not e in ( the_Edges_of G));

          then G == H by GLIB_006:def 11;

          hence thesis by Th85;

        end;

      end;

      cluster -> with_max_out_degree for addAdjVertex of G, v, e, w;

      coherence

      proof

        let H be addAdjVertex of G, v, e, w;

        per cases ;

          suppose v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & not w in ( the_Vertices_of G);

          then

          consider G9 be addVertex of G, w such that

           A10: H is addEdge of G9, v, e, w by GLIB_006: 125;

          thus thesis by A10;

        end;

          suppose not v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & w in ( the_Vertices_of G);

          then

          consider G9 be addVertex of G, v such that

           A11: H is addEdge of G9, v, e, w by GLIB_006: 126;

          thus thesis by A11;

        end;

          suppose not ((v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & not w in ( the_Vertices_of G)) or ( not v in ( the_Vertices_of G) & not e in ( the_Edges_of G) & w in ( the_Vertices_of G)));

          then G == H by GLIB_006:def 12;

          hence thesis by Th85;

        end;

      end;

    end

    registration

      let G be with_max_out_degree _Graph, v be object, V be set;

      cluster -> with_max_out_degree for addAdjVertexAll of G, v, V;

      coherence

      proof

        let H be addAdjVertexAll of G, v, V;

        per cases ;

          suppose

           A1: not v in ( the_Vertices_of G) & V c= ( the_Vertices_of G);

          consider v0 be Vertex of G such that

           A2: for w0 be Vertex of G holds (w0 .outDegree() ) c= (v0 .outDegree() ) by Def14;

          

           A3: ( the_Vertices_of H) = (( the_Vertices_of G) \/ {v}) by A1, GLIB_007:def 4;

          then

          reconsider v9 = v0 as Vertex of H by XBOOLE_0:def 3;

          reconsider v1 = v as Vertex of H by A1, GLIB_007: 50;

          

           A4: for w be Vertex of H, w0 be Vertex of G st w = w0 & (w .outDegree() ) <> ((w0 .outDegree() ) +` 1) holds (w .outDegree() ) = (w0 .outDegree() )

          proof

            let w be Vertex of H, w0 be Vertex of G;

            assume

             A5: w = w0;

            assume

             A6: (w .outDegree() ) <> ((w0 .outDegree() ) +` 1);

            

             A7: (w .outDegree() ) c= ((w0 .outDegree() ) +` 1) by A5, GLIBPRE0: 60;

            then

             A8: ((w .outDegree() ) +` 1) c= ((w0 .outDegree() ) +` 1) by A6, Lm1;

            G is Subgraph of H by GLIB_006: 57;

            then

             A9: (w0 .outDegree() ) c= (w .outDegree() ) by A5, GLIB_000: 78, CARD_1: 11;

            then ((w0 .outDegree() ) +` 1) c= ((w .outDegree() ) +` 1) by CARD_2: 83;

            then

             A10: ((w .outDegree() ) +` 1) = ((w0 .outDegree() ) +` 1) by A8, XBOOLE_0:def 10;

            per cases by A7;

              suppose

               A11: (w0 .outDegree() ) is infinite;

              then

               A12: (w .outDegree() ) is infinite by A9;

              then 1 c= (w .outDegree() );

              then

               A13: ((w .outDegree() ) +` 1) = (w .outDegree() ) by A12, CARD_2: 76;

              1 c= (w0 .outDegree() ) by A11;

              hence thesis by A10, A11, A13, CARD_2: 76;

            end;

              suppose (w .outDegree() ) is finite;

              then

              reconsider m = (w0 .outDegree() ), n = (w .outDegree() ) as Nat by A9;

              (m + 1) = (m +` 1)

              .= (n +` 1) by A10

              .= (n + 1);

              hence thesis;

            end;

          end;

          per cases by ORDINAL1: 16;

            suppose

             A14: ((v0 .outDegree() ) +` 1) c= (v1 .outDegree() );

            now

              let w be Vertex of H;

              per cases by A3, XBOOLE_0:def 3;

                suppose w in ( the_Vertices_of G);

                then

                reconsider w0 = w as Vertex of G;

                

                 A15: (w .outDegree() ) c= ((w0 .outDegree() ) +` 1) by GLIBPRE0: 60;

                (w0 .outDegree() ) c= (v0 .outDegree() ) & 1 c= 1 by A2;

                then ((w0 .outDegree() ) +` 1) c= ((v0 .outDegree() ) +` 1) by CARD_2: 83;

                then (w .outDegree() ) c= ((v0 .outDegree() ) +` 1) by A15, XBOOLE_1: 1;

                hence (w .outDegree() ) c= (v1 .outDegree() ) by A14, XBOOLE_1: 1;

              end;

                suppose w in {v};

                hence (w .outDegree() ) c= (v1 .outDegree() ) by TARSKI:def 1;

              end;

            end;

            hence thesis;

          end;

            suppose

             A16: (v1 .outDegree() ) in ((v0 .outDegree() ) +` 1) & (v9 .outDegree() ) = ((v0 .outDegree() ) +` 1);

            now

              let w be Vertex of H;

              per cases by A3, XBOOLE_0:def 3;

                suppose w in ( the_Vertices_of G);

                then

                reconsider w0 = w as Vertex of G;

                

                 A17: (w .outDegree() ) c= ((w0 .outDegree() ) +` 1) by GLIBPRE0: 60;

                (w0 .outDegree() ) c= (v0 .outDegree() ) & 1 c= 1 by A2;

                then ((w0 .outDegree() ) +` 1) c= ((v0 .outDegree() ) +` 1) by CARD_2: 83;

                hence (w .outDegree() ) c= (v9 .outDegree() ) by A16, A17, XBOOLE_1: 1;

              end;

                suppose w in {v};

                then w = v1 by TARSKI:def 1;

                hence (w .outDegree() ) c= (v9 .outDegree() ) by A16, ORDINAL1:def 2;

              end;

            end;

            hence thesis;

          end;

            suppose

             A18: (v1 .outDegree() ) in ((v0 .outDegree() ) +` 1) & (v9 .outDegree() ) <> ((v0 .outDegree() ) +` 1) & for w0 be Vertex of G, w be Vertex of H st w0 = w & (w .outDegree() ) = ((w0 .outDegree() ) +` 1) holds ((w0 .outDegree() ) +` 1) c= (v0 .outDegree() );

            then

             A19: (v9 .outDegree() ) = (v0 .outDegree() ) by A4;

            now

              let w be Vertex of H;

              per cases by A3, XBOOLE_0:def 3;

                suppose w in ( the_Vertices_of G);

                then

                reconsider w0 = w as Vertex of G;

                per cases ;

                  suppose (w .outDegree() ) = ((w0 .outDegree() ) +` 1);

                  hence (w .outDegree() ) c= (v9 .outDegree() ) by A18, A19;

                end;

                  suppose (w .outDegree() ) <> ((w0 .outDegree() ) +` 1);

                  then (w .outDegree() ) = (w0 .outDegree() ) by A4;

                  hence (w .outDegree() ) c= (v9 .outDegree() ) by A2, A19;

                end;

              end;

                suppose w in {v};

                then w = v1 by TARSKI:def 1;

                hence (w .outDegree() ) c= (v9 .outDegree() ) by A18, A19, Lm7;

              end;

            end;

            hence thesis;

          end;

            suppose

             A20: (v1 .outDegree() ) c= ((v0 .outDegree() ) +` 1) & (v9 .outDegree() ) <> ((v0 .outDegree() ) +` 1) & not for w0 be Vertex of G, w be Vertex of H st w0 = w & (w .outDegree() ) = ((w0 .outDegree() ) +` 1) holds (w .outDegree() ) = ((w0 .outDegree() ) +` 1) & ((w0 .outDegree() ) +` 1) c= (v0 .outDegree() );

            consider w0 be Vertex of G, w be Vertex of H such that

             A21: w0 = w & (w .outDegree() ) = ((w0 .outDegree() ) +` 1) and

             A22: not ((w0 .outDegree() ) +` 1) c= (v0 .outDegree() ) by A20;

            (v0 .outDegree() ) in (w .outDegree() ) by A21, A22, ORDINAL1: 16;

            then (v0 .outDegree() ) c= (w .outDegree() ) & (v0 .outDegree() ) <> (w .outDegree() ) by ORDINAL1: 16;

            then

             A23: ((v0 .outDegree() ) +` 1) c= (w .outDegree() ) by Lm1;

            now

              let u be Vertex of H;

              per cases by A3, XBOOLE_0:def 3;

                suppose u in ( the_Vertices_of G);

                then

                reconsider u0 = u as Vertex of G;

                

                 A24: (u .outDegree() ) c= ((u0 .outDegree() ) +` 1) by GLIBPRE0: 60;

                (u0 .outDegree() ) c= (v0 .outDegree() ) & 1 c= 1 by A2;

                then ((u0 .outDegree() ) +` 1) c= ((v0 .outDegree() ) +` 1) by CARD_2: 83;

                then ((u0 .outDegree() ) +` 1) c= (w .outDegree() ) by A23, XBOOLE_1: 1;

                hence (u .outDegree() ) c= (w .outDegree() ) by A24, XBOOLE_1: 1;

              end;

                suppose u in {v};

                then u = v1 by TARSKI:def 1;

                hence (u .outDegree() ) c= (w .outDegree() ) by A20, A23, XBOOLE_1: 1;

              end;

            end;

            hence thesis;

          end;

        end;

          suppose not ( not v in ( the_Vertices_of G) & V c= ( the_Vertices_of G));

          then G == H by GLIB_007:def 4;

          hence thesis by Th85;

        end;

      end;

    end

    theorem :: GLIB_013:87

    for G be locally-finite with_max_degree _Graph, n be Nat holds (G .maxDegree() ) = n iff ex v be Vertex of G st (v .degree() ) = n & for w be Vertex of G holds (w .degree() ) <= (v .degree() )

    proof

      let G be locally-finite with_max_degree _Graph, n be Nat;

      hereby

        assume (G .maxDegree() ) = n;

        then

        consider v be Vertex of G such that

         A1: (v .degree() ) = n and

         A2: for w be Vertex of G holds (w .degree() ) c= (v .degree() ) by Th79;

        take v;

        thus (v .degree() ) = n by A1;

        let w be Vertex of G;

        ( Segm (w .degree() )) c= ( Segm (v .degree() )) by A2;

        hence (w .degree() ) <= (v .degree() ) by NAT_1: 39;

      end;

      given v be Vertex of G such that

       A3: (v .degree() ) = n and

       A4: for w be Vertex of G holds (w .degree() ) <= (v .degree() );

      now

        let w be Vertex of G;

        ( Segm (w .degree() )) c= ( Segm (v .degree() )) by A4, NAT_1: 39;

        hence (w .degree() ) c= (v .degree() );

      end;

      hence thesis by A3, Th48;

    end;

    theorem :: GLIB_013:88

    for G be locally-finite with_max_in_degree _Graph, n be Nat holds (G .maxInDegree() ) = n iff ex v be Vertex of G st (v .inDegree() ) = n & for w be Vertex of G holds (w .inDegree() ) <= (v .inDegree() )

    proof

      let G be locally-finite with_max_in_degree _Graph, n be Nat;

      hereby

        assume (G .maxInDegree() ) = n;

        then

        consider v be Vertex of G such that

         A1: (v .inDegree() ) = n and

         A2: for w be Vertex of G holds (w .inDegree() ) c= (v .inDegree() ) by Th80;

        take v;

        thus (v .inDegree() ) = n by A1;

        let w be Vertex of G;

        ( Segm (w .inDegree() )) c= ( Segm (v .inDegree() )) by A2;

        hence (w .inDegree() ) <= (v .inDegree() ) by NAT_1: 39;

      end;

      given v be Vertex of G such that

       A3: (v .inDegree() ) = n and

       A4: for w be Vertex of G holds (w .inDegree() ) <= (v .inDegree() );

      now

        let w be Vertex of G;

        ( Segm (w .inDegree() )) c= ( Segm (v .inDegree() )) by A4, NAT_1: 39;

        hence (w .inDegree() ) c= (v .inDegree() );

      end;

      hence thesis by A3, Th49;

    end;

    theorem :: GLIB_013:89

    for G be locally-finite with_max_out_degree _Graph, n be Nat holds (G .maxOutDegree() ) = n iff ex v be Vertex of G st (v .outDegree() ) = n & for w be Vertex of G holds (w .outDegree() ) <= (v .outDegree() )

    proof

      let G be locally-finite with_max_out_degree _Graph, n be Nat;

      hereby

        assume (G .maxOutDegree() ) = n;

        then

        consider v be Vertex of G such that

         A1: (v .outDegree() ) = n and

         A2: for w be Vertex of G holds (w .outDegree() ) c= (v .outDegree() ) by Th81;

        take v;

        thus (v .outDegree() ) = n by A1;

        let w be Vertex of G;

        ( Segm (w .outDegree() )) c= ( Segm (v .outDegree() )) by A2;

        hence (w .outDegree() ) <= (v .outDegree() ) by NAT_1: 39;

      end;

      given v be Vertex of G such that

       A3: (v .outDegree() ) = n and

       A4: for w be Vertex of G holds (w .outDegree() ) <= (v .outDegree() );

      now

        let w be Vertex of G;

        ( Segm (w .outDegree() )) c= ( Segm (v .outDegree() )) by A4, NAT_1: 39;

        hence (w .outDegree() ) c= (v .outDegree() );

      end;

      hence thesis by A3, Th50;

    end;

    theorem :: GLIB_013:90

    for c be Cardinal, G be _trivialc -edge _Graph holds (G .maxInDegree() ) = c & (G .minInDegree() ) = c & (G .maxOutDegree() ) = c & (G .minOutDegree() ) = c & (G .maxDegree() ) = (c +` c) & (G .minDegree() ) = (c +` c)

    proof

      let c be Cardinal, G be _trivialc -edge _Graph;

      set v = the Vertex of G;

      now

        let w be Vertex of G;

        (w .inDegree() ) = (G .size() ) & (v .inDegree() ) = (G .size() ) by GLIBPRE0: 27;

        hence (w .inDegree() ) c= (v .inDegree() );

      end;

      

      hence (G .maxInDegree() ) = (G .size() ) by Th49, GLIBPRE0: 27

      .= c by Def4;

      now

        let w be Vertex of G;

        (w .inDegree() ) = (G .size() ) & (v .inDegree() ) = (G .size() ) by GLIBPRE0: 27;

        hence (v .inDegree() ) c= (w .inDegree() );

      end;

      

      hence (G .minInDegree() ) = (G .size() ) by Th37, GLIBPRE0: 27

      .= c by Def4;

      now

        let w be Vertex of G;

        (w .outDegree() ) = (G .size() ) & (v .outDegree() ) = (G .size() ) by GLIBPRE0: 27;

        hence (w .outDegree() ) c= (v .outDegree() );

      end;

      

      hence (G .maxOutDegree() ) = (G .size() ) by Th50, GLIBPRE0: 27

      .= c by Def4;

      now

        let w be Vertex of G;

        (w .outDegree() ) = (G .size() ) & (v .outDegree() ) = (G .size() ) by GLIBPRE0: 27;

        hence (v .outDegree() ) c= (w .outDegree() );

      end;

      

      hence (G .minOutDegree() ) = (G .size() ) by Th38, GLIBPRE0: 27

      .= c by Def4;

      now

        let w be Vertex of G;

        (w .degree() ) = ((G .size() ) +` (G .size() )) & (v .degree() ) = ((G .size() ) +` (G .size() )) by GLIBPRE0: 27;

        hence (w .degree() ) c= (v .degree() );

      end;

      

      hence (G .maxDegree() ) = ((G .size() ) +` (G .size() )) by Th48, GLIBPRE0: 27

      .= ((G .size() ) +` c) by Def4

      .= (c +` c) by Def4;

      now

        let w be Vertex of G;

        (w .degree() ) = ((G .size() ) +` (G .size() )) & (v .degree() ) = ((G .size() ) +` (G .size() )) by GLIBPRE0: 27;

        hence (v .degree() ) c= (w .degree() );

      end;

      

      hence (G .minDegree() ) = ((G .size() ) +` (G .size() )) by Th36, GLIBPRE0: 27

      .= ((G .size() ) +` c) by Def4

      .= (c +` c) by Def4;

    end;

    definition

      let G be _Graph, v be Vertex of G;

      :: GLIB_013:def15

      attr v is with_min_degree means (v .degree() ) = (G .minDegree() );

      :: GLIB_013:def16

      attr v is with_min_in_degree means (v .inDegree() ) = (G .minInDegree() );

      :: GLIB_013:def17

      attr v is with_min_out_degree means (v .outDegree() ) = (G .minOutDegree() );

      :: GLIB_013:def18

      attr v is with_max_degree means (v .degree() ) = (G .supDegree() );

      :: GLIB_013:def19

      attr v is with_max_in_degree means (v .inDegree() ) = (G .supInDegree() );

      :: GLIB_013:def20

      attr v is with_max_out_degree means (v .outDegree() ) = (G .supOutDegree() );

    end

    theorem :: GLIB_013:91

    for G be _Graph, v,w be Vertex of G st v is with_min_degree holds (v .degree() ) c= (w .degree() )

    proof

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

      assume v is with_min_degree;

      then (v .degree() ) = (G .minDegree() );

      then

      consider v0 be Vertex of G such that

       A1: (v0 .degree() ) = (v .degree() ) and

       A2: for u be Vertex of G holds (v0 .degree() ) c= (u .degree() ) by Th36;

      thus thesis by A1, A2;

    end;

    theorem :: GLIB_013:92

    

     Th92: for G be _Graph, v,w be Vertex of G st v is with_min_in_degree holds (v .inDegree() ) c= (w .inDegree() )

    proof

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

      assume v is with_min_in_degree;

      then (v .inDegree() ) = (G .minInDegree() );

      then

      consider v0 be Vertex of G such that

       A1: (v0 .inDegree() ) = (v .inDegree() ) and

       A2: for u be Vertex of G holds (v0 .inDegree() ) c= (u .inDegree() ) by Th37;

      thus thesis by A1, A2;

    end;

    theorem :: GLIB_013:93

    

     Th93: for G be _Graph, v,w be Vertex of G st v is with_min_out_degree holds (v .outDegree() ) c= (w .outDegree() )

    proof

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

      assume v is with_min_out_degree;

      then (v .outDegree() ) = (G .minOutDegree() );

      then

      consider v0 be Vertex of G such that

       A1: (v0 .outDegree() ) = (v .outDegree() ) and

       A2: for u be Vertex of G holds (v0 .outDegree() ) c= (u .outDegree() ) by Th38;

      thus thesis by A1, A2;

    end;

    theorem :: GLIB_013:94

    for G be _Graph, v,w be Vertex of G st w is with_max_degree holds (v .degree() ) c= (w .degree() )

    proof

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

      assume w is with_max_degree;

      then (w .degree() ) = (G .supDegree() );

      then

      consider v0 be Vertex of G such that

       A1: (v0 .degree() ) = (w .degree() ) and

       A2: for u be Vertex of G holds (u .degree() ) c= (v0 .degree() ) by Th79, Lm3;

      thus thesis by A1, A2;

    end;

    theorem :: GLIB_013:95

    

     Th95: for G be _Graph, v,w be Vertex of G st w is with_max_in_degree holds (v .inDegree() ) c= (w .inDegree() )

    proof

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

      assume w is with_max_in_degree;

      then (w .inDegree() ) = (G .supInDegree() );

      then

      consider v0 be Vertex of G such that

       A1: (v0 .inDegree() ) = (w .inDegree() ) and

       A2: for u be Vertex of G holds (u .inDegree() ) c= (v0 .inDegree() ) by Th80, Lm4;

      thus thesis by A1, A2;

    end;

    theorem :: GLIB_013:96

    

     Th96: for G be _Graph, v,w be Vertex of G st w is with_max_out_degree holds (v .outDegree() ) c= (w .outDegree() )

    proof

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

      assume w is with_max_out_degree;

      then (w .outDegree() ) = (G .supOutDegree() );

      then

      consider v0 be Vertex of G such that

       A1: (v0 .outDegree() ) = (w .outDegree() ) and

       A2: for u be Vertex of G holds (u .outDegree() ) c= (v0 .outDegree() ) by Th81, Lm5;

      thus thesis by A1, A2;

    end;

    registration

      let G be _Graph;

      cluster with_min_degree for Vertex of G;

      existence

      proof

        consider v be Vertex of G such that

         A1: (v .degree() ) = (G .minDegree() ) and for w be Vertex of G holds (v .degree() ) c= (w .degree() ) by Th36;

        take v;

        thus thesis by A1;

      end;

      cluster with_min_in_degree for Vertex of G;

      existence

      proof

        consider v be Vertex of G such that

         A2: (v .inDegree() ) = (G .minInDegree() ) and for w be Vertex of G holds (v .inDegree() ) c= (w .inDegree() ) by Th37;

        take v;

        thus thesis by A2;

      end;

      cluster with_min_out_degree for Vertex of G;

      existence

      proof

        consider v be Vertex of G such that

         A3: (v .outDegree() ) = (G .minOutDegree() ) and for w be Vertex of G holds (v .outDegree() ) c= (w .outDegree() ) by Th38;

        take v;

        thus thesis by A3;

      end;

      cluster with_min_in_degree with_min_out_degree -> with_min_degree for Vertex of G;

      coherence

      proof

        let v be Vertex of G;

        assume

         A4: v is with_min_in_degree with_min_out_degree;

        now

          let w be Vertex of G;

          (v .inDegree() ) c= (w .inDegree() ) & (v .outDegree() ) c= (w .outDegree() ) by A4, Th92, Th93;

          hence (v .degree() ) c= (w .degree() ) by CARD_2: 83;

        end;

        hence thesis by Th36;

      end;

      cluster with_max_in_degree with_max_out_degree -> with_max_degree for Vertex of G;

      coherence

      proof

        let w be Vertex of G;

        assume

         A5: w is with_max_in_degree with_max_out_degree;

        now

          let v be Vertex of G;

          (v .inDegree() ) c= (w .inDegree() ) & (v .outDegree() ) c= (w .outDegree() ) by A5, Th95, Th96;

          hence (v .degree() ) c= (w .degree() ) by CARD_2: 83;

        end;

        hence thesis by Th48;

      end;

      cluster isolated -> with_min_degree with_min_in_degree with_min_out_degree for Vertex of G;

      coherence

      proof

        let v be Vertex of G;

        assume

         A6: v is isolated;

        then (G .minDegree() ) = 0 & (G .minInDegree() ) = 0 & (G .minOutDegree() ) = 0 by Th46;

        hence thesis by A6, GLIBPRE0: 35, GLIBPRE0: 34;

      end;

    end

    theorem :: GLIB_013:97

    

     Th97: for G be _Graph holds G is with_max_degree iff ex v be Vertex of G st v is with_max_degree

    proof

      let G be _Graph;

      hereby

        assume G is with_max_degree;

        then

        consider v be Vertex of G such that

         A1: (v .degree() ) = (G .supDegree() ) and for w be Vertex of G holds (w .degree() ) c= (v .degree() ) by Th79;

        take v;

        thus v is with_max_degree by A1;

      end;

      thus thesis by Lm3;

    end;

    theorem :: GLIB_013:98

    

     Th98: for G be _Graph holds G is with_max_in_degree iff ex v be Vertex of G st v is with_max_in_degree

    proof

      let G be _Graph;

      hereby

        assume G is with_max_in_degree;

        then

        consider v be Vertex of G such that

         A1: (v .inDegree() ) = (G .supInDegree() ) and for w be Vertex of G holds (w .inDegree() ) c= (v .inDegree() ) by Th80;

        take v;

        thus v is with_max_in_degree by A1;

      end;

      thus thesis by Lm4;

    end;

    theorem :: GLIB_013:99

    

     Th99: for G be _Graph holds G is with_max_out_degree iff ex v be Vertex of G st v is with_max_out_degree

    proof

      let G be _Graph;

      hereby

        assume G is with_max_out_degree;

        then

        consider v be Vertex of G such that

         A1: (v .outDegree() ) = (G .supOutDegree() ) and for w be Vertex of G holds (w .outDegree() ) c= (v .outDegree() ) by Th81;

        take v;

        thus v is with_max_out_degree by A1;

      end;

      thus thesis by Lm5;

    end;

    registration

      let G be with_max_degree _Graph;

      cluster with_max_degree for Vertex of G;

      existence by Th97;

    end

    registration

      let G be with_max_in_degree _Graph;

      cluster with_max_in_degree for Vertex of G;

      existence by Th98;

    end

    registration

      let G be with_max_out_degree _Graph;

      cluster with_max_out_degree for Vertex of G;

      existence by Th99;

    end