glib_000.miz



    begin

    registration

      cluster finite NAT -defined for Function;

      existence

      proof

        take {} ;

        thus {} is finite;

        thus ( dom {} ) c= NAT ;

      end;

    end

    definition

      mode GraphStruct is finite NAT -defined Function;

    end

    definition

      :: GLIB_000:def1

      func VertexSelector -> Element of NAT equals 1;

      coherence ;

      :: GLIB_000:def2

      func EdgeSelector -> Element of NAT equals 2;

      coherence ;

      :: GLIB_000:def3

      func SourceSelector -> Element of NAT equals 3;

      coherence ;

      :: GLIB_000:def4

      func TargetSelector -> Element of NAT equals 4;

      coherence ;

    end

    definition

      :: GLIB_000:def5

      func _GraphSelectors -> non empty Subset of NAT equals { VertexSelector , EdgeSelector , SourceSelector , TargetSelector };

      coherence ;

    end

    definition

      let G be GraphStruct;

      :: GLIB_000:def6

      func the_Vertices_of G -> set equals (G . VertexSelector );

      coherence ;

      :: GLIB_000:def7

      func the_Edges_of G -> set equals (G . EdgeSelector );

      coherence ;

      :: GLIB_000:def8

      func the_Source_of G -> set equals (G . SourceSelector );

      coherence ;

      :: GLIB_000:def9

      func the_Target_of G -> set equals (G . TargetSelector );

      coherence ;

    end

    definition

      let G be GraphStruct;

      :: GLIB_000:def10

      attr G is [Graph-like] means

      : Def10: VertexSelector in ( dom G) & EdgeSelector in ( dom G) & SourceSelector in ( dom G) & TargetSelector in ( dom G) & ( the_Vertices_of G) is non empty set & ( the_Source_of G) is Function of ( the_Edges_of G), ( the_Vertices_of G) & ( the_Target_of G) is Function of ( the_Edges_of G), ( the_Vertices_of G);

    end

    registration

      cluster [Graph-like] for GraphStruct;

      existence

      proof

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

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

        set G = <*V, E, S, S*>;

        ( len G) = 4 by FINSEQ_4: 76;

        then

         A1: ( dom G) = ( Seg 4) by FINSEQ_1:def 3;

        reconsider G as GraphStruct;

        

         A2: SourceSelector in ( dom G) & TargetSelector in ( dom G) by A1, FINSEQ_1: 1;

        

         A3: ( the_Vertices_of G) = V & ( the_Edges_of G) = E by FINSEQ_4: 76;

        

         A4: ( the_Source_of G) = S & ( the_Target_of G) = S by FINSEQ_4: 76;

         VertexSelector in ( dom G) & EdgeSelector in ( dom G) by A1, FINSEQ_1: 1;

        then G is [Graph-like] by A3, A4, A2;

        hence thesis;

      end;

    end

    definition

      mode _Graph is [Graph-like] GraphStruct;

    end

    registration

      let G be _Graph;

      cluster ( the_Vertices_of G) -> non empty;

      coherence by Def10;

    end

    definition

      let G be _Graph;

      :: original: the_Source_of

      redefine

      func the_Source_of G -> Function of ( the_Edges_of G), ( the_Vertices_of G) ;

      coherence by Def10;

      :: original: the_Target_of

      redefine

      func the_Target_of G -> Function of ( the_Edges_of G), ( the_Vertices_of G) ;

      coherence by Def10;

    end

    definition

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

      :: GLIB_000:def11

      func createGraph (V,E,S,T) -> _Graph equals <*V, E, S, T*>;

      coherence

      proof

        set G = <*V, E, S, T*>;

        ( len G) = 4 by FINSEQ_4: 76;

        then

         A1: ( dom G) = ( Seg 4) by FINSEQ_1:def 3;

        reconsider G as GraphStruct;

        

         A2: SourceSelector in ( dom G) & TargetSelector in ( dom G) by A1, FINSEQ_1: 1;

        

         A3: ( the_Vertices_of G) = V & ( the_Edges_of G) = E by FINSEQ_4: 76;

        

         A4: ( the_Source_of G) = S & ( the_Target_of G) = T by FINSEQ_4: 76;

         VertexSelector in ( dom G) & EdgeSelector in ( dom G) by A1, FINSEQ_1: 1;

        hence thesis by A3, A4, A2, Def10;

      end;

    end

    definition

      let G be GraphStruct, n be Nat, x be set;

      :: GLIB_000:def12

      func G .set (n,x) -> GraphStruct equals (G +* (n .--> x));

      coherence

      proof

        set IT = (G +* (n .--> x));

        n in NAT by ORDINAL1:def 12;

        then

         A2: {n} c= NAT by ZFMISC_1: 31;

        ( dom IT) = (( dom G) \/ ( dom (n .--> x))) & ( dom G) c= NAT by FUNCT_4:def 1;

        then ( dom IT) c= NAT by A2, XBOOLE_1: 8;

        hence thesis by RELAT_1:def 18;

      end;

    end

    

     Lm1: for GS be GraphStruct holds GS is [Graph-like] iff _GraphSelectors c= ( dom GS) & ( the_Vertices_of GS) is non empty & ( the_Source_of GS) is Function of ( the_Edges_of GS), ( the_Vertices_of GS) & ( the_Target_of GS) is Function of ( the_Edges_of GS), ( the_Vertices_of GS)

    proof

      let GS be GraphStruct;

      now

        thus VertexSelector in ( dom GS) & EdgeSelector in ( dom GS) & SourceSelector in ( dom GS) & TargetSelector in ( dom GS) implies _GraphSelectors c= ( dom GS) by ENUMSET1:def 2;

        

         A1: VertexSelector in _GraphSelectors & EdgeSelector in _GraphSelectors by ENUMSET1:def 2;

        

         A2: SourceSelector in _GraphSelectors & TargetSelector in _GraphSelectors by ENUMSET1:def 2;

        assume _GraphSelectors c= ( dom GS);

        hence VertexSelector in ( dom GS) & EdgeSelector in ( dom GS) & SourceSelector in ( dom GS) & TargetSelector in ( dom GS) by A1, A2;

      end;

      hence thesis;

    end;

    registration

      let G be _Graph;

      cluster (G | _GraphSelectors ) -> [Graph-like];

      coherence

      proof

        now

          let x be object;

          assume x in _GraphSelectors ;

          then x = VertexSelector or x = EdgeSelector or x = SourceSelector or x = TargetSelector by ENUMSET1:def 2;

          hence x in ( dom G) by Def10;

        end;

        then

         A1: _GraphSelectors c= ( dom G);

        set G2 = (G | _GraphSelectors );

         VertexSelector in _GraphSelectors by ENUMSET1:def 2;

        then

         A2: ( the_Vertices_of G2) = ( the_Vertices_of G) by FUNCT_1: 49;

         EdgeSelector in _GraphSelectors by ENUMSET1:def 2;

        then

         A3: ( the_Edges_of G2) = ( the_Edges_of G) by FUNCT_1: 49;

         TargetSelector in _GraphSelectors by ENUMSET1:def 2;

        then

         A4: ( the_Target_of G2) = ( the_Target_of G) by FUNCT_1: 49;

         SourceSelector in _GraphSelectors by ENUMSET1:def 2;

        then

         A5: ( the_Source_of G2) = ( the_Source_of G) by FUNCT_1: 49;

        ( dom G2) = (( dom G) /\ _GraphSelectors ) by RELAT_1: 61

        .= _GraphSelectors by A1, XBOOLE_1: 28;

        hence thesis by A2, A3, A5, A4, Lm1;

      end;

    end

    definition

      let G be _Graph, x,y,e be object;

      :: GLIB_000:def13

      pred e Joins x,y,G means e in ( the_Edges_of G) & ((( the_Source_of G) . e) = x & (( the_Target_of G) . e) = y or (( the_Source_of G) . e) = y & (( the_Target_of G) . e) = x);

    end

    definition

      let G be _Graph, x,y,e be object;

      :: GLIB_000:def14

      pred e DJoins x,y,G means e in ( the_Edges_of G) & (( the_Source_of G) . e) = x & (( the_Target_of G) . e) = y;

    end

    definition

      let G be _Graph, X,Y be set, e be object;

      :: GLIB_000:def15

      pred e SJoins X,Y,G means e in ( the_Edges_of G) & ((( the_Source_of G) . e) in X & (( the_Target_of G) . e) in Y or (( the_Source_of G) . e) in Y & (( the_Target_of G) . e) in X);

      :: GLIB_000:def16

      pred e DSJoins X,Y,G means e in ( the_Edges_of G) & (( the_Source_of G) . e) in X & (( the_Target_of G) . e) in Y;

    end

    definition

      let G be _Graph;

      :: GLIB_000:def17

      attr G is _finite means

      : Def17: ( the_Vertices_of G) is finite & ( the_Edges_of G) is finite;

      :: GLIB_000:def18

      attr G is loopless means

      : Def18: not ex e be object st e in ( the_Edges_of G) & (( the_Source_of G) . e) = (( the_Target_of G) . e);

      :: GLIB_000:def19

      attr G is _trivial means

      : Def19: ( card ( the_Vertices_of G)) = 1;

      :: GLIB_000:def20

      attr G is non-multi means

      : Def20: for e1,e2,v1,v2 be object holds e1 Joins (v1,v2,G) & e2 Joins (v1,v2,G) implies e1 = e2;

      :: GLIB_000:def21

      attr G is non-Dmulti means for e1,e2,v1,v2 be object holds e1 DJoins (v1,v2,G) & e2 DJoins (v1,v2,G) implies e1 = e2;

    end

    definition

      let G be _Graph;

      :: GLIB_000:def22

      attr G is simple means G is loopless & G is non-multi;

      :: GLIB_000:def23

      attr G is Dsimple means G is loopless & G is non-Dmulti;

    end

    

     Lm2: for G be _Graph holds ( the_Edges_of G) = {} implies G is simple

    proof

      let G be _Graph;

      assume

       A1: ( the_Edges_of G) = {} ;

      then

       A2: G is loopless;

      for e1,e2,v1,v2 be object holds e1 Joins (v1,v2,G) & e2 Joins (v1,v2,G) implies e1 = e2 by A1;

      then G is non-multi;

      hence thesis by A2;

    end;

    registration

      cluster non-multi -> non-Dmulti for _Graph;

      coherence

      proof

        let G be _Graph;

        assume

         A1: G is non-multi;

        now

          let e1,e2,v1,v2 be object;

          assume e1 DJoins (v1,v2,G) & e2 DJoins (v1,v2,G);

          then e1 Joins (v1,v2,G) & e2 Joins (v1,v2,G);

          hence e1 = e2 by A1;

        end;

        hence thesis;

      end;

      cluster simple -> loopless non-multi for _Graph;

      coherence ;

      cluster loopless non-multi -> simple for _Graph;

      coherence ;

      cluster loopless non-Dmulti -> Dsimple for _Graph;

      coherence ;

      cluster Dsimple -> loopless non-Dmulti for _Graph;

      coherence ;

      cluster _trivial loopless -> _finite for _Graph;

      coherence

      proof

        let G be _Graph;

        assume that

         A2: G is _trivial and

         A3: G is loopless;

        ( card ( the_Vertices_of G)) = 1 by A2;

        then

        consider v be object such that

         A4: ( the_Vertices_of G) = {v} by CARD_2: 42;

        now

          per cases ;

            suppose ( the_Edges_of G) is empty;

            hence ( the_Edges_of G) is finite;

          end;

            suppose ( the_Edges_of G) is non empty;

            then

            consider e be object such that

             A5: e in ( the_Edges_of G) by XBOOLE_0:def 1;

            (( the_Target_of G) . e) in ( the_Vertices_of G) by A5, FUNCT_2: 5;

            then

             A6: (( the_Target_of G) . e) = v by A4, TARSKI:def 1;

            (( the_Source_of G) . e) in ( the_Vertices_of G) by A5, FUNCT_2: 5;

            then (( the_Source_of G) . e) = v by A4, TARSKI:def 1;

            hence ( the_Edges_of G) is finite by A3, A5, A6;

          end;

        end;

        hence thesis by A4;

      end;

      cluster _trivial non-Dmulti -> _finite for _Graph;

      coherence

      proof

        let G be _Graph;

        assume that

         A7: G is _trivial and

         A8: G is non-Dmulti;

        ( card ( the_Vertices_of G)) = 1 by A7;

        then

        consider v be object such that

         A9: ( the_Vertices_of G) = {v} by CARD_2: 42;

        now

          set e1 = the Element of ( the_Edges_of G);

          set v1 = (( the_Source_of G) . e1), v2 = (( the_Target_of G) . e1);

          assume

           A10: not ( the_Edges_of G) is finite;

          then

           A11: ( the_Edges_of G) <> {} ;

          v2 in ( the_Vertices_of G) by A10, FUNCT_2: 5;

          then

           A12: v2 = v by A9, TARSKI:def 1;

          v1 in ( the_Vertices_of G) by A10, FUNCT_2: 5;

          then v1 = v by A9, TARSKI:def 1;

          then

           A13: e1 DJoins (v,v,G) by A11, A12;

          now

            let x be object;

            set v1 = (( the_Source_of G) . x), v2 = (( the_Target_of G) . x);

            hereby

              assume x in {e1};

              then x = e1 by TARSKI:def 1;

              hence x in ( the_Edges_of G) by A11;

            end;

            assume

             A14: x in ( the_Edges_of G);

            then v2 in ( the_Vertices_of G) by FUNCT_2: 5;

            then

             A15: v2 = v by A9, TARSKI:def 1;

            v1 in ( the_Vertices_of G) by A14, FUNCT_2: 5;

            then v1 = v by A9, TARSKI:def 1;

            then x DJoins (v,v,G) by A14, A15;

            then x = e1 by A8, A13;

            hence x in {e1} by TARSKI:def 1;

          end;

          hence contradiction by A10, TARSKI: 2;

        end;

        hence thesis by A9;

      end;

    end

    registration

      cluster _trivial simple for _Graph;

      existence

      proof

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

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

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

        take G;

        ( the_Vertices_of G) = {1} by FINSEQ_4: 76;

        then ( card ( the_Vertices_of G)) = 1 by CARD_1: 30;

        hence G is _trivial;

        ( the_Edges_of G) = {} by FINSEQ_4: 76;

        then for e1,e2,v1,v2 be object st e1 Joins (v1,v2,G) & e2 Joins (v1,v2,G) holds e1 = e2;

        then

         A1: G is non-multi;

         not ex e be object st e in ( the_Edges_of G) & (( the_Source_of G) . e) = (( the_Target_of G) . e) by FINSEQ_4: 76;

        then G is loopless;

        hence thesis by A1;

      end;

      cluster _finite non _trivial simple for _Graph;

      existence

      proof

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

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

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

        take G;

        

         A2: ( the_Edges_of G) = {} by FINSEQ_4: 76;

        

         A3: ( the_Vertices_of G) = {1, 2} by FINSEQ_4: 76;

        hence G is _finite by A2;

        ( card ( the_Vertices_of G)) <> 1 by A3, CARD_2: 57;

        hence G is non _trivial;

         not ex e be object st e in ( the_Edges_of G) & (( the_Source_of G) . e) = (( the_Target_of G) . e) by FINSEQ_4: 76;

        then

         A4: G is loopless;

        for e1,e2,v1,v2 be object st e1 Joins (v1,v2,G) & e2 Joins (v1,v2,G) holds e1 = e2 by A2;

        then G is non-multi;

        hence thesis by A4;

      end;

    end

    registration

      let G be _finite _Graph;

      cluster ( the_Vertices_of G) -> finite;

      coherence by Def17;

      cluster ( the_Edges_of G) -> finite;

      coherence by Def17;

    end

    registration

      let G be _trivial _Graph;

      cluster ( the_Vertices_of G) -> finite;

      coherence

      proof

        ( card ( the_Vertices_of G)) = 1 by Def19;

        hence thesis;

      end;

    end

    registration

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

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

      coherence by FINSEQ_4: 76;

    end

    registration

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

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

      coherence

      proof

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

        ( the_Edges_of G) = E by FINSEQ_4: 76;

        then for e1,e2,v1,v2 be object st e1 Joins (v1,v2,G) & e2 Joins (v1,v2,G) holds e1 = e2;

        then

         A1: G is non-multi;

         not ex e be object st e in ( the_Edges_of G) & (( the_Source_of G) . e) = (( the_Target_of G) . e) by FINSEQ_4: 76;

        then G is loopless;

        hence thesis by A1;

      end;

    end

    registration

      let v be set, E be set, S,T be Function of E, {v};

      cluster ( createGraph ( {v},E,S,T)) -> _trivial;

      coherence

      proof

        set G = ( createGraph ( {v},E,S,T));

        ( the_Vertices_of G) = {v} by FINSEQ_4: 76;

        then ( card ( the_Vertices_of G)) = 1 by CARD_1: 30;

        hence thesis;

      end;

    end

    definition

      let G be _Graph;

      :: GLIB_000:def24

      func G .order() -> Cardinal equals ( card ( the_Vertices_of G));

      coherence ;

    end

    definition

      let G be _finite _Graph;

      :: original: .order()

      redefine

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

      coherence

      proof

        (G .order() ) = ( card ( the_Vertices_of G));

        hence thesis;

      end;

    end

    definition

      let G be _Graph;

      :: GLIB_000:def25

      func G .size() -> Cardinal equals ( card ( the_Edges_of G));

      coherence ;

    end

    definition

      let G be _finite _Graph;

      :: original: .size()

      redefine

      func G .size() -> Element of NAT ;

      coherence

      proof

        (G .size() ) = ( card ( the_Edges_of G));

        hence thesis;

      end;

    end

    definition

      let G be _Graph, X be set;

      :: GLIB_000:def26

      func G .edgesInto (X) -> Subset of ( the_Edges_of G) means

      : Def26: for e be set holds e in it iff e in ( the_Edges_of G) & (( the_Target_of G) . e) in X;

      existence

      proof

        defpred P[ set] means (( the_Target_of G) . $1) in X;

        consider IT be Subset of ( the_Edges_of G) such that

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

        take IT;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let IT1,IT2 be Subset of ( the_Edges_of G) such that

         A2: for e be set holds e in IT1 iff e in ( the_Edges_of G) & (( the_Target_of G) . e) in X and

         A3: for e be set holds e in IT2 iff e in ( the_Edges_of G) & (( the_Target_of G) . e) in X;

        now

          let e be object;

          hereby

            assume

             A4: e in IT1;

            then (( the_Target_of G) . e) in X by A2;

            hence e in IT2 by A3, A4;

          end;

          assume

           A5: e in IT2;

          then (( the_Target_of G) . e) in X by A3;

          hence e in IT1 by A2, A5;

        end;

        hence thesis by TARSKI: 2;

      end;

      :: GLIB_000:def27

      func G .edgesOutOf (X) -> Subset of ( the_Edges_of G) means

      : Def27: for e be set holds e in it iff e in ( the_Edges_of G) & (( the_Source_of G) . e) in X;

      existence

      proof

        defpred P[ set] means (( the_Source_of G) . $1) in X;

        consider IT be Subset of ( the_Edges_of G) such that

         A6: for e be set holds e in IT iff e in ( the_Edges_of G) & P[e] from SUBSET_1:sch 1;

        take IT;

        thus thesis by A6;

      end;

      uniqueness

      proof

        let IT1,IT2 be Subset of ( the_Edges_of G) such that

         A7: for e be set holds e in IT1 iff e in ( the_Edges_of G) & (( the_Source_of G) . e) in X and

         A8: for e be set holds e in IT2 iff e in ( the_Edges_of G) & (( the_Source_of G) . e) in X;

        now

          let e be object;

          hereby

            assume

             A9: e in IT1;

            then (( the_Source_of G) . e) in X by A7;

            hence e in IT2 by A8, A9;

          end;

          assume

           A10: e in IT2;

          then (( the_Source_of G) . e) in X by A8;

          hence e in IT1 by A7, A10;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let G be _Graph, X be set;

      :: GLIB_000:def28

      func G .edgesInOut (X) -> Subset of ( the_Edges_of G) equals ((G .edgesInto X) \/ (G .edgesOutOf X));

      coherence ;

      :: GLIB_000:def29

      func G .edgesBetween (X) -> Subset of ( the_Edges_of G) equals ((G .edgesInto X) /\ (G .edgesOutOf X));

      coherence ;

    end

    definition

      let G be _Graph, X,Y be set;

      :: GLIB_000:def30

      func G .edgesBetween (X,Y) -> Subset of ( the_Edges_of G) means

      : Def30: for e be object holds e in it iff e SJoins (X,Y,G);

      existence

      proof

        defpred P[ object] means $1 SJoins (X,Y,G);

        consider IT be Subset of ( the_Edges_of G) such that

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

        take IT;

        let e be object;

        thus e in IT implies P[e] by A1;

        assume

         A2: e SJoins (X,Y,G);

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let IT1,IT2 be Subset of ( the_Edges_of G) such that

         A3: for e be object holds e in IT1 iff e SJoins (X,Y,G) and

         A4: for e be object holds e in IT2 iff e SJoins (X,Y,G);

        for e be object holds e in IT2 iff e in IT1 by A3, A4;

        hence thesis by TARSKI: 2;

      end;

      :: GLIB_000:def31

      func G .edgesDBetween (X,Y) -> Subset of ( the_Edges_of G) means

      : Def31: for e be object holds e in it iff e DSJoins (X,Y,G);

      existence

      proof

        defpred P[ object] means $1 DSJoins (X,Y,G);

        consider IT be Subset of ( the_Edges_of G) such that

         A5: for e be set holds e in IT iff e in ( the_Edges_of G) & P[e] from SUBSET_1:sch 1;

        take IT;

        let e be object;

        thus e in IT implies P[e] by A5;

        assume

         A6: e DSJoins (X,Y,G);

        thus thesis by A5, A6;

      end;

      uniqueness

      proof

        let IT1,IT2 be Subset of ( the_Edges_of G) such that

         A7: for e be object holds e in IT1 iff e DSJoins (X,Y,G) and

         A8: for e be object holds e in IT2 iff e DSJoins (X,Y,G);

        for e be object holds e in IT2 iff e in IT1 by A7, A8;

        hence thesis by TARSKI: 2;

      end;

    end

    scheme :: GLIB_000:sch1

    FinGraphOrderInd { P[ finite _Graph] } :

for G be _finite _Graph holds P[G]

      provided

       A1: for G be _finite _Graph st (G .order() ) = 1 holds P[G]

       and

       A2: for k be non zero Nat st (for Gk be _finite _Graph st (Gk .order() ) = k holds P[Gk]) holds for Gk1 be _finite _Graph st (Gk1 .order() ) = (k + 1) holds P[Gk1];

      defpred P2[ Nat] means for G be _finite _Graph st (G .order() ) = $1 holds P[G];

      

       A3: for k be non zero Nat st P2[k] holds P2[(k + 1)] by A2;

      let G be _finite _Graph;

      

       A4: (G .order() ) = (G .order() );

      

       A5: P2[1] by A1;

      for k be non zero Nat holds P2[k] from NAT_1:sch 10( A5, A3);

      hence thesis by A4;

    end;

    scheme :: GLIB_000:sch2

    FinGraphSizeInd { P[ finite _Graph] } :

for G be _finite _Graph holds P[G]

      provided

       A1: for G be _finite _Graph st (G .size() ) = 0 holds P[G]

       and

       A2: for k be Nat st (for Gk be _finite _Graph st (Gk .size() ) = k holds P[Gk]) holds for Gk1 be _finite _Graph st (Gk1 .size() ) = (k + 1) holds P[Gk1];

      defpred P2[ Nat] means for G be _finite _Graph st (G .size() ) = $1 holds P[G];

      

       A3: for k be Nat st P2[k] holds P2[(k + 1)] by A2;

      let G be _finite _Graph;

      

       A4: (G .size() ) = (G .size() );

      

       A5: P2[ 0 ] by A1;

      for k be Nat holds P2[k] from NAT_1:sch 2( A5, A3);

      hence thesis by A4;

    end;

    definition

      let G be _Graph;

      :: GLIB_000:def32

      mode Subgraph of G -> _Graph means

      : Def32: ( the_Vertices_of it ) c= ( the_Vertices_of G) & ( the_Edges_of it ) c= ( the_Edges_of G) & for e be set st e in ( the_Edges_of it ) holds (( the_Source_of it ) . e) = (( the_Source_of G) . e) & (( the_Target_of it ) . e) = (( the_Target_of G) . e);

      existence

      proof

        take G;

        thus thesis;

      end;

    end

    definition

      let G1 be _Graph, G2 be Subgraph of G1;

      :: original: the_Vertices_of

      redefine

      func the_Vertices_of G2 -> non empty Subset of ( the_Vertices_of G1) ;

      coherence by Def32;

      :: original: the_Edges_of

      redefine

      func the_Edges_of G2 -> Subset of ( the_Edges_of G1) ;

      coherence by Def32;

    end

    registration

      let G be _Graph;

      cluster _trivial simple for Subgraph of G;

      existence

      proof

        set v = the Element of ( the_Vertices_of G);

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

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

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

        

         A1: ( the_Vertices_of IT) = {v} & for e be set st e in ( the_Edges_of IT) holds (( the_Source_of IT) . e) = (( the_Source_of G) . e) & (( the_Target_of IT) . e) = (( the_Target_of G) . e) by FINSEQ_4: 76;

        ( the_Edges_of IT) = {} by FINSEQ_4: 76;

        then ( the_Edges_of IT) c= ( the_Edges_of G);

        then

        reconsider IT as Subgraph of G by A1, Def32;

        take IT;

        thus thesis;

      end;

    end

    

     Lm3: for G be _Graph holds G is Subgraph of G

    proof

      let G be _Graph;

      for e be set st e in ( the_Edges_of G) holds (( the_Source_of G) . e) = (( the_Source_of G) . e) & (( the_Target_of G) . e) = (( the_Target_of G) . e);

      hence thesis by Def32;

    end;

    

     Lm4: for G1 be _Graph, G2 be Subgraph of G1, x,y,e be object holds e Joins (x,y,G2) implies e Joins (x,y,G1)

    proof

      let G1 be _Graph, G2 be Subgraph of G1, x,y,e be object;

      assume

       A1: e Joins (x,y,G2);

      then

       A2: e in ( the_Edges_of G2);

      (( the_Source_of G2) . e) = x & (( the_Target_of G2) . e) = y or (( the_Source_of G2) . e) = y & (( the_Target_of G2) . e) = x by A1;

      then (( the_Source_of G1) . e) = x & (( the_Target_of G1) . e) = y or (( the_Source_of G1) . e) = y & (( the_Target_of G1) . e) = x by A2, Def32;

      hence thesis by A2;

    end;

    registration

      let G be _finite _Graph;

      cluster -> _finite for Subgraph of G;

      coherence

      proof

        let G2 be Subgraph of G;

        ( the_Vertices_of G2) is finite & ( the_Edges_of G2) is finite;

        hence thesis;

      end;

    end

    registration

      let G be loopless _Graph;

      cluster -> loopless for Subgraph of G;

      coherence

      proof

        let G2 be Subgraph of G;

        now

          given e be object such that

           A1: e in ( the_Edges_of G2) and

           A2: (( the_Source_of G2) . e) = (( the_Target_of G2) . e);

          (( the_Source_of G2) . e) = (( the_Source_of G) . e) & (( the_Target_of G2) . e) = (( the_Target_of G) . e) by A1, Def32;

          hence contradiction by A1, A2, Def18;

        end;

        hence thesis;

      end;

    end

    registration

      let G be _trivial _Graph;

      cluster -> _trivial for Subgraph of G;

      coherence

      proof

        let G2 be Subgraph of G;

        ( card ( the_Vertices_of G)) = 1 by Def19;

        then

        consider v be object such that

         A1: ( the_Vertices_of G) = {v} by CARD_2: 42;

        ( the_Vertices_of G2) = {v} by A1, ZFMISC_1: 33;

        then ( card ( the_Vertices_of G2)) = 1 by CARD_1: 30;

        hence thesis;

      end;

    end

    registration

      let G be non-multi _Graph;

      cluster -> non-multi for Subgraph of G;

      coherence

      proof

        let G2 be Subgraph of G;

        now

          let e1,e2,v1,v2 be object;

          assume e1 Joins (v1,v2,G2) & e2 Joins (v1,v2,G2);

          then e1 Joins (v1,v2,G) & e2 Joins (v1,v2,G) by Lm4;

          hence e1 = e2 by Def20;

        end;

        hence thesis;

      end;

    end

    definition

      let G1 be _Graph, G2 be Subgraph of G1;

      :: GLIB_000:def33

      attr G2 is spanning means

      : Def33: ( the_Vertices_of G2) = ( the_Vertices_of G1);

    end

    registration

      let G be _Graph;

      cluster spanning for Subgraph of G;

      existence

      proof

        reconsider G9 = G as Subgraph of G by Lm3;

        take G9;

        thus thesis;

      end;

    end

    definition

      let G1,G2 be _Graph;

      :: GLIB_000:def34

      pred G1 == G2 means ( the_Vertices_of G1) = ( the_Vertices_of G2) & ( the_Edges_of G1) = ( the_Edges_of G2) & ( the_Source_of G1) = ( the_Source_of G2) & ( the_Target_of G1) = ( the_Target_of G2);

      reflexivity ;

      symmetry ;

    end

    notation

      let G1,G2 be _Graph;

      antonym G1 != G2 for G1 == G2;

    end

    definition

      let G1,G2 be _Graph;

      :: GLIB_000:def35

      pred G1 c= G2 means G1 is Subgraph of G2;

      reflexivity by Lm3;

    end

    definition

      let G1,G2 be _Graph;

      :: GLIB_000:def36

      pred G1 c< G2 means G1 c= G2 & G1 != G2;

      irreflexivity ;

    end

    definition

      let G be _Graph, V,E be set;

      :: GLIB_000:def37

      mode inducedSubgraph of G,V,E -> Subgraph of G means

      : Def37: ( the_Vertices_of it ) = V & ( the_Edges_of it ) = E if V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V)

      otherwise it == G;

      existence

      proof

        hereby

          assume that

           A1: V is non empty Subset of ( the_Vertices_of G) and

           A2: E c= (G .edgesBetween V);

          reconsider E9 = E as Subset of ( the_Edges_of G) by A2, XBOOLE_1: 1;

          set S = (( the_Source_of G) | E9), T = (( the_Target_of G) | E9);

          reconsider V9 = V as non empty Subset of ( the_Vertices_of G) by A1;

          ( dom ( the_Target_of G)) = ( the_Edges_of G) by FUNCT_2:def 1;

          then

           A3: ( dom T) = E9 by RELAT_1: 62;

          now

            let e be object;

            assume

             A4: e in E9;

            then e in (G .edgesInto V) by A2, XBOOLE_0:def 4;

            then (( the_Target_of G) . e) in V by Def26;

            hence (T . e) in V by A4, FUNCT_1: 49;

          end;

          then

          reconsider T as Function of E9, V9 by A3, FUNCT_2: 3;

          ( dom ( the_Source_of G)) = ( the_Edges_of G) by FUNCT_2:def 1;

          then

           A5: ( dom S) = E9 by RELAT_1: 62;

          now

            let e be object;

            assume

             A6: e in E9;

            then e in (G .edgesOutOf V) by A2, XBOOLE_0:def 4;

            then (( the_Source_of G) . e) in V by Def27;

            hence (S . e) in V by A6, FUNCT_1: 49;

          end;

          then

          reconsider S as Function of E9, V9 by A5, FUNCT_2: 3;

          set IT = ( createGraph (V9,E9,S,T));

          

           A7: ( the_Edges_of IT) = E by FINSEQ_4: 76;

          ( the_Source_of IT) = S & ( the_Target_of IT) = T by FINSEQ_4: 76;

          then ( the_Vertices_of IT) = V & for e be set st e in ( the_Edges_of IT) holds (( the_Source_of IT) . e) = (( the_Source_of G) . e) & (( the_Target_of IT) . e) = (( the_Target_of G) . e) by A7, FINSEQ_4: 76, FUNCT_1: 49;

          then

          reconsider IT as Subgraph of G by A7, Def32;

          take IT;

          thus ( the_Vertices_of IT) = V & ( the_Edges_of IT) = E by FINSEQ_4: 76;

        end;

        G is Subgraph of G by Lm3;

        hence thesis;

      end;

      consistency ;

    end

    definition

      let G be _Graph, V be set;

      mode inducedSubgraph of G,V is inducedSubgraph of G, V, (G .edgesBetween V);

    end

    registration

      let G be _Graph, V be finite non empty Subset of ( the_Vertices_of G), E be finite Subset of (G .edgesBetween V);

      cluster -> _finite for inducedSubgraph of G, V, E;

      coherence by Def37;

    end

    registration

      let G be _Graph, v be Element of ( the_Vertices_of G), E be Subset of (G .edgesBetween {v});

      cluster -> _trivial for inducedSubgraph of G, {v}, E;

      coherence

      proof

        let IT be inducedSubgraph of G, {v}, E;

        ( the_Vertices_of IT) = {v} by Def37;

        then ( card ( the_Vertices_of IT)) = 1 by CARD_1: 30;

        hence thesis;

      end;

    end

    registration

      let G be _Graph, v be Element of ( the_Vertices_of G);

      cluster -> _finite _trivial for inducedSubgraph of G, {v}, {} ;

      coherence

      proof

        reconsider E = {} as finite Subset of (G .edgesBetween {v}) by XBOOLE_1: 2;

        let IT be inducedSubgraph of G, {v}, {} ;

        IT is inducedSubgraph of G, {v}, E;

        hence thesis;

      end;

    end

    registration

      let G be _Graph, V be non empty Subset of ( the_Vertices_of G);

      cluster -> simple for inducedSubgraph of G, V, {} ;

      coherence

      proof

        let IT be inducedSubgraph of G, V, {} ;

        reconsider E = {} as Subset of (G .edgesBetween V) by XBOOLE_1: 2;

        IT is inducedSubgraph of G, V, E;

        then ( the_Edges_of IT) = {} by Def37;

        hence thesis by Lm2;

      end;

    end

    

     Lm5: for G be _Graph, e,X be set holds e in ( the_Edges_of G) & (( the_Source_of G) . e) in X & (( the_Target_of G) . e) in X iff e in (G .edgesBetween X)

    proof

      let G be _Graph, e,X be set;

      hereby

        assume e in ( the_Edges_of G) & (( the_Source_of G) . e) in X & (( the_Target_of G) . e) in X;

        then e in (G .edgesInto X) & e in (G .edgesOutOf X) by Def26, Def27;

        hence e in (G .edgesBetween X) by XBOOLE_0:def 4;

      end;

      assume e in (G .edgesBetween X);

      then e in (G .edgesInto X) & e in (G .edgesOutOf X) by XBOOLE_0:def 4;

      hence thesis by Def26, Def27;

    end;

    

     Lm6: for G be _Graph holds ( the_Edges_of G) = (G .edgesBetween ( the_Vertices_of G))

    proof

      let G be _Graph;

      set EG = ( the_Edges_of G), SG = ( the_Source_of G), TG = ( the_Target_of G);

      now

        let x be object;

        hereby

          assume

           A1: x in EG;

          then (SG . x) in ( the_Vertices_of G) & (TG . x) in ( the_Vertices_of G) by FUNCT_2: 5;

          hence x in (G .edgesBetween ( the_Vertices_of G)) by A1, Lm5;

        end;

        assume x in (G .edgesBetween ( the_Vertices_of G));

        hence x in EG;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let G be _Graph, E be Subset of ( the_Edges_of G);

      cluster -> spanning for inducedSubgraph of G, ( the_Vertices_of G), E;

      coherence

      proof

        let G1 be inducedSubgraph of G, ( the_Vertices_of G), E;

        (G .edgesBetween ( the_Vertices_of G)) = ( the_Edges_of G) & ( the_Vertices_of G) c= ( the_Vertices_of G) by Lm6;

        then ( the_Vertices_of G1) = ( the_Vertices_of G) by Def37;

        hence thesis;

      end;

    end

    registration

      let G be _Graph;

      cluster -> spanning for inducedSubgraph of G, ( the_Vertices_of G), {} ;

      coherence

      proof

        let G1 be inducedSubgraph of G, ( the_Vertices_of G), {} ;

        ( the_Vertices_of G) c= ( the_Vertices_of G) & {} c= (G .edgesBetween ( the_Vertices_of G));

        then ( the_Vertices_of G1) = ( the_Vertices_of G) by Def37;

        hence thesis;

      end;

    end

    definition

      let G be _Graph, v be set;

      mode removeVertex of G,v is inducedSubgraph of G, (( the_Vertices_of G) \ {v});

    end

    definition

      let G be _Graph, V be set;

      mode removeVertices of G,V is inducedSubgraph of G, (( the_Vertices_of G) \ V);

    end

    definition

      let G be _Graph, e be set;

      mode removeEdge of G,e is inducedSubgraph of G, ( the_Vertices_of G), (( the_Edges_of G) \ {e});

    end

    definition

      let G be _Graph, E be set;

      mode removeEdges of G,E is inducedSubgraph of G, ( the_Vertices_of G), (( the_Edges_of G) \ E);

    end

    registration

      let G be _Graph, e be set;

      cluster -> spanning for removeEdge of G, e;

      coherence ;

    end

    registration

      let G be _Graph, E be set;

      cluster -> spanning for removeEdges of G, E;

      coherence ;

    end

    definition

      let G be _Graph;

      mode Vertex of G is Element of ( the_Vertices_of G);

    end

    definition

      let G be _Graph, v be Vertex of G;

      :: GLIB_000:def38

      func v .edgesIn() -> Subset of ( the_Edges_of G) equals (G .edgesInto {v});

      coherence ;

      :: GLIB_000:def39

      func v .edgesOut() -> Subset of ( the_Edges_of G) equals (G .edgesOutOf {v});

      coherence ;

      :: GLIB_000:def40

      func v .edgesInOut() -> Subset of ( the_Edges_of G) equals (G .edgesInOut {v});

      coherence ;

    end

    

     Lm7: for G be _Graph, v be Vertex of G, e be set holds e in (v .edgesIn() ) iff e in ( the_Edges_of G) & (( the_Target_of G) . e) = v

    proof

      let G be _Graph, v be Vertex of G, e be set;

      hereby

        assume

         A1: e in (v .edgesIn() );

        then (( the_Target_of G) . e) in {v} by Def26;

        hence e in ( the_Edges_of G) & (( the_Target_of G) . e) = v by A1, TARSKI:def 1;

      end;

      assume that

       A2: e in ( the_Edges_of G) and

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

      (( the_Target_of G) . e) in {v} by A3, TARSKI:def 1;

      hence thesis by A2, Def26;

    end;

    

     Lm8: for G be _Graph, v be Vertex of G, e be set holds e in (v .edgesOut() ) iff e in ( the_Edges_of G) & (( the_Source_of G) . e) = v

    proof

      let G be _Graph, v be Vertex of G, e be set;

      hereby

        assume

         A1: e in (v .edgesOut() );

        then (( the_Source_of G) . e) in {v} by Def27;

        hence e in ( the_Edges_of G) & (( the_Source_of G) . e) = v by A1, TARSKI:def 1;

      end;

      assume that

       A2: e in ( the_Edges_of G) and

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

      (( the_Source_of G) . e) in {v} by A3, TARSKI:def 1;

      hence thesis by A2, Def27;

    end;

    definition

      let G be _Graph, v be Vertex of G, e be object;

      :: GLIB_000:def41

      func v .adj (e) -> Vertex of G equals

      : Def41: (( the_Source_of G) . e) if e in ( the_Edges_of G) & (( the_Target_of G) . e) = v,

(( the_Target_of G) . e) if e in ( the_Edges_of G) & (( the_Source_of G) . e) = v & not (( the_Target_of G) . e) = v

      otherwise v;

      coherence by FUNCT_2: 5;

      consistency ;

    end

    definition

      let G be _Graph, v be Vertex of G;

      :: GLIB_000:def42

      func v .inDegree() -> Cardinal equals ( card (v .edgesIn() ));

      coherence ;

      :: GLIB_000:def43

      func v .outDegree() -> Cardinal equals ( card (v .edgesOut() ));

      coherence ;

    end

    definition

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

      :: original: .inDegree()

      redefine

      func v .inDegree() -> Element of NAT ;

      coherence

      proof

        (v .inDegree() ) = ( card (v .edgesIn() ));

        hence thesis;

      end;

      :: original: .outDegree()

      redefine

      func v .outDegree() -> Element of NAT ;

      coherence

      proof

        (v .outDegree() ) = ( card (v .edgesOut() ));

        hence thesis;

      end;

    end

    definition

      let G be _Graph, v be Vertex of G;

      :: GLIB_000:def44

      func v .degree() -> Cardinal equals ((v .inDegree() ) +` (v .outDegree() ));

      coherence ;

    end

    definition

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

      :: original: .degree()

      redefine

      :: GLIB_000:def45

      func v .degree() -> Element of NAT equals ((v .inDegree() ) + (v .outDegree() ));

      correctness

      proof

        (v .degree() ) = ( card ((v .inDegree() ) +^ (v .outDegree() ))) by CARD_2:def 1

        .= ( card ((v .inDegree() ) + (v .outDegree() ))) by CARD_2: 36

        .= ((v .inDegree() ) + (v .outDegree() ));

        hence thesis;

      end;

    end

    definition

      let G be _Graph, v be Vertex of G;

      :: GLIB_000:def46

      func v .inNeighbors() -> Subset of ( the_Vertices_of G) equals (( the_Source_of G) .: (v .edgesIn() ));

      coherence ;

      :: GLIB_000:def47

      func v .outNeighbors() -> Subset of ( the_Vertices_of G) equals (( the_Target_of G) .: (v .edgesOut() ));

      coherence ;

    end

    definition

      let G be _Graph, v be Vertex of G;

      :: GLIB_000:def48

      func v .allNeighbors() -> Subset of ( the_Vertices_of G) equals ((v .inNeighbors() ) \/ (v .outNeighbors() ));

      coherence ;

    end

    definition

      let G be _Graph, v be Vertex of G;

      :: GLIB_000:def49

      attr v is isolated means (v .edgesInOut() ) = {} ;

    end

    definition

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

      :: original: isolated

      redefine

      :: GLIB_000:def50

      attr v is isolated means (v .degree() ) = 0 ;

      compatibility

      proof

        hereby

          assume v is isolated;

          then

           A1: (v .edgesInOut() ) = {} ;

          then (v .inDegree() ) = 0 by CARD_1: 27, XBOOLE_1: 15;

          hence (v .degree() ) = 0 by A1, CARD_1: 27, XBOOLE_1: 15;

        end;

        assume

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

        then (v .edgesIn() ) = {} ;

        hence thesis by A2;

      end;

    end

    definition

      let G be _Graph, v be Vertex of G;

      :: GLIB_000:def51

      attr v is endvertex means ex e be object st (v .edgesInOut() ) = {e} & not e Joins (v,v,G);

    end

    definition

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

      :: original: endvertex

      redefine

      :: GLIB_000:def52

      attr v is endvertex means (v .degree() ) = 1;

      compatibility

      proof

        hereby

          assume v is endvertex;

          then

          consider e be object such that

           A1: (v .edgesInOut() ) = {e} and

           A2: not e Joins (v,v,G);

          now

            per cases by A1, ZFMISC_1: 37;

              suppose

               A3: (v .edgesIn() ) = {e} & (v .edgesOut() ) = {e};

              then e in (v .edgesOut() ) by TARSKI:def 1;

              then

               A4: (( the_Source_of G) . e) = v by Lm8;

              

               A5: e in (v .edgesIn() ) by A3, TARSKI:def 1;

              then (( the_Target_of G) . e) = v by Lm7;

              hence (v .degree() ) = 1 by A2, A5, A4;

            end;

              suppose (v .edgesIn() ) = {} & (v .edgesOut() ) = {e};

              hence (v .degree() ) = 1 by CARD_1: 30;

            end;

              suppose (v .edgesIn() ) = {e} & (v .edgesOut() ) = {} ;

              hence (v .degree() ) = 1 by CARD_1: 30;

            end;

          end;

          hence (v .degree() ) = 1;

        end;

        assume

         A6: (v .degree() ) = 1;

        now

          per cases ;

            suppose

             A7: ( card (v .edgesIn() )) = 0 ;

            then

            consider e be object such that

             A8: (v .edgesOut() ) = {e} by A6, CARD_2: 42;

            

             A9: (v .edgesIn() ) = {} by A7;

            then

             A10: not e Joins (v,v,G) by Lm7;

            (v .edgesInOut() ) = {e} by A9, A8;

            hence thesis by A10;

          end;

            suppose ( card (v .edgesIn() )) <> 0 ;

            then 0 < ( card (v .edgesIn() ));

            then

             A11: ( 0 + 1) <= ( card (v .edgesIn() )) by NAT_1: 13;

            ( card (v .edgesIn() )) <= 1 by A6, NAT_1: 11;

            then

             A12: ( card (v .edgesIn() )) = 1 by A11, XXREAL_0: 1;

            then

            consider e be object such that

             A13: (v .edgesIn() ) = {e} by CARD_2: 42;

            

             A14: (v .edgesOut() ) = {} by A6, A12;

            then

             A15: not e Joins (v,v,G) by Lm8;

            (v .edgesInOut() ) = {e} by A13, A14;

            hence thesis by A15;

          end;

        end;

        hence thesis;

      end;

    end

    

     LmNat: for F be ManySortedSet of NAT , n be object holds n is Nat iff n in ( dom F)

    proof

      let F be ManySortedSet of NAT , n be object;

      hereby

        assume n is Nat;

        then n in NAT by ORDINAL1:def 12;

        hence n in ( dom F) by PARTFUN1:def 2;

      end;

      assume n in ( dom F);

      hence n is Nat;

    end;

    definition

      let F be Function;

      :: GLIB_000:def53

      attr F is Graph-yielding means

      : Def53a: for x be object st x in ( dom F) holds (F . x) is _Graph;

    end

    definition

      let F be ManySortedSet of NAT ;

      :: original: Graph-yielding

      redefine

      :: GLIB_000:def54

      attr F is Graph-yielding means

      : Def53: for n be Nat holds (F . n) is _Graph;

      compatibility

      proof

        thus F is Graph-yielding implies for n be Nat holds (F . n) is _Graph by LmNat;

        assume

         A2: for n be Nat holds (F . n) is _Graph;

        let x be object;

        assume x in ( dom F);

        hence thesis by A2;

      end;

      :: GLIB_000:def55

      attr F is halting means ex n be Nat st (F . n) = (F . (n + 1));

    end

    definition

      let F be ManySortedSet of NAT ;

      :: GLIB_000:def56

      func F .Lifespan() -> Element of NAT means (F . it ) = (F . (it + 1)) & for n be Nat st (F . n) = (F . (n + 1)) holds it <= n if F is halting

      otherwise it = 0 ;

      existence

      proof

        defpred P[ Nat] means (F . $1) = (F . ($1 + 1));

        hereby

          assume F is halting;

          then

           A1: ex n be Nat st P[n];

          ex IT be Nat st P[IT] & for n be Nat st P[n] holds IT <= n from NAT_1:sch 5( A1);

          then

          consider IT be Nat such that

           A2: P[IT] & for n be Nat st P[n] holds IT <= n;

          IT in NAT by ORDINAL1:def 12;

          hence ex IT be Element of NAT st P[IT] & for n be Nat st P[n] holds IT <= n by A2;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be Element of NAT ;

        hereby

          assume F is halting;

          assume

           A3: (F . IT1) = (F . (IT1 + 1)) & for n be Nat st (F . n) = (F . (n + 1)) holds IT1 <= n;

          assume (F . IT2) = (F . (IT2 + 1)) & for n be Nat st (F . n) = (F . (n + 1)) holds IT2 <= n;

          then IT1 <= IT2 & IT2 <= IT1 by A3;

          hence IT1 = IT2 by XXREAL_0: 1;

        end;

        thus thesis;

      end;

      consistency ;

    end

    definition

      let F be ManySortedSet of NAT ;

      :: GLIB_000:def57

      func F .Result() -> set equals (F . (F .Lifespan() ));

      coherence ;

    end

    registration

      cluster empty -> Graph-yielding for Function;

      coherence ;

    end

    registration

      let G be _Graph;

      cluster ( NAT --> G) -> Graph-yielding;

      coherence

      proof

        set F = ( NAT --> G);

        

         A1: ( dom F) = NAT ;

        reconsider F as ManySortedSet of NAT ;

        let x be Nat;

        x in NAT by ORDINAL1:def 12;

        then (F . x) in ( rng F) by A1, FUNCT_1: 3;

        then (F . x) in {G} by FUNCOP_1: 8;

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      cluster Graph-yielding for ManySortedSet of NAT ;

      existence

      proof

        set G = the _Graph;

        set F = ( NAT --> G);

        reconsider F as ManySortedSet of NAT ;

        take F;

        thus thesis;

      end;

    end

    definition

      mode GraphSeq is Graph-yielding ManySortedSet of NAT ;

    end

    registration

      cluster -> non empty for GraphSeq;

      coherence

      proof

        let GSeq be GraphSeq;

        ( dom GSeq) = NAT by PARTFUN1:def 2;

        hence thesis;

      end;

    end

    registration

      cluster non empty Graph-yielding for Function;

      existence

      proof

        take the GraphSeq;

        thus thesis;

      end;

    end

    registration

      let GF be non empty Graph-yielding Function, x be Element of ( dom GF);

      cluster (GF . x) -> Function-like Relation-like;

      coherence by Def53a;

    end

    registration

      let GSq be GraphSeq, x be Nat;

      cluster (GSq . x) -> Function-like Relation-like;

      coherence by Def53;

    end

    registration

      let GF be non empty Graph-yielding Function, x be Element of ( dom GF);

      cluster (GF . x) -> NAT -defined finite;

      coherence by Def53a;

    end

    registration

      let GSq be GraphSeq, x be Nat;

      cluster (GSq . x) -> NAT -defined finite;

      coherence by Def53;

    end

    registration

      let GF be non empty Graph-yielding Function, x be Element of ( dom GF);

      cluster (GF . x) -> [Graph-like];

      coherence by Def53a;

    end

    registration

      let GSq be GraphSeq, x be Nat;

      cluster (GSq . x) -> [Graph-like];

      coherence by Def53;

    end

    definition

      let GF be Graph-yielding Function;

      :: GLIB_000:def58

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

      :: GLIB_000:def59

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

      :: GLIB_000:def60

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

      :: GLIB_000:def61

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

      :: GLIB_000:def62

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

      :: GLIB_000:def63

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

      :: GLIB_000:def64

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

      :: GLIB_000:def65

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

    end

    registration

      cluster empty -> _finite loopless _trivial non-trivial non-multi non-Dmulti simple Dsimple for Graph-yielding Function;

      coherence ;

    end

    definition

      let GF be non empty Graph-yielding Function;

      :: original: _finite

      redefine

      :: GLIB_000:def66

      attr GF is _finite means

      : Def57b: for x be Element of ( dom GF) holds (GF . x) is _finite;

      compatibility

      proof

        hereby

          assume

           A1: GF is _finite;

          let x be Element of ( dom GF);

          consider G be _Graph such that

           A2: (GF . x) = G & G is _finite by A1;

          thus (GF . x) is _finite by A2;

        end;

        assume

         A3: for x be Element of ( dom GF) holds (GF . x) is _finite;

        let x be object;

        assume x in ( dom GF);

        then

        reconsider y = x as Element of ( dom GF);

        take (GF . y);

        thus thesis by A3;

      end;

      :: original: loopless

      redefine

      :: GLIB_000:def67

      attr GF is loopless means

      : Def58b: for x be Element of ( dom GF) holds (GF . x) is loopless;

      compatibility

      proof

        hereby

          assume

           A1: GF is loopless;

          let x be Element of ( dom GF);

          consider G be _Graph such that

           A2: (GF . x) = G & G is loopless by A1;

          thus (GF . x) is loopless by A2;

        end;

        assume

         A3: for x be Element of ( dom GF) holds (GF . x) is loopless;

        let x be object;

        assume x in ( dom GF);

        then

        reconsider y = x as Element of ( dom GF);

        take (GF . y);

        thus thesis by A3;

      end;

      :: original: _trivial

      redefine

      :: GLIB_000:def68

      attr GF is _trivial means

      : Def59b: for x be Element of ( dom GF) holds (GF . x) is _trivial;

      compatibility

      proof

        hereby

          assume

           A1: GF is _trivial;

          let x be Element of ( dom GF);

          consider G be _Graph such that

           A2: (GF . x) = G & G is _trivial by A1;

          thus (GF . x) is _trivial by A2;

        end;

        assume

         A3: for x be Element of ( dom GF) holds (GF . x) is _trivial;

        let x be object;

        assume x in ( dom GF);

        then

        reconsider y = x as Element of ( dom GF);

        take (GF . y);

        thus thesis by A3;

      end;

      :: original: non-trivial

      redefine

      :: GLIB_000:def69

      attr GF is non-trivial means

      : Def60b: for x be Element of ( dom GF) holds (GF . x) is non _trivial;

      compatibility

      proof

        hereby

          assume

           A1: GF is non-trivial;

          let x be Element of ( dom GF);

          consider G be _Graph such that

           A2: (GF . x) = G & G is non _trivial by A1;

          thus (GF . x) is non _trivial by A2;

        end;

        assume

         A3: for x be Element of ( dom GF) holds (GF . x) is non _trivial;

        let x be object;

        assume x in ( dom GF);

        then

        reconsider y = x as Element of ( dom GF);

        take (GF . y);

        thus thesis by A3;

      end;

      :: original: non-multi

      redefine

      :: GLIB_000:def70

      attr GF is non-multi means

      : Def61b: for x be Element of ( dom GF) holds (GF . x) is non-multi;

      compatibility

      proof

        hereby

          assume

           A1: GF is non-multi;

          let x be Element of ( dom GF);

          consider G be _Graph such that

           A2: (GF . x) = G & G is non-multi by A1;

          thus (GF . x) is non-multi by A2;

        end;

        assume

         A3: for x be Element of ( dom GF) holds (GF . x) is non-multi;

        let x be object;

        assume x in ( dom GF);

        then

        reconsider y = x as Element of ( dom GF);

        take (GF . y);

        thus thesis by A3;

      end;

      :: original: non-Dmulti

      redefine

      :: GLIB_000:def71

      attr GF is non-Dmulti means

      : Def62b: for x be Element of ( dom GF) holds (GF . x) is non-Dmulti;

      compatibility

      proof

        hereby

          assume

           A1: GF is non-Dmulti;

          let x be Element of ( dom GF);

          consider G be _Graph such that

           A2: (GF . x) = G & G is non-Dmulti by A1;

          thus (GF . x) is non-Dmulti by A2;

        end;

        assume

         A3: for x be Element of ( dom GF) holds (GF . x) is non-Dmulti;

        let x be object;

        assume x in ( dom GF);

        then

        reconsider y = x as Element of ( dom GF);

        take (GF . y);

        thus thesis by A3;

      end;

      :: original: simple

      redefine

      :: GLIB_000:def72

      attr GF is simple means

      : Def63b: for x be Element of ( dom GF) holds (GF . x) is simple;

      compatibility

      proof

        hereby

          assume

           A1: GF is simple;

          let x be Element of ( dom GF);

          consider G be _Graph such that

           A2: (GF . x) = G & G is simple by A1;

          thus (GF . x) is simple by A2;

        end;

        assume

         A3: for x be Element of ( dom GF) holds (GF . x) is simple;

        let x be object;

        assume x in ( dom GF);

        then

        reconsider y = x as Element of ( dom GF);

        take (GF . y);

        thus thesis by A3;

      end;

      :: original: Dsimple

      redefine

      :: GLIB_000:def73

      attr GF is Dsimple means

      : Def64b: for x be Element of ( dom GF) holds (GF . x) is Dsimple;

      compatibility

      proof

        hereby

          assume

           A1: GF is Dsimple;

          let x be Element of ( dom GF);

          consider G be _Graph such that

           A2: (GF . x) = G & G is Dsimple by A1;

          thus (GF . x) is Dsimple by A2;

        end;

        assume

         A3: for x be Element of ( dom GF) holds (GF . x) is Dsimple;

        let x be object;

        assume x in ( dom GF);

        then

        reconsider y = x as Element of ( dom GF);

        take (GF . y);

        thus thesis by A3;

      end;

    end

    definition

      let GSq be GraphSeq;

      :: original: _finite

      redefine

      :: GLIB_000:def74

      attr GSq is _finite means

      : Def57: for x be Nat holds (GSq . x) is _finite;

      compatibility

      proof

        hereby

          assume

           A1: GSq is _finite;

          let x be Nat;

          x in ( dom GSq) by LmNat;

          hence (GSq . x) is _finite by A1;

        end;

        assume

         A2: for x be Nat holds (GSq . x) is _finite;

        let x be Element of ( dom GSq);

        thus thesis by A2;

      end;

      :: original: loopless

      redefine

      :: GLIB_000:def75

      attr GSq is loopless means

      : Def58: for x be Nat holds (GSq . x) is loopless;

      compatibility

      proof

        hereby

          assume

           A1: GSq is loopless;

          let x be Nat;

          x in ( dom GSq) by LmNat;

          hence (GSq . x) is loopless by A1;

        end;

        assume

         A2: for x be Nat holds (GSq . x) is loopless;

        let x be Element of ( dom GSq);

        thus thesis by A2;

      end;

      :: original: _trivial

      redefine

      :: GLIB_000:def76

      attr GSq is _trivial means

      : Def59: for x be Nat holds (GSq . x) is _trivial;

      compatibility

      proof

        hereby

          assume

           A1: GSq is _trivial;

          let x be Nat;

          x in ( dom GSq) by LmNat;

          hence (GSq . x) is _trivial by A1;

        end;

        assume

         A2: for x be Nat holds (GSq . x) is _trivial;

        let x be Element of ( dom GSq);

        thus thesis by A2;

      end;

      :: original: non-trivial

      redefine

      :: GLIB_000:def77

      attr GSq is non-trivial means

      : Def60: for x be Nat holds (GSq . x) is non _trivial;

      compatibility

      proof

        hereby

          assume

           A1: GSq is non-trivial;

          let x be Nat;

          x in ( dom GSq) by LmNat;

          hence (GSq . x) is non _trivial by A1;

        end;

        assume

         A2: for x be Nat holds (GSq . x) is non _trivial;

        let x be Element of ( dom GSq);

        thus thesis by A2;

      end;

      :: original: non-multi

      redefine

      :: GLIB_000:def78

      attr GSq is non-multi means

      : Def61: for x be Nat holds (GSq . x) is non-multi;

      compatibility

      proof

        hereby

          assume

           A1: GSq is non-multi;

          let x be Nat;

          x in ( dom GSq) by LmNat;

          hence (GSq . x) is non-multi by A1;

        end;

        assume

         A2: for x be Nat holds (GSq . x) is non-multi;

        let x be Element of ( dom GSq);

        thus thesis by A2;

      end;

      :: original: non-Dmulti

      redefine

      :: GLIB_000:def79

      attr GSq is non-Dmulti means

      : Def62: for x be Nat holds (GSq . x) is non-Dmulti;

      compatibility

      proof

        hereby

          assume

           A1: GSq is non-Dmulti;

          let x be Nat;

          x in ( dom GSq) by LmNat;

          hence (GSq . x) is non-Dmulti by A1;

        end;

        assume

         A2: for x be Nat holds (GSq . x) is non-Dmulti;

        let x be Element of ( dom GSq);

        thus thesis by A2;

      end;

      :: original: simple

      redefine

      :: GLIB_000:def80

      attr GSq is simple means

      : Def63: for x be Nat holds (GSq . x) is simple;

      compatibility

      proof

        hereby

          assume

           A1: GSq is simple;

          let x be Nat;

          x in ( dom GSq) by LmNat;

          hence (GSq . x) is simple by A1;

        end;

        assume

         A2: for x be Nat holds (GSq . x) is simple;

        let x be Element of ( dom GSq);

        thus thesis by A2;

      end;

      :: original: Dsimple

      redefine

      :: GLIB_000:def81

      attr GSq is Dsimple means

      : Def64: for x be Nat holds (GSq . x) is Dsimple;

      compatibility

      proof

        hereby

          assume

           A1: GSq is Dsimple;

          let x be Nat;

          x in ( dom GSq) by LmNat;

          hence (GSq . x) is Dsimple by A1;

        end;

        assume

         A2: for x be Nat holds (GSq . x) is Dsimple;

        let x be Element of ( dom GSq);

        thus thesis by A2;

      end;

    end

    definition

      let GSq be GraphSeq;

      :: original: halting

      redefine

      :: GLIB_000:def82

      attr GSq is halting means ex n be Nat st (GSq . n) = (GSq . (n + 1));

      compatibility ;

    end

    registration

      cluster halting _finite loopless _trivial non-multi non-Dmulti simple Dsimple for GraphSeq;

      existence

      proof

        set G = the _finite loopless _trivial non-multi non-Dmulti simple Dsimple _Graph;

        set F = ( NAT --> G);

        reconsider F as ManySortedSet of NAT ;

        reconsider F as GraphSeq;

        

         A2: (F . (1 + 1)) = G;

        take F;

        (F . 1) = G;

        hence F is halting by A2;

        thus thesis;

      end;

      cluster halting _finite loopless non-trivial non-multi non-Dmulti simple Dsimple for GraphSeq;

      existence

      proof

        set G = the _finite loopless non _trivial non-multi non-Dmulti simple Dsimple _Graph;

        set F = ( NAT --> G);

        reconsider F as ManySortedSet of NAT ;

        reconsider F as GraphSeq;

        

         A4: (F . (1 + 1)) = G;

        take F;

        (F . 1) = G;

        hence F is halting by A4;

        thus thesis;

      end;

    end

    registration

      let GF be _finite non empty Graph-yielding Function, x be Element of ( dom GF);

      cluster (GF . x) -> _finite;

      coherence by Def57b;

    end

    registration

      let GSq be _finite GraphSeq, x be Nat;

      cluster (GSq . x) -> _finite;

      coherence by Def57;

    end

    registration

      let GF be loopless non empty Graph-yielding Function, x be Element of ( dom GF);

      cluster (GF . x) -> loopless;

      coherence by Def58b;

    end

    registration

      let GSq be loopless GraphSeq, x be Nat;

      cluster (GSq . x) -> loopless;

      coherence by Def58;

    end

    registration

      let GF be _trivial non empty Graph-yielding Function, x be Element of ( dom GF);

      cluster (GF . x) -> _trivial;

      coherence by Def59b;

    end

    registration

      let GSq be _trivial GraphSeq, x be Nat;

      cluster (GSq . x) -> _trivial;

      coherence by Def59;

    end

    registration

      let GF be non-trivial non empty Graph-yielding Function;

      let x be Element of ( dom GF);

      cluster (GF . x) -> non _trivial;

      coherence by Def60b;

    end

    registration

      let GSq be non-trivial GraphSeq, x be Nat;

      cluster (GSq . x) -> non _trivial;

      coherence by Def60;

    end

    registration

      let GF be non-multi non empty Graph-yielding Function;

      let x be Element of ( dom GF);

      cluster (GF . x) -> non-multi;

      coherence by Def61b;

    end

    registration

      let GSq be non-multi GraphSeq, x be Nat;

      cluster (GSq . x) -> non-multi;

      coherence by Def61;

    end

    registration

      let GF be non-Dmulti non empty Graph-yielding Function;

      let x be Element of ( dom GF);

      cluster (GF . x) -> non-Dmulti;

      coherence by Def62b;

    end

    registration

      let GSq be non-Dmulti GraphSeq, x be Nat;

      cluster (GSq . x) -> non-Dmulti;

      coherence by Def62;

    end

    registration

      let GF be simple non empty Graph-yielding Function, x be Element of ( dom GF);

      cluster (GF . x) -> simple;

      coherence by Def63b;

    end

    registration

      let GSq be simple GraphSeq, x be Nat;

      cluster (GSq . x) -> simple;

      coherence by Def63;

    end

    registration

      let GF be Dsimple non empty Graph-yielding Function, x be Element of ( dom GF);

      cluster (GF . x) -> Dsimple;

      coherence by Def64b;

    end

    registration

      let GSq be Dsimple GraphSeq, x be Nat;

      cluster (GSq . x) -> Dsimple;

      coherence by Def64;

    end

    registration

      cluster non-multi -> non-Dmulti for Graph-yielding Function;

      coherence

      proof

        let GF be Graph-yielding Function;

        per cases ;

          suppose GF is empty;

          hence thesis;

        end;

          suppose GF is non empty;

          hence thesis;

        end;

      end;

    end

    registration

      cluster simple -> loopless non-multi for Graph-yielding Function;

      coherence

      proof

        let GF be Graph-yielding Function;

        per cases ;

          suppose GF is empty;

          hence thesis;

        end;

          suppose GF is non empty;

          hence thesis;

        end;

      end;

    end

    registration

      cluster loopless non-multi -> simple for Graph-yielding Function;

      coherence

      proof

        let GF be Graph-yielding Function;

        per cases ;

          suppose GF is empty;

          hence thesis;

        end;

          suppose GF is non empty;

          hence thesis;

        end;

      end;

    end

    registration

      cluster loopless non-Dmulti -> Dsimple for Graph-yielding Function;

      coherence

      proof

        let GF be Graph-yielding Function;

        per cases ;

          suppose GF is empty;

          hence thesis;

        end;

          suppose GF is non empty;

          hence thesis;

        end;

      end;

    end

    registration

      cluster Dsimple -> loopless non-Dmulti for Graph-yielding Function;

      coherence

      proof

        let GF be Graph-yielding Function;

        per cases ;

          suppose GF is empty;

          hence thesis;

        end;

          suppose GF is non empty;

          hence thesis;

        end;

      end;

    end

    registration

      cluster _trivial loopless -> _finite for Graph-yielding Function;

      coherence

      proof

        let GF be Graph-yielding Function;

        per cases ;

          suppose GF is empty;

          hence thesis;

        end;

          suppose GF is non empty;

          hence thesis;

        end;

      end;

    end

    registration

      cluster _trivial non-Dmulti -> _finite for Graph-yielding Function;

      coherence

      proof

        let GF be Graph-yielding Function;

        per cases ;

          suppose GF is empty;

          hence thesis;

        end;

          suppose GF is non empty;

          hence thesis;

        end;

      end;

    end

    begin

    reserve GS for GraphStruct;

    reserve G,G1,G2,G3 for _Graph;

    reserve e,x,x1,x2,y,y1,y2,E,V,X,Y for set;

    reserve n,n1,n2 for Nat;

    reserve v,v1,v2 for Vertex of G;

    theorem :: GLIB_000:1

     VertexSelector = 1 & EdgeSelector = 2 & SourceSelector = 3 & TargetSelector = 4;

    theorem :: GLIB_000:2

     _GraphSelectors c= ( dom G)

    proof

      let x be object;

      assume x in _GraphSelectors ;

      then x = VertexSelector or x = EdgeSelector or x = SourceSelector or x = TargetSelector by ENUMSET1:def 2;

      hence x in ( dom G) by Def10;

    end;

    theorem :: GLIB_000:3

    ( the_Vertices_of GS) = (GS . VertexSelector ) & ( the_Edges_of GS) = (GS . EdgeSelector ) & ( the_Source_of GS) = (GS . SourceSelector ) & ( the_Target_of GS) = (GS . TargetSelector );

    theorem :: GLIB_000:4

    ( dom ( the_Source_of G)) = ( the_Edges_of G) & ( dom ( the_Target_of G)) = ( the_Edges_of G) & ( rng ( the_Source_of G)) c= ( the_Vertices_of G) & ( rng ( the_Target_of G)) c= ( the_Vertices_of G) by FUNCT_2:def 1;

    theorem :: GLIB_000:5

    GS is [Graph-like] iff _GraphSelectors c= ( dom GS) & ( the_Vertices_of GS) is non empty & ( the_Source_of GS) is Function of ( the_Edges_of GS), ( the_Vertices_of GS) & ( the_Target_of GS) is Function of ( the_Edges_of GS), ( the_Vertices_of GS) by Lm1;

    theorem :: GLIB_000:6

    for V be non empty set, E be set, S,T be Function of E, V holds ( the_Vertices_of ( createGraph (V,E,S,T))) = V & ( the_Edges_of ( createGraph (V,E,S,T))) = E & ( the_Source_of ( createGraph (V,E,S,T))) = S & ( the_Target_of ( createGraph (V,E,S,T))) = T by FINSEQ_4: 76;

    theorem :: GLIB_000:7

    

     Th7: ( dom (GS .set (n,x))) = (( dom GS) \/ {n})

    proof

      set G2 = (GS .set (n,x));

      

      thus ( dom G2) = (( dom GS) \/ ( dom (n .--> x))) by FUNCT_4:def 1

      .= (( dom GS) \/ {n});

    end;

    theorem :: GLIB_000:8

    

     Th8: ((GS .set (n,x)) . n) = x

    proof

      set G2 = (GS .set (n,x));

      n in ( dom (n .--> x)) by TARSKI:def 1;

      

      hence (G2 . n) = ((n .--> x) . n) by FUNCT_4: 13

      .= x by FUNCOP_1: 72;

    end;

    theorem :: GLIB_000:9

    

     Th9: n1 <> n2 implies (GS . n2) = ((GS .set (n1,x)) . n2)

    proof

      assume n1 <> n2;

      then not n2 in ( dom (n1 .--> x)) by TARSKI:def 1;

      hence thesis by FUNCT_4: 11;

    end;

    theorem :: GLIB_000:10

     not n in _GraphSelectors implies ( the_Vertices_of G) = ( the_Vertices_of (G .set (n,x))) & ( the_Edges_of G) = ( the_Edges_of (G .set (n,x))) & ( the_Source_of G) = ( the_Source_of (G .set (n,x))) & ( the_Target_of G) = ( the_Target_of (G .set (n,x))) & (G .set (n,x)) is _Graph

    proof

      set G2 = (G .set (n,x));

      

       A1: ( dom G) c= ( dom G2) by FUNCT_4: 10;

      assume

       A2: not n in _GraphSelectors ;

      then EdgeSelector <> n by ENUMSET1:def 2;

      then

       A3: not EdgeSelector in ( dom (n .--> x)) by TARSKI:def 1;

       TargetSelector <> n by A2, ENUMSET1:def 2;

      then

       A4: not TargetSelector in ( dom (n .--> x)) by TARSKI:def 1;

       SourceSelector <> n by A2, ENUMSET1:def 2;

      then

       A5: not SourceSelector in ( dom (n .--> x)) by TARSKI:def 1;

       VertexSelector <> n by A2, ENUMSET1:def 2;

      then not VertexSelector in ( dom (n .--> x)) by TARSKI:def 1;

      hence

       A6: ( the_Vertices_of G2) = ( the_Vertices_of G) & ( the_Edges_of G2) = ( the_Edges_of G) & ( the_Source_of G2) = ( the_Source_of G) & ( the_Target_of G2) = ( the_Target_of G) by A3, A5, A4, FUNCT_4: 11;

      

       A7: SourceSelector in ( dom G) & TargetSelector in ( dom G) by Def10;

       VertexSelector in ( dom G) & EdgeSelector in ( dom G) by Def10;

      hence thesis by A7, A1, A6, Def10;

    end;

    theorem :: GLIB_000:11

    ( the_Vertices_of (GS .set ( VertexSelector ,x))) = x & ( the_Edges_of (GS .set ( EdgeSelector ,x))) = x & ( the_Source_of (GS .set ( SourceSelector ,x))) = x & ( the_Target_of (GS .set ( TargetSelector ,x))) = x by Th8;

    theorem :: GLIB_000:12

    n1 <> n2 implies n1 in ( dom ((GS .set (n1,x)) .set (n2,y))) & n2 in ( dom ((GS .set (n1,x)) .set (n2,y))) & (((GS .set (n1,x)) .set (n2,y)) . n1) = x & (((GS .set (n1,x)) .set (n2,y)) . n2) = y

    proof

      assume

       A1: n1 <> n2;

      set G2 = (GS .set (n1,x)), G3 = (G2 .set (n2,y));

      

       A2: ( dom G3) = (( dom G2) \/ {n2}) by Th7;

      ( dom G2) = (( dom GS) \/ {n1}) & n1 in {n1} by Th7, TARSKI:def 1;

      then n1 in ( dom G2) by XBOOLE_0:def 3;

      hence n1 in ( dom ((GS .set (n1,x)) .set (n2,y))) by A2, XBOOLE_0:def 3;

      n2 in {n2} by TARSKI:def 1;

      hence n2 in ( dom ((GS .set (n1,x)) .set (n2,y))) by A2, XBOOLE_0:def 3;

      

      thus (((GS .set (n1,x)) .set (n2,y)) . n1) = (G2 . n1) by A1, Th9

      .= x by Th8;

      thus thesis by Th8;

    end;

    theorem :: GLIB_000:13

    for e,x,y be object holds e Joins (x,y,G) implies x in ( the_Vertices_of G) & y in ( the_Vertices_of G) by FUNCT_2: 5;

    theorem :: GLIB_000:14

    for e,x,y be object holds e Joins (x,y,G) implies e Joins (y,x,G);

    theorem :: GLIB_000:15

    for e,x1,x2,y1,y2 be object holds e Joins (x1,y1,G) & e Joins (x2,y2,G) implies x1 = x2 & y1 = y2 or x1 = y2 & y1 = x2;

    theorem :: GLIB_000:16

    for e,x,y be object holds e Joins (x,y,G) iff (e DJoins (x,y,G) or e DJoins (y,x,G));

    theorem :: GLIB_000:17

    for e,x,y be object st e Joins (x,y,G) & (x in X & y in Y or x in Y & y in X) holds e SJoins (X,Y,G);

    theorem :: GLIB_000:18

    G is loopless iff for v be object holds not ex e be object st e Joins (v,v,G)

    proof

      thus G is loopless implies for v be object holds not ex e be object st e Joins (v,v,G);

      assume

       A1: for v be object holds not ex e be object st e Joins (v,v,G);

      now

        given e be object such that

         A2: e in ( the_Edges_of G) & (( the_Source_of G) . e) = (( the_Target_of G) . e);

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

        e Joins (v,v,G) by A2;

        hence contradiction by A1;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:19

    for G be loopless _Graph, v be Vertex of G holds (v .degree() ) = ( card (v .edgesInOut() ))

    proof

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

      set In = (v .edgesIn() ), Out = (v .edgesOut() );

      now

        given e be object such that

         A1: e in (In /\ Out);

        e in Out by A1, XBOOLE_0:def 4;

        then

         A2: (( the_Source_of G) . e) = v by Lm8;

        e in In by A1, XBOOLE_0:def 4;

        then (( the_Target_of G) . e) = v by Lm7;

        hence contradiction by A1, A2, Def18;

      end;

      then (In /\ Out) = {} by XBOOLE_0:def 1;

      then In misses Out by XBOOLE_0:def 7;

      hence thesis by CARD_2: 35;

    end;

    theorem :: GLIB_000:20

    for G be non _trivial _Graph, v be Vertex of G holds (( the_Vertices_of G) \ {v}) is non empty

    proof

      let G be non _trivial _Graph, v be Vertex of G;

      set VG = ( the_Vertices_of G);

      now

        assume (VG \ {v}) = {} ;

        then VG c= {v} by XBOOLE_1: 37;

        then VG = {v} by ZFMISC_1: 33;

        then ( card VG) = 1 by CARD_1: 30;

        hence contradiction by Def19;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:21

    for G be non _trivial _Graph holds ex v1,v2 be Vertex of G st v1 <> v2

    proof

      let G be non _trivial _Graph;

      set VG = ( the_Vertices_of G);

      take v1 = the Element of VG;

      set VG2 = (VG \ {v1});

      now

        assume

         A1: VG2 = {} ;

        ( card (VG2 \/ {v1})) = (( card VG2) +` ( card {v1})) by CARD_2: 35, XBOOLE_1: 79

        .= ( 0 +` 1) by A1, CARD_1: 30

        .= ( card ( 0 +^ 1)) by CARD_2:def 1

        .= ( card ( 0 + 1)) by CARD_2: 36

        .= 1;

        then ( card VG) = 1 by XBOOLE_1: 45;

        hence contradiction by Def19;

      end;

      then

      reconsider VG2 as non empty set;

      set v2 = the Element of VG2;

      

       A2: not v2 in {v1} by XBOOLE_0:def 5;

      reconsider v2 as Vertex of G by XBOOLE_0:def 5;

      take v2;

      thus thesis by A2, TARSKI:def 1;

    end;

    theorem :: GLIB_000:22

    

     Th22: for G be _trivial _Graph holds ex v be Vertex of G st ( the_Vertices_of G) = {v}

    proof

      let G be _trivial _Graph;

      ( card ( the_Vertices_of G)) = 1 by Def19;

      then

      consider v be object such that

       A1: ( the_Vertices_of G) = {v} by CARD_2: 42;

      reconsider v as Vertex of G by A1, TARSKI:def 1;

      take v;

      thus thesis by A1;

    end;

    theorem :: GLIB_000:23

    for G be _trivial loopless _Graph holds ( the_Edges_of G) = {}

    proof

      let G be _trivial loopless _Graph;

      consider v be Vertex of G such that

       A1: ( the_Vertices_of G) = {v} by Th22;

      now

        assume ( the_Edges_of G) <> {} ;

        then

        consider e be object such that

         A2: e in ( the_Edges_of G) by XBOOLE_0:def 1;

        (( the_Target_of G) . e) in {v} by A1, A2, FUNCT_2: 5;

        then

         A3: (( the_Target_of G) . e) = v by TARSKI:def 1;

        (( the_Source_of G) . e) in {v} by A1, A2, FUNCT_2: 5;

        then (( the_Source_of G) . e) = v by TARSKI:def 1;

        hence contradiction by A2, A3, Def18;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:24

    ( the_Edges_of G) = {} implies G is simple

    proof

      assume

       A1: ( the_Edges_of G) = {} ;

      then

       A2: G is loopless;

      for e1,e2,v1,v2 be object holds e1 Joins (v1,v2,G) & e2 Joins (v1,v2,G) implies e1 = e2 by A1;

      then G is non-multi;

      hence thesis by A2;

    end;

    theorem :: GLIB_000:25

    for G be _finite _Graph holds (G .order() ) >= 1

    proof

      let G be _finite _Graph;

      ( 0 + 1) < ((G .order() ) + 1) by NAT_1: 3, XREAL_1: 8;

      hence thesis by NAT_1: 13;

    end;

    theorem :: GLIB_000:26

    for G be _Graph holds (G .order() ) = 1 iff G is _trivial;

    theorem :: GLIB_000:27

    for G be _Graph holds (G .order() ) = 1 iff ex v be Vertex of G st ( the_Vertices_of G) = {v}

    proof

      let G be _Graph;

      hereby

        assume (G .order() ) = 1;

        then

        consider v be object such that

         A1: ( the_Vertices_of G) = {v} by CARD_2: 42;

        reconsider v as Vertex of G by A1, TARSKI:def 1;

        take v;

        thus ( the_Vertices_of G) = {v} by A1;

      end;

      given v be Vertex of G such that

       A2: ( the_Vertices_of G) = {v};

      thus thesis by A2, CARD_1: 30;

    end;

    theorem :: GLIB_000:28

    

     Th28: e in ( the_Edges_of G) & ((( the_Source_of G) . e) in X or (( the_Target_of G) . e) in X) iff e in (G .edgesInOut X)

    proof

      hereby

        assume that

         A1: e in ( the_Edges_of G) and

         A2: (( the_Source_of G) . e) in X or (( the_Target_of G) . e) in X;

        now

          per cases by A2;

            suppose (( the_Source_of G) . e) in X;

            then e in (G .edgesOutOf X) by A1, Def27;

            hence e in (G .edgesInOut X) by XBOOLE_0:def 3;

          end;

            suppose (( the_Target_of G) . e) in X;

            then e in (G .edgesInto X) by A1, Def26;

            hence e in (G .edgesInOut X) by XBOOLE_0:def 3;

          end;

        end;

        hence e in (G .edgesInOut X);

      end;

      assume e in (G .edgesInOut X);

      then e in (G .edgesInto X) or e in (G .edgesOutOf X) by XBOOLE_0:def 3;

      hence thesis by Def26, Def27;

    end;

    theorem :: GLIB_000:29

    (G .edgesInto X) c= (G .edgesInOut X) & (G .edgesOutOf X) c= (G .edgesInOut X) by XBOOLE_0:def 3;

    theorem :: GLIB_000:30

    ( the_Edges_of G) = (G .edgesInOut ( the_Vertices_of G))

    proof

      set EG = ( the_Edges_of G), SG = ( the_Source_of G);

      now

        let x be object;

        hereby

          assume

           A1: x in EG;

          then (SG . x) in ( the_Vertices_of G) by FUNCT_2: 5;

          hence x in (G .edgesInOut ( the_Vertices_of G)) by A1, Th28;

        end;

        assume x in (G .edgesInOut ( the_Vertices_of G));

        hence x in EG;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLIB_000:31

    e in ( the_Edges_of G) & (( the_Source_of G) . e) in X & (( the_Target_of G) . e) in X iff e in (G .edgesBetween X) by Lm5;

    theorem :: GLIB_000:32

    for e,x,y be object holds x in X & y in X & e Joins (x,y,G) implies e in (G .edgesBetween X) by Lm5;

    theorem :: GLIB_000:33

    (G .edgesBetween X) c= (G .edgesInOut X)

    proof

      let z be object;

      assume z in (G .edgesBetween X);

      then z in (G .edgesInto X) by XBOOLE_0:def 4;

      hence z in (G .edgesInOut X) by XBOOLE_0:def 3;

    end;

    theorem :: GLIB_000:34

    

     Th34: ( the_Edges_of G) = (G .edgesBetween ( the_Vertices_of G))

    proof

      set EG = ( the_Edges_of G), SG = ( the_Source_of G), TG = ( the_Target_of G);

      now

        let x be object;

        hereby

          assume

           A1: x in EG;

          then (SG . x) in ( the_Vertices_of G) & (TG . x) in ( the_Vertices_of G) by FUNCT_2: 5;

          hence x in (G .edgesBetween ( the_Vertices_of G)) by A1, Lm5;

        end;

        assume x in (G .edgesBetween ( the_Vertices_of G));

        hence x in EG;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLIB_000:35

    

     Th35: (( the_Edges_of G) \ (G .edgesInOut X)) = (G .edgesBetween (( the_Vertices_of G) \ X))

    proof

      set EG = ( the_Edges_of G), VG = ( the_Vertices_of G);

      set EIO = (G .edgesInOut X), EB = (G .edgesBetween (VG \ X));

      now

        let x be object;

        hereby

          assume

           A1: x in (EG \ EIO);

          then

           A2: (( the_Target_of G) . x) in VG by FUNCT_2: 5;

          

           A3: not x in EIO by A1, XBOOLE_0:def 5;

          then not (( the_Target_of G) . x) in X by A1, Th28;

          then

           A4: (( the_Target_of G) . x) in (VG \ X) by A2, XBOOLE_0:def 5;

          

           A5: (( the_Source_of G) . x) in VG by A1, FUNCT_2: 5;

           not (( the_Source_of G) . x) in X by A1, A3, Th28;

          then (( the_Source_of G) . x) in (VG \ X) by A5, XBOOLE_0:def 5;

          hence x in EB by A1, A4, Lm5;

        end;

        assume

         A6: x in EB;

        then (( the_Target_of G) . x) in (VG \ X) by Lm5;

        then

         A7: not (( the_Target_of G) . x) in X by XBOOLE_0:def 5;

        (( the_Source_of G) . x) in (VG \ X) by A6, Lm5;

        then not (( the_Source_of G) . x) in X by XBOOLE_0:def 5;

        then not x in EIO by A7, Th28;

        hence x in (EG \ EIO) by A6, XBOOLE_0:def 5;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLIB_000:36

    X c= Y implies (G .edgesBetween X) c= (G .edgesBetween Y)

    proof

      assume

       A1: X c= Y;

      let x be object;

      assume

       A2: x in (G .edgesBetween X);

      then (( the_Source_of G) . x) in X & (( the_Target_of G) . x) in X by Lm5;

      hence x in (G .edgesBetween Y) by A1, A2, Lm5;

    end;

    theorem :: GLIB_000:37

    for G be _Graph, X1,X2,Y1,Y2 be set st X1 c= X2 & Y1 c= Y2 holds (G .edgesBetween (X1,Y1)) c= (G .edgesBetween (X2,Y2))

    proof

      let G be _Graph, X1,X2,Y1,Y2 be set;

      assume

       A1: X1 c= X2 & Y1 c= Y2;

      let e be object;

      assume e in (G .edgesBetween (X1,Y1));

      then e SJoins (X1,Y1,G) by Def30;

      then e SJoins (X2,Y2,G) by A1;

      hence e in (G .edgesBetween (X2,Y2)) by Def30;

    end;

    theorem :: GLIB_000:38

    for G be _Graph, X1,X2,Y1,Y2 be set st X1 c= X2 & Y1 c= Y2 holds (G .edgesDBetween (X1,Y1)) c= (G .edgesDBetween (X2,Y2))

    proof

      let G be _Graph, X1,X2,Y1,Y2 be set;

      assume

       A1: X1 c= X2 & Y1 c= Y2;

      let e be object;

      assume e in (G .edgesDBetween (X1,Y1));

      then e DSJoins (X1,Y1,G) by Def31;

      then e DSJoins (X2,Y2,G) by A1;

      hence e in (G .edgesDBetween (X2,Y2)) by Def31;

    end;

    theorem :: GLIB_000:39

    for G be _Graph, v be Vertex of G holds (v .edgesIn() ) = (G .edgesDBetween (( the_Vertices_of G), {v})) & (v .edgesOut() ) = (G .edgesDBetween ( {v},( the_Vertices_of G)))

    proof

      let G be _Graph, v be Vertex of G;

      now

        let e be object;

        hereby

          assume

           A1: e in (v .edgesIn() );

          then (( the_Target_of G) . e) = v by Lm7;

          then

           A2: (( the_Target_of G) . e) in {v} by TARSKI:def 1;

          (( the_Source_of G) . e) in ( the_Vertices_of G) by A1, FUNCT_2: 5;

          then e DSJoins (( the_Vertices_of G), {v},G) by A1, A2;

          hence e in (G .edgesDBetween (( the_Vertices_of G), {v})) by Def31;

        end;

        assume

         A3: e in (G .edgesDBetween (( the_Vertices_of G), {v}));

        then e DSJoins (( the_Vertices_of G), {v},G) by Def31;

        then (( the_Target_of G) . e) = v by TARSKI:def 1;

        hence e in (v .edgesIn() ) by A3, Lm7;

      end;

      hence (v .edgesIn() ) = (G .edgesDBetween (( the_Vertices_of G), {v})) by TARSKI: 2;

      now

        let e be object;

        hereby

          assume

           A4: e in (v .edgesOut() );

          then (( the_Source_of G) . e) = v by Lm8;

          then

           A5: (( the_Source_of G) . e) in {v} by TARSKI:def 1;

          (( the_Target_of G) . e) in ( the_Vertices_of G) by A4, FUNCT_2: 5;

          then e DSJoins ( {v},( the_Vertices_of G),G) by A4, A5;

          hence e in (G .edgesDBetween ( {v},( the_Vertices_of G))) by Def31;

        end;

        assume

         A6: e in (G .edgesDBetween ( {v},( the_Vertices_of G)));

        then e DSJoins ( {v},( the_Vertices_of G),G) by Def31;

        then (( the_Source_of G) . e) = v by TARSKI:def 1;

        hence e in (v .edgesOut() ) by A6, Lm8;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLIB_000:40

    G is Subgraph of G by Lm3;

    theorem :: GLIB_000:41

    

     Th41: G1 is Subgraph of G2 & G2 is Subgraph of G1 iff ( the_Vertices_of G1) = ( the_Vertices_of G2) & ( the_Edges_of G1) = ( the_Edges_of G2) & ( the_Source_of G1) = ( the_Source_of G2) & ( the_Target_of G1) = ( the_Target_of G2)

    proof

      hereby

        assume that

         A1: G1 is Subgraph of G2 and

         A2: G2 is Subgraph of G1;

        

         A3: ( the_Vertices_of G2) c= ( the_Vertices_of G1) & ( the_Edges_of G2) c= ( the_Edges_of G1) by A2, Def32;

        ( the_Vertices_of G1) c= ( the_Vertices_of G2) & ( the_Edges_of G1) c= ( the_Edges_of G2) by A1, Def32;

        hence

         A4: ( the_Vertices_of G1) = ( the_Vertices_of G2) & ( the_Edges_of G1) = ( the_Edges_of G2) by A3, XBOOLE_0:def 10;

        then

         A5: ( dom ( the_Source_of G1)) = ( the_Edges_of G1) & ( dom ( the_Source_of G2)) = ( the_Edges_of G1) by FUNCT_2:def 1;

        for e be object st e in ( dom ( the_Source_of G1)) holds (( the_Source_of G1) . e) = (( the_Source_of G2) . e) by A1, Def32;

        hence ( the_Source_of G1) = ( the_Source_of G2) by A5, FUNCT_1: 2;

        

         A6: ( dom ( the_Target_of G1)) = ( the_Edges_of G1) & ( dom ( the_Target_of G2)) = ( the_Edges_of G1) by A4, FUNCT_2:def 1;

        for e be object st e in ( dom ( the_Target_of G1)) holds (( the_Target_of G1) . e) = (( the_Target_of G2) . e) by A1, Def32;

        hence ( the_Target_of G1) = ( the_Target_of G2) by A6, FUNCT_1: 2;

      end;

      assume that

       A7: ( the_Vertices_of G1) = ( the_Vertices_of G2) & ( the_Edges_of G1) = ( the_Edges_of G2) and

       A8: ( the_Source_of G1) = ( the_Source_of G2) & ( the_Target_of G1) = ( the_Target_of G2);

      for e be set st e in ( the_Edges_of G1) holds (( the_Source_of G1) . e) = (( the_Source_of G2) . e) & (( the_Target_of G1) . e) = (( the_Target_of G2) . e) by A8;

      hence thesis by A7, Def32;

    end;

    theorem :: GLIB_000:42

    for G1 be _Graph, G2 be Subgraph of G1, x be set holds (x in ( the_Vertices_of G2) implies x in ( the_Vertices_of G1)) & (x in ( the_Edges_of G2) implies x in ( the_Edges_of G1));

    theorem :: GLIB_000:43

    

     Th43: for G1 be _Graph, G2 be Subgraph of G1, G3 be Subgraph of G2 holds G3 is Subgraph of G1

    proof

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

      

       A1: ( the_Edges_of G2) c= ( the_Edges_of G1);

      

       A2: ( the_Vertices_of G3) c= ( the_Vertices_of G2);

      now

        thus ( the_Vertices_of G3) c= ( the_Vertices_of G1) by A2, XBOOLE_1: 1;

        thus ( the_Edges_of G3) c= ( the_Edges_of G1) by A1;

        let e be set;

        assume

         A3: e in ( the_Edges_of G3);

        

        hence (( the_Source_of G3) . e) = (( the_Source_of G2) . e) by Def32

        .= (( the_Source_of G1) . e) by A3, Def32;

        

        thus (( the_Target_of G3) . e) = (( the_Target_of G2) . e) by A3, Def32

        .= (( the_Target_of G1) . e) by A3, Def32;

      end;

      hence thesis by Def32;

    end;

    theorem :: GLIB_000:44

    

     Th44: for G be _Graph, G1,G2 be Subgraph of G st ( the_Vertices_of G1) c= ( the_Vertices_of G2) & ( the_Edges_of G1) c= ( the_Edges_of G2) holds G1 is Subgraph of G2

    proof

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

      assume that

       A1: ( the_Vertices_of G1) c= ( the_Vertices_of G2) and

       A2: ( the_Edges_of G1) c= ( the_Edges_of G2);

      now

        let e be set;

        assume

         A3: e in ( the_Edges_of G1);

        

        hence (( the_Source_of G1) . e) = (( the_Source_of G) . e) by Def32

        .= (( the_Source_of G2) . e) by A2, A3, Def32;

        

        thus (( the_Target_of G1) . e) = (( the_Target_of G) . e) by A3, Def32

        .= (( the_Target_of G2) . e) by A2, A3, Def32;

      end;

      hence thesis by A1, A2, Def32;

    end;

    theorem :: GLIB_000:45

    

     Th45: for G1 be _Graph, G2 be Subgraph of G1 holds ( the_Source_of G2) = (( the_Source_of G1) | ( the_Edges_of G2)) & ( the_Target_of G2) = (( the_Target_of G1) | ( the_Edges_of G2))

    proof

      let G1 be _Graph, G2 be Subgraph of G1;

      set S2 = (( the_Source_of G1) | ( the_Edges_of G2));

      set T2 = (( the_Target_of G1) | ( the_Edges_of G2));

       A1:

      now

        let x be object;

        assume

         A2: x in ( dom ( the_Source_of G2));

        

        hence (( the_Source_of G2) . x) = (( the_Source_of G1) . x) by Def32

        .= (S2 . x) by A2, FUNCT_1: 49;

      end;

      ( dom ( the_Source_of G1)) = ( the_Edges_of G1) by FUNCT_2:def 1;

      then ( dom ( the_Source_of G2)) = ( the_Edges_of G2) & ( dom S2) = ( the_Edges_of G2) by FUNCT_2:def 1, RELAT_1: 62;

      hence ( the_Source_of G2) = S2 by A1, FUNCT_1: 2;

       A3:

      now

        let x be object;

        assume

         A4: x in ( dom ( the_Target_of G2));

        

        hence (( the_Target_of G2) . x) = (( the_Target_of G1) . x) by Def32

        .= (T2 . x) by A4, FUNCT_1: 49;

      end;

      ( dom ( the_Target_of G1)) = ( the_Edges_of G1) by FUNCT_2:def 1;

      then ( dom ( the_Target_of G2)) = ( the_Edges_of G2) & ( dom T2) = ( the_Edges_of G2) by FUNCT_2:def 1, RELAT_1: 62;

      hence thesis by A3, FUNCT_1: 2;

    end;

    theorem :: GLIB_000:46

    for G be _Graph, V1,V2,E1,E2 be set, G1 be inducedSubgraph of G, V1, E1, G2 be inducedSubgraph of G, V2, E2 st V2 c= V1 & E2 c= E1 & V2 is non empty Subset of ( the_Vertices_of G) & E2 c= (G .edgesBetween V2) holds G2 is Subgraph of G1

    proof

      let G be _Graph, V1,V2,E1,E2 be set, G1 be inducedSubgraph of G, V1, E1, G2 be inducedSubgraph of G, V2, E2;

      assume that

       A1: V2 c= V1 & E2 c= E1 and

       A2: V2 is non empty Subset of ( the_Vertices_of G) & E2 c= (G .edgesBetween V2);

      

       A3: ( the_Vertices_of G2) = V2 & ( the_Edges_of G2) = E2 by A2, Def37;

      now

        per cases ;

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

          then ( the_Vertices_of G1) = V1 & ( the_Edges_of G1) = E1 by Def37;

          hence thesis by A1, A3, Th44;

        end;

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

          then G1 == G by Def37;

          hence thesis by A3, Th44;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:47

    

     Th47: for G1 be non _trivial _Graph, v be Vertex of G1, G2 be removeVertex of G1, v holds ( the_Vertices_of G2) = (( the_Vertices_of G1) \ {v}) & ( the_Edges_of G2) = (G1 .edgesBetween (( the_Vertices_of G1) \ {v}))

    proof

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

      set VG = ( the_Vertices_of G1), V = (VG \ {v});

      now

        assume V is empty;

        then VG c= {v} by XBOOLE_1: 37;

        then VG = {v} by ZFMISC_1: 33;

        then ( card VG) = 1 by CARD_1: 30;

        hence contradiction by Def19;

      end;

      then

      reconsider V as non empty Subset of VG;

      G2 is inducedSubgraph of G1, V;

      hence thesis by Def37;

    end;

    theorem :: GLIB_000:48

    for G1 be _finite non _trivial _Graph, v be Vertex of G1, G2 be removeVertex of G1, v holds ((G2 .order() ) + 1) = (G1 .order() ) & ((G2 .size() ) + ( card (v .edgesInOut() ))) = (G1 .size() )

    proof

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

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

      set EG1 = ( the_Edges_of G1), EG2 = ( the_Edges_of G2), EV = (v .edgesInOut() );

      

       A1: VG2 = (VG1 \ {v}) by Th47;

      v in {v} by TARSKI:def 1;

      then not v in VG2 by A1, XBOOLE_0:def 5;

      then ( card ((VG1 \ {v}) \/ {v})) = ((G2 .order() ) + 1) by A1, CARD_2: 41;

      hence ((G2 .order() ) + 1) = (G1 .order() ) by XBOOLE_1: 45;

      

       A2: EG2 = (G1 .edgesBetween (VG1 \ {v})) & (G1 .edgesBetween (VG1 \ {v})) = (EG1 \ EV) by Th35, Th47;

      then EG1 = (EG2 \/ EV) by XBOOLE_1: 45;

      hence thesis by A2, CARD_2: 40, XBOOLE_1: 79;

    end;

    theorem :: GLIB_000:49

    

     Th49: for G1 be _Graph, V be set, G2 be removeVertices of G1, V st V c< ( the_Vertices_of G1) holds ( the_Vertices_of G2) = (( the_Vertices_of G1) \ V) & ( the_Edges_of G2) = (G1 .edgesBetween (( the_Vertices_of G1) \ V))

    proof

      let G1 be _Graph, V be set, G2 be removeVertices of G1, V;

      set VG2 = (( the_Vertices_of G1) \ V);

      assume

       A1: V c< ( the_Vertices_of G1);

      now

        assume VG2 is empty;

        then ( the_Vertices_of G1) c= V by XBOOLE_1: 37;

        hence contradiction by A1, XBOOLE_0:def 8;

      end;

      then

      reconsider VG2 as non empty Subset of ( the_Vertices_of G1);

      G2 is inducedSubgraph of G1, VG2;

      hence thesis by Def37;

    end;

    theorem :: GLIB_000:50

    for G1 be _finite _Graph, V be Subset of ( the_Vertices_of G1), G2 be removeVertices of G1, V st V <> ( the_Vertices_of G1) holds ((G2 .order() ) + ( card V)) = (G1 .order() ) & ((G2 .size() ) + ( card (G1 .edgesInOut V))) = (G1 .size() )

    proof

      let G1 be _finite _Graph, V be Subset of ( the_Vertices_of G1), G2 be removeVertices of G1, V;

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

      set EG1 = ( the_Edges_of G1), EG2 = ( the_Edges_of G2);

      

       A1: (G1 .edgesBetween (VG1 \ V)) = (EG1 \ (G1 .edgesInOut V)) by Th35;

      assume V <> VG1;

      then

       A2: V c< VG1 by XBOOLE_0:def 8;

      then

       A3: VG2 = (VG1 \ V) by Th49;

      then ( card (VG2 \/ V)) = (( card VG2) + ( card V)) by CARD_2: 40, XBOOLE_1: 79;

      hence ((G2 .order() ) + ( card V)) = (G1 .order() ) by A3, XBOOLE_1: 45;

      

       A4: EG2 = (G1 .edgesBetween (VG1 \ V)) by A2, Th49;

      then EG1 = (EG2 \/ (G1 .edgesInOut V)) by A1, XBOOLE_1: 45;

      hence thesis by A4, A1, CARD_2: 40, XBOOLE_1: 79;

    end;

    theorem :: GLIB_000:51

    

     Th51: for G1 be _Graph, e be set, G2 be removeEdge of G1, e holds ( the_Vertices_of G2) = ( the_Vertices_of G1) & ( the_Edges_of G2) = (( the_Edges_of G1) \ {e})

    proof

      let G1 be _Graph, e be set, G2 be removeEdge of G1, e;

      set V = ( the_Vertices_of G1);

      V c= V;

      then

      reconsider V as non empty Subset of ( the_Vertices_of G1);

      set E = (( the_Edges_of G1) \ {e});

      reconsider E as Subset of (G1 .edgesBetween V) by Th34;

      G2 is inducedSubgraph of G1, V, E;

      hence thesis by Def37;

    end;

    theorem :: GLIB_000:52

    for G1 be _finite _Graph, e be set, G2 be removeEdge of G1, e holds (G1 .order() ) = (G2 .order() ) & (e in ( the_Edges_of G1) implies ((G2 .size() ) + 1) = (G1 .size() ))

    proof

      let G1 be _finite _Graph, e be set, G2 be removeEdge of G1, e;

      

       A1: ( the_Edges_of G2) = (( the_Edges_of G1) \ {e}) by Th51;

      thus (G1 .order() ) = (G2 .order() ) by Th51;

      assume e in ( the_Edges_of G1);

      then for x be object st x in {e} holds x in ( the_Edges_of G1) by TARSKI:def 1;

      then {e} c= ( the_Edges_of G1);

      then

       A2: ( the_Edges_of G1) = (( the_Edges_of G2) \/ {e}) by A1, XBOOLE_1: 45;

      e in {e} by TARSKI:def 1;

      then not e in ( the_Edges_of G2) by A1, XBOOLE_0:def 5;

      hence thesis by A2, CARD_2: 41;

    end;

    theorem :: GLIB_000:53

    

     Th53: for G1 be _Graph, E be set, G2 be removeEdges of G1, E holds ( the_Vertices_of G2) = ( the_Vertices_of G1) & ( the_Edges_of G2) = (( the_Edges_of G1) \ E)

    proof

      let G1 be _Graph, E be set, G2 be removeEdges of G1, E;

      set V = ( the_Vertices_of G1);

      V c= V;

      then

      reconsider V as non empty Subset of ( the_Vertices_of G1);

      set E2 = (( the_Edges_of G1) \ E);

      reconsider E2 as Subset of (G1 .edgesBetween V) by Th34;

      G2 is inducedSubgraph of G1, V, E2;

      hence thesis by Def37;

    end;

    theorem :: GLIB_000:54

    for G1 be _Graph, E be set, G2 be removeEdges of G1, E holds (G1 .order() ) = (G2 .order() ) by Th53;

    theorem :: GLIB_000:55

    for G1 be _finite _Graph, E be Subset of ( the_Edges_of G1), G2 be removeEdges of G1, E holds ((G2 .size() ) + ( card E)) = (G1 .size() )

    proof

      let G1 be _finite _Graph, E be Subset of ( the_Edges_of G1), G2 be removeEdges of G1, E;

      

       A1: ( the_Edges_of G2) = (( the_Edges_of G1) \ E) by Th53;

      then ( the_Edges_of G1) = (( the_Edges_of G2) \/ E) by XBOOLE_1: 45;

      hence thesis by A1, CARD_2: 40, XBOOLE_1: 79;

    end;

    theorem :: GLIB_000:56

    e in (v .edgesIn() ) iff e in ( the_Edges_of G) & (( the_Target_of G) . e) = v by Lm7;

    theorem :: GLIB_000:57

    e in (v .edgesIn() ) iff ex x be set st e DJoins (x,v,G)

    proof

      hereby

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

        assume

         A1: e in (v .edgesIn() );

        take x;

        (( the_Target_of G) . e) = v by A1, Lm7;

        hence e DJoins (x,v,G) by A1;

      end;

      given x be set such that

       A2: e DJoins (x,v,G);

      e in ( the_Edges_of G) & (( the_Target_of G) . e) = v by A2;

      hence thesis by Lm7;

    end;

    theorem :: GLIB_000:58

    e in (v .edgesOut() ) iff e in ( the_Edges_of G) & (( the_Source_of G) . e) = v by Lm8;

    theorem :: GLIB_000:59

    e in (v .edgesOut() ) iff ex x be set st e DJoins (v,x,G)

    proof

      hereby

        set x = (( the_Target_of G) . e);

        assume

         A1: e in (v .edgesOut() );

        take x;

        (( the_Source_of G) . e) = v by A1, Lm8;

        hence e DJoins (v,x,G) by A1;

      end;

      given x be set such that

       A2: e DJoins (v,x,G);

      e in ( the_Edges_of G) & (( the_Source_of G) . e) = v by A2;

      hence thesis by Lm8;

    end;

    theorem :: GLIB_000:60

    (v .edgesInOut() ) = ((v .edgesIn() ) \/ (v .edgesOut() ));

    theorem :: GLIB_000:61

    

     Th61: e in (v .edgesInOut() ) iff e in ( the_Edges_of G) & ((( the_Source_of G) . e) = v or (( the_Target_of G) . e) = v)

    proof

      hereby

        assume

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

        hence e in ( the_Edges_of G);

        e in (v .edgesIn() ) or e in (v .edgesOut() ) by A1, XBOOLE_0:def 3;

        hence (( the_Source_of G) . e) = v or (( the_Target_of G) . e) = v by Lm7, Lm8;

      end;

      assume e in ( the_Edges_of G) & ((( the_Source_of G) . e) = v or (( the_Target_of G) . e) = v);

      then e in (v .edgesIn() ) or e in (v .edgesOut() ) by Lm7, Lm8;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: GLIB_000:62

    

     Th62: for e,x be object holds e Joins (v1,x,G) implies e in (v1 .edgesInOut() ) by Th61;

    theorem :: GLIB_000:63

    

     Th63: e Joins (v1,v2,G) implies e in (v1 .edgesIn() ) & e in (v2 .edgesOut() ) or e in (v2 .edgesIn() ) & e in (v1 .edgesOut() )

    proof

      assume

       A1: e Joins (v1,v2,G);

      then

       A2: e in ( the_Edges_of G);

      now

        per cases by A1;

          suppose (( the_Source_of G) . e) = v1 & (( the_Target_of G) . e) = v2;

          hence thesis by A2, Lm7, Lm8;

        end;

          suppose (( the_Source_of G) . e) = v2 & (( the_Target_of G) . e) = v1;

          hence thesis by A2, Lm7, Lm8;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:64

    e in (v1 .edgesInOut() ) iff ex v2 be Vertex of G st e Joins (v1,v2,G)

    proof

      hereby

        assume

         A1: e in (v1 .edgesInOut() );

        now

          per cases by A1, Th61;

            suppose

             A2: (( the_Source_of G) . e) = v1;

            set v2 = (( the_Target_of G) . e);

            reconsider v2 as Vertex of G by A1, FUNCT_2: 5;

            take v2;

            thus e Joins (v1,v2,G) by A1, A2;

          end;

            suppose

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

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

            reconsider v2 as Vertex of G by A1, FUNCT_2: 5;

            take v2;

            thus e Joins (v1,v2,G) by A1, A3;

          end;

        end;

        hence ex v2 be Vertex of G st e Joins (v1,v2,G);

      end;

      given v2 be Vertex of G such that

       A4: e Joins (v1,v2,G);

      thus thesis by A4, Th62;

    end;

    theorem :: GLIB_000:65

    for e,x,y be object holds e in (v .edgesInOut() ) & e Joins (x,y,G) implies v = x or v = y

    proof

      let e,x,y be object;

      assume that

       A1: e in (v .edgesInOut() ) and

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

      now

        assume

         A3: v <> x;

        now

          per cases by A1, Th61;

            suppose (( the_Source_of G) . e) = v;

            hence v = y by A2, A3;

          end;

            suppose (( the_Target_of G) . e) = v;

            hence v = y by A2, A3;

          end;

        end;

        hence v = y;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:66

    for e be object holds e Joins (v1,v2,G) implies (v1 .adj e) = v2 & (v2 .adj e) = v1

    proof

      let e be object;

      assume

       A1: e Joins (v1,v2,G);

      then

       A2: e in (v1 .edgesInOut() ) by Th62;

      now

        per cases by A1;

          suppose

           A3: (( the_Source_of G) . e) = v2 & (( the_Target_of G) . e) = v1;

          hence (v1 .adj e) = v2 by A2, Def41;

          now

            per cases ;

              suppose v1 = v2;

              hence (v2 .adj e) = v1 by A2, A3, Def41;

            end;

              suppose v1 <> v2;

              hence (v2 .adj e) = v1 by A2, A3, Def41;

            end;

          end;

          hence (v2 .adj e) = v1;

        end;

          suppose

           A4: (( the_Source_of G) . e) = v1 & (( the_Target_of G) . e) = v2;

          now

            per cases ;

              suppose v1 = v2;

              hence (v1 .adj e) = v2 by A2, A4, Def41;

            end;

              suppose v1 <> v2;

              hence (v1 .adj e) = v2 by A2, A4, Def41;

            end;

          end;

          hence (v1 .adj e) = v2;

          thus (v2 .adj e) = v1 by A2, A4, Def41;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:67

    e in (v .edgesInOut() ) iff e Joins (v,(v .adj e),G)

    proof

      hereby

        assume

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

        then

         A2: (( the_Source_of G) . e) = v or (( the_Target_of G) . e) = v by Th61;

        now

          per cases ;

            suppose

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

            then (v .adj e) = (( the_Source_of G) . e) by A1, Def41;

            hence e Joins (v,(v .adj e),G) by A1, A3;

          end;

            suppose

             A4: (( the_Target_of G) . e) <> v;

            then (v .adj e) = (( the_Target_of G) . e) by A1, A2, Def41;

            hence e Joins (v,(v .adj e),G) by A1, A2, A4;

          end;

        end;

        hence e Joins (v,(v .adj e),G);

      end;

      assume e Joins (v,(v .adj e),G);

      hence thesis by Th62;

    end;

    theorem :: GLIB_000:68

    for G be _finite _Graph, e be set, v1,v2 be Vertex of G holds e Joins (v1,v2,G) implies 1 <= (v1 .degree() ) & 1 <= (v2 .degree() )

    proof

      let G be _finite _Graph, e be set, v1,v2 be Vertex of G;

      assume

       A1: e Joins (v1,v2,G);

      now

        per cases by A1, Th63;

          suppose

           A2: e in (v1 .edgesIn() ) & e in (v2 .edgesOut() );

          then for x be object st x in {e} holds x in (v1 .edgesIn() ) by TARSKI:def 1;

          then {e} c= (v1 .edgesIn() );

          then ( card {e}) <= ( card (v1 .edgesIn() )) by NAT_1: 43;

          then 1 <= (v1 .inDegree() ) by CARD_1: 30;

          hence 1 <= (v1 .degree() ) by NAT_1: 12;

          for x be object st x in {e} holds x in (v2 .edgesOut() ) by A2, TARSKI:def 1;

          then {e} c= (v2 .edgesOut() );

          then ( card {e}) <= ( card (v2 .edgesOut() )) by NAT_1: 43;

          then 1 <= (v2 .outDegree() ) by CARD_1: 30;

          hence 1 <= (v2 .degree() ) by NAT_1: 12;

        end;

          suppose

           A3: e in (v2 .edgesIn() ) & e in (v1 .edgesOut() );

          then for x be object st x in {e} holds x in (v1 .edgesOut() ) by TARSKI:def 1;

          then {e} c= (v1 .edgesOut() );

          then ( card {e}) <= ( card (v1 .edgesOut() )) by NAT_1: 43;

          then 1 <= (v1 .outDegree() ) by CARD_1: 30;

          hence 1 <= (v1 .degree() ) by NAT_1: 12;

          for x be object st x in {e} holds x in (v2 .edgesIn() ) by A3, TARSKI:def 1;

          then {e} c= (v2 .edgesIn() );

          then ( card {e}) <= ( card (v2 .edgesIn() )) by NAT_1: 43;

          then 1 <= (v2 .inDegree() ) by CARD_1: 30;

          hence 1 <= (v2 .degree() ) by NAT_1: 12;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:69

    

     Th69: x in (v .inNeighbors() ) iff ex e be object st e DJoins (x,v,G)

    proof

      hereby

        assume x in (v .inNeighbors() );

        then

        consider e be object such that

         A1: e in ( dom ( the_Source_of G)) and

         A2: e in (v .edgesIn() ) and

         A3: x = (( the_Source_of G) . e) by FUNCT_1:def 6;

        take e;

        (( the_Target_of G) . e) = v by A2, Lm7;

        hence e DJoins (x,v,G) by A1, A3;

      end;

      given e be object such that

       A4: e DJoins (x,v,G);

      

       A5: e in ( the_Edges_of G) by A4;

      then

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

      (( the_Target_of G) . e) = v by A4;

      then

       A7: e in (v .edgesIn() ) by A5, Lm7;

      (( the_Source_of G) . e) = x by A4;

      hence thesis by A7, A6, FUNCT_1:def 6;

    end;

    theorem :: GLIB_000:70

    

     Th70: x in (v .outNeighbors() ) iff ex e be object st e DJoins (v,x,G)

    proof

      hereby

        assume x in (v .outNeighbors() );

        then

        consider e be object such that

         A1: e in ( dom ( the_Target_of G)) and

         A2: e in (v .edgesOut() ) and

         A3: x = (( the_Target_of G) . e) by FUNCT_1:def 6;

        take e;

        (( the_Source_of G) . e) = v by A2, Lm8;

        hence e DJoins (v,x,G) by A1, A3;

      end;

      given e be object such that

       A4: e DJoins (v,x,G);

      

       A5: e in ( the_Edges_of G) by A4;

      then

       A6: e in ( dom ( the_Target_of G)) by FUNCT_2:def 1;

      (( the_Source_of G) . e) = v by A4;

      then

       A7: e in (v .edgesOut() ) by A5, Lm8;

      (( the_Target_of G) . e) = x by A4;

      hence thesis by A7, A6, FUNCT_1:def 6;

    end;

    theorem :: GLIB_000:71

    

     Th71: x in (v .allNeighbors() ) iff ex e be object st e Joins (v,x,G)

    proof

      hereby

        assume

         A1: x in (v .allNeighbors() );

        now

          per cases by A1, XBOOLE_0:def 3;

            suppose x in (v .inNeighbors() );

            then

            consider e be object such that

             A2: e DJoins (x,v,G) by Th69;

            take e;

            thus e Joins (v,x,G) by A2;

          end;

            suppose x in (v .outNeighbors() );

            then

            consider e be object such that

             A3: e DJoins (v,x,G) by Th70;

            take e;

            thus e Joins (v,x,G) by A3;

          end;

        end;

        hence ex e be object st e Joins (v,x,G);

      end;

      given e be object such that

       A4: e Joins (v,x,G);

      now

        per cases by A4;

          suppose e DJoins (x,v,G);

          then x in (v .inNeighbors() ) by Th69;

          hence x in ((v .inNeighbors() ) \/ (v .outNeighbors() )) by XBOOLE_0:def 3;

        end;

          suppose e DJoins (v,x,G);

          then x in (v .outNeighbors() ) by Th70;

          hence x in ((v .inNeighbors() ) \/ (v .outNeighbors() )) by XBOOLE_0:def 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:72

    

     Th72: for G1 be _Graph, G2 be Subgraph of G1, x,y be set, e be object holds (e Joins (x,y,G2) implies e Joins (x,y,G1)) & (e DJoins (x,y,G2) implies e DJoins (x,y,G1)) & (e SJoins (x,y,G2) implies e SJoins (x,y,G1)) & (e DSJoins (x,y,G2) implies e DSJoins (x,y,G1))

    proof

      let G1 be _Graph, G2 be Subgraph of G1, x,y be set, e be object;

      thus e Joins (x,y,G2) implies e Joins (x,y,G1) by Lm4;

      hereby

        assume

         A1: e DJoins (x,y,G2);

        then

         A2: e in ( the_Edges_of G2);

        (( the_Target_of G2) . e) = y by A1;

        then

         A3: (( the_Target_of G1) . e) = y by A2, Def32;

        (( the_Source_of G2) . e) = x by A1;

        then (( the_Source_of G1) . e) = x by A2, Def32;

        hence e DJoins (x,y,G1) by A2, A3;

      end;

      hereby

        assume

         A4: e SJoins (x,y,G2);

        then

         A5: (( the_Source_of G2) . e) in x & (( the_Target_of G2) . e) in y or (( the_Source_of G2) . e) in y & (( the_Target_of G2) . e) in x;

        

         A6: e in ( the_Edges_of G2) by A4;

        then (( the_Source_of G2) . e) = (( the_Source_of G1) . e) & (( the_Target_of G2) . e) = (( the_Target_of G1) . e) by Def32;

        hence e SJoins (x,y,G1) by A6, A5;

      end;

      assume

       A7: e DSJoins (x,y,G2);

      then

       A8: (( the_Source_of G2) . e) in x & (( the_Target_of G2) . e) in y;

      

       A9: e in ( the_Edges_of G2) by A7;

      then (( the_Source_of G2) . e) = (( the_Source_of G1) . e) & (( the_Target_of G2) . e) = (( the_Target_of G1) . e) by Def32;

      hence thesis by A9, A8;

    end;

    theorem :: GLIB_000:73

    for G1 be _Graph, G2 be Subgraph of G1, x,y,e be set st e in ( the_Edges_of G2) holds (e Joins (x,y,G1) implies e Joins (x,y,G2)) & (e DJoins (x,y,G1) implies e DJoins (x,y,G2)) & (e SJoins (x,y,G1) implies e SJoins (x,y,G2)) & (e DSJoins (x,y,G1) implies e DSJoins (x,y,G2)) by Def32;

    theorem :: GLIB_000:74

    for G1 be _Graph, G2 be spanning Subgraph of G1, G3 be spanning Subgraph of G2 holds G3 is spanning Subgraph of G1

    proof

      let G1 be _Graph, G2 be spanning Subgraph of G1, G3 be spanning Subgraph of G2;

      ( the_Vertices_of G3) = ( the_Vertices_of G2) by Def33

      .= ( the_Vertices_of G1) by Def33;

      hence thesis by Def33, Th43;

    end;

    theorem :: GLIB_000:75

    for G1 be _finite _Graph, G2 be Subgraph of G1 holds (G2 .order() ) <= (G1 .order() ) & (G2 .size() ) <= (G1 .size() )

    proof

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

      ( card ( the_Vertices_of G2)) <= ( card ( the_Vertices_of G1)) by NAT_1: 43;

      hence (G2 .order() ) <= (G1 .order() );

      ( card ( the_Edges_of G2)) <= ( card ( the_Edges_of G1)) by NAT_1: 43;

      hence thesis;

    end;

    theorem :: GLIB_000:76

    for G1 be _Graph, G2 be Subgraph of G1, X be set holds (G2 .edgesInto X) c= (G1 .edgesInto X) & (G2 .edgesOutOf X) c= (G1 .edgesOutOf X) & (G2 .edgesInOut X) c= (G1 .edgesInOut X) & (G2 .edgesBetween X) c= (G1 .edgesBetween X)

    proof

      let G1 be _Graph, G2 be Subgraph of G1, X be set;

      now

        let e be object;

        assume

         A1: e in (G2 .edgesInto X);

        then

         A2: (( the_Target_of G2) . e) = (( the_Target_of G1) . e) by Def32;

        e in ( the_Edges_of G2) & (( the_Target_of G2) . e) in X by A1, Def26;

        hence e in (G1 .edgesInto X) by A2, Def26;

      end;

      hence

       A3: (G2 .edgesInto X) c= (G1 .edgesInto X);

      then

       A4: (G2 .edgesInto X) c= (G1 .edgesInOut X) by XBOOLE_1: 10;

      now

        let e be object;

        assume

         A5: e in (G2 .edgesOutOf X);

        then

         A6: (( the_Source_of G2) . e) = (( the_Source_of G1) . e) by Def32;

        e in ( the_Edges_of G2) & (( the_Source_of G2) . e) in X by A5, Def27;

        hence e in (G1 .edgesOutOf X) by A6, Def27;

      end;

      hence

       A7: (G2 .edgesOutOf X) c= (G1 .edgesOutOf X);

      then (G2 .edgesOutOf X) c= (G1 .edgesInOut X) by XBOOLE_1: 10;

      hence (G2 .edgesInOut X) c= (G1 .edgesInOut X) by A4, XBOOLE_1: 8;

      thus thesis by A3, A7, XBOOLE_1: 27;

    end;

    theorem :: GLIB_000:77

    for G1 be _Graph, G2 be Subgraph of G1, X,Y be set holds (G2 .edgesBetween (X,Y)) c= (G1 .edgesBetween (X,Y)) & (G2 .edgesDBetween (X,Y)) c= (G1 .edgesDBetween (X,Y))

    proof

      let G1 be _Graph, G2 be Subgraph of G1, X,Y be set;

      now

        let x be object;

        assume x in (G2 .edgesBetween (X,Y));

        then x SJoins (X,Y,G2) by Def30;

        then x SJoins (X,Y,G1) by Th72;

        hence x in (G1 .edgesBetween (X,Y)) by Def30;

      end;

      hence (G2 .edgesBetween (X,Y)) c= (G1 .edgesBetween (X,Y));

      now

        let x be object;

        assume x in (G2 .edgesDBetween (X,Y));

        then x DSJoins (X,Y,G2) by Def31;

        then x DSJoins (X,Y,G1) by Th72;

        hence x in (G1 .edgesDBetween (X,Y)) by Def31;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:78

    

     Th78: for G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2 st v1 = v2 holds (v2 .edgesIn() ) c= (v1 .edgesIn() ) & (v2 .edgesOut() ) c= (v1 .edgesOut() ) & (v2 .edgesInOut() ) c= (v1 .edgesInOut() )

    proof

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

      assume

       A1: v1 = v2;

      now

        let x be object;

        assume

         A2: x in (v2 .edgesIn() );

        then (( the_Target_of G2) . x) = v2 by Lm7;

        then

         A3: (( the_Target_of G1) . x) = v1 by A1, A2, Def32;

        x in ( the_Edges_of G2) by A2;

        hence x in (v1 .edgesIn() ) by A3, Lm7;

      end;

      hence (v2 .edgesIn() ) c= (v1 .edgesIn() );

      now

        let x be object;

        assume

         A4: x in (v2 .edgesOut() );

        then (( the_Source_of G2) . x) = v2 by Lm8;

        then

         A5: (( the_Source_of G1) . x) = v1 by A1, A4, Def32;

        x in ( the_Edges_of G2) by A4;

        hence x in (v1 .edgesOut() ) by A5, Lm8;

      end;

      hence (v2 .edgesOut() ) c= (v1 .edgesOut() );

      now

        let x be object;

        assume

         A6: x in (v2 .edgesInOut() );

        then (( the_Source_of G2) . x) = v2 or (( the_Target_of G2) . x) = v2 by Th61;

        then

         A7: (( the_Source_of G1) . x) = v1 or (( the_Target_of G1) . x) = v1 by A1, A6, Def32;

        x in ( the_Edges_of G2) by A6;

        hence x in (v1 .edgesInOut() ) by A7, Th61;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:79

    

     Th79: for G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2 st v1 = v2 holds (v2 .edgesIn() ) = ((v1 .edgesIn() ) /\ ( the_Edges_of G2)) & (v2 .edgesOut() ) = ((v1 .edgesOut() ) /\ ( the_Edges_of G2)) & (v2 .edgesInOut() ) = ((v1 .edgesInOut() ) /\ ( the_Edges_of G2))

    proof

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

      assume

       A1: v1 = v2;

      now

        let x be object;

        hereby

          assume

           A2: x in (v2 .edgesIn() );

          (v2 .edgesIn() ) c= (v1 .edgesIn() ) by A1, Th78;

          hence x in ((v1 .edgesIn() ) /\ ( the_Edges_of G2)) by A2, XBOOLE_0:def 4;

        end;

        assume

         A3: x in ((v1 .edgesIn() ) /\ ( the_Edges_of G2));

        then

         A4: x in ( the_Edges_of G2) by XBOOLE_0:def 4;

        x in (v1 .edgesIn() ) by A3, XBOOLE_0:def 4;

        then (( the_Target_of G1) . x) = v1 by Lm7;

        then (( the_Target_of G2) . x) = v2 by A1, A4, Def32;

        hence x in (v2 .edgesIn() ) by A4, Lm7;

      end;

      hence

       A5: (v2 .edgesIn() ) = ((v1 .edgesIn() ) /\ ( the_Edges_of G2)) by TARSKI: 2;

      now

        let x be object;

        hereby

          assume

           A6: x in (v2 .edgesOut() );

          (v2 .edgesOut() ) c= (v1 .edgesOut() ) by A1, Th78;

          hence x in ((v1 .edgesOut() ) /\ ( the_Edges_of G2)) by A6, XBOOLE_0:def 4;

        end;

        assume

         A7: x in ((v1 .edgesOut() ) /\ ( the_Edges_of G2));

        then

         A8: x in ( the_Edges_of G2) by XBOOLE_0:def 4;

        x in (v1 .edgesOut() ) by A7, XBOOLE_0:def 4;

        then (( the_Source_of G1) . x) = v1 by Lm8;

        then (( the_Source_of G2) . x) = v2 by A1, A8, Def32;

        hence x in (v2 .edgesOut() ) by A8, Lm8;

      end;

      hence

       A9: (v2 .edgesOut() ) = ((v1 .edgesOut() ) /\ ( the_Edges_of G2)) by TARSKI: 2;

      now

        let x be object;

        hereby

          assume

           A10: x in ((v1 .edgesInOut() ) /\ ( the_Edges_of G2));

          then

           A11: x in ( the_Edges_of G2) by XBOOLE_0:def 4;

          

           A12: x in (v1 .edgesInOut() ) by A10, XBOOLE_0:def 4;

          now

            per cases by A12, XBOOLE_0:def 3;

              suppose x in (v1 .edgesIn() );

              then x in ((v1 .edgesIn() ) /\ ( the_Edges_of G2)) by A11, XBOOLE_0:def 4;

              hence x in (v2 .edgesInOut() ) by A5, XBOOLE_0:def 3;

            end;

              suppose x in (v1 .edgesOut() );

              then x in ((v1 .edgesOut() ) /\ ( the_Edges_of G2)) by A11, XBOOLE_0:def 4;

              hence x in (v2 .edgesInOut() ) by A9, XBOOLE_0:def 3;

            end;

          end;

          hence x in (v2 .edgesInOut() );

        end;

        assume

         A13: x in (v2 .edgesInOut() );

        now

          per cases by A5, A9, A13, XBOOLE_0:def 3;

            suppose

             A14: x in ((v1 .edgesIn() ) /\ ( the_Edges_of G2));

            then x in (v1 .edgesIn() ) by XBOOLE_0:def 4;

            then

             A15: x in ((v1 .edgesIn() ) \/ (v1 .edgesOut() )) by XBOOLE_0:def 3;

            x in ( the_Edges_of G2) by A14, XBOOLE_0:def 4;

            hence x in ((v1 .edgesInOut() ) /\ ( the_Edges_of G2)) by A15, XBOOLE_0:def 4;

          end;

            suppose

             A16: x in ((v1 .edgesOut() ) /\ ( the_Edges_of G2));

            then x in (v1 .edgesOut() ) by XBOOLE_0:def 4;

            then

             A17: x in ((v1 .edgesIn() ) \/ (v1 .edgesOut() )) by XBOOLE_0:def 3;

            x in ( the_Edges_of G2) by A16, XBOOLE_0:def 4;

            hence x in ((v1 .edgesInOut() ) /\ ( the_Edges_of G2)) by A17, XBOOLE_0:def 4;

          end;

        end;

        hence x in ((v1 .edgesInOut() ) /\ ( the_Edges_of G2));

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLIB_000:80

    for G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2, e be set st v1 = v2 & e in ( the_Edges_of G2) holds (v1 .adj e) = (v2 .adj e)

    proof

      let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2, e be set;

      assume that

       A1: v1 = v2 and

       A2: e in ( the_Edges_of G2);

      

       A3: (( the_Source_of G2) . e) = (( the_Source_of G1) . e) & (( the_Target_of G2) . e) = (( the_Target_of G1) . e) by A2, Def32;

      now

        per cases ;

          suppose

           A4: (( the_Target_of G1) . e) = v1;

          

          hence (v1 .adj e) = (( the_Source_of G1) . e) by A2, Def41

          .= (v2 .adj e) by A1, A2, A3, A4, Def41;

        end;

          suppose

           A5: (( the_Source_of G1) . e) = v1 & (( the_Target_of G1) . e) <> v1;

          

          hence (v1 .adj e) = (( the_Target_of G1) . e) by A2, Def41

          .= (v2 .adj e) by A1, A2, A3, A5, Def41;

        end;

          suppose

           A6: (( the_Source_of G1) . e) <> v1 & (( the_Target_of G1) . e) <> v1;

          

          hence (v1 .adj e) = v2 by A1, Def41

          .= (v2 .adj e) by A1, A3, A6, Def41;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:81

    for G1 be _finite _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2 st v1 = v2 holds (v2 .inDegree() ) <= (v1 .inDegree() ) & (v2 .outDegree() ) <= (v1 .outDegree() ) & (v2 .degree() ) <= (v1 .degree() )

    proof

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

      assume

       A1: v1 = v2;

      then (v2 .edgesIn() ) = ((v1 .edgesIn() ) /\ ( the_Edges_of G2)) by Th79;

      hence

       A2: (v2 .inDegree() ) <= (v1 .inDegree() ) by NAT_1: 43, XBOOLE_1: 17;

      

       A3: (v2 .edgesOut() ) = ((v1 .edgesOut() ) /\ ( the_Edges_of G2)) by A1, Th79;

      hence (v2 .outDegree() ) <= (v1 .outDegree() ) by NAT_1: 43, XBOOLE_1: 17;

      (v2 .outDegree() ) <= ( card (v1 .edgesOut() )) by A3, NAT_1: 43, XBOOLE_1: 17;

      hence thesis by A2, XREAL_1: 7;

    end;

    theorem :: GLIB_000:82

    for G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2 st v1 = v2 holds (v2 .inNeighbors() ) c= (v1 .inNeighbors() ) & (v2 .outNeighbors() ) c= (v1 .outNeighbors() ) & (v2 .allNeighbors() ) c= (v1 .allNeighbors() )

    proof

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

      assume

       A1: v1 = v2;

      now

        let v be object;

        assume v in (v2 .inNeighbors() );

        then

        consider e be object such that

         A2: e DJoins (v,v2,G2) by Th69;

        e DJoins (v,v1,G1) by A1, A2, Th72;

        hence v in (v1 .inNeighbors() ) by Th69;

      end;

      hence (v2 .inNeighbors() ) c= (v1 .inNeighbors() );

      now

        let v be object;

        assume v in (v2 .outNeighbors() );

        then

        consider e be object such that

         A3: e DJoins (v2,v,G2) by Th70;

        e DJoins (v1,v,G1) by A1, A3, Th72;

        hence v in (v1 .outNeighbors() ) by Th70;

      end;

      hence (v2 .outNeighbors() ) c= (v1 .outNeighbors() );

      let v be object;

      assume v in (v2 .allNeighbors() );

      then

      consider e be object such that

       A4: e Joins (v2,v,G2) by Th71;

      e Joins (v1,v,G1) by A1, A4, Lm4;

      hence v in (v1 .allNeighbors() ) by Th71;

    end;

    theorem :: GLIB_000:83

    for G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2 st v1 = v2 & v1 is isolated holds v2 is isolated

    proof

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

      assume v1 = v2 & v1 is isolated;

      then (v1 .edgesInOut() ) = {} & (v2 .edgesInOut() ) c= (v1 .edgesInOut() ) by Th78;

      hence thesis;

    end;

    theorem :: GLIB_000:84

    for G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2 st v1 = v2 & v1 is endvertex holds v2 is endvertex or v2 is isolated

    proof

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

      assume that

       A1: v1 = v2 and

       A2: v1 is endvertex;

      consider e be object such that

       A3: (v1 .edgesInOut() ) = {e} and

       A4: not e Joins (v1,v1,G1) by A2;

      (v2 .edgesInOut() ) c= (v1 .edgesInOut() ) by A1, Th78;

      then

       A5: (v2 .edgesInOut() ) = {} or (v2 .edgesInOut() ) = {e} by A3, ZFMISC_1: 33;

       not v2 is isolated implies v2 is endvertex by A5, A1, A4, Lm4;

      hence thesis;

    end;

    theorem :: GLIB_000:85

    G1 == G2 & G2 == G3 implies G1 == G3;

    theorem :: GLIB_000:86

    

     Th86: for G be _Graph, G1,G2 be Subgraph of G st ( the_Vertices_of G1) = ( the_Vertices_of G2) & ( the_Edges_of G1) = ( the_Edges_of G2) holds G1 == G2

    proof

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

      assume that

       A1: ( the_Vertices_of G1) = ( the_Vertices_of G2) and

       A2: ( the_Edges_of G1) = ( the_Edges_of G2);

      

       A3: ( dom ( the_Target_of G1)) = ( the_Edges_of G1) & ( dom ( the_Target_of G2)) = ( the_Edges_of G2) by FUNCT_2:def 1;

      now

        let e be object;

        assume

         A4: e in ( the_Edges_of G1);

        then (( the_Target_of G1) . e) = (( the_Target_of G) . e) by Def32;

        hence (( the_Target_of G1) . e) = (( the_Target_of G2) . e) by A2, A4, Def32;

      end;

      then

       A5: ( the_Target_of G1) = ( the_Target_of G2) by A2, A3, FUNCT_1: 2;

       A6:

      now

        let e be object;

        assume

         A7: e in ( the_Edges_of G1);

        then (( the_Source_of G1) . e) = (( the_Source_of G) . e) by Def32;

        hence (( the_Source_of G1) . e) = (( the_Source_of G2) . e) by A2, A7, Def32;

      end;

      ( dom ( the_Source_of G1)) = ( the_Edges_of G1) & ( dom ( the_Source_of G2)) = ( the_Edges_of G2) by FUNCT_2:def 1;

      then ( the_Source_of G1) = ( the_Source_of G2) by A2, A6, FUNCT_1: 2;

      hence thesis by A1, A2, A5;

    end;

    theorem :: GLIB_000:87

    

     Th87: G1 == G2 iff G1 is Subgraph of G2 & G2 is Subgraph of G1 by Th41;

    theorem :: GLIB_000:88

    for e,x,y be object holds G1 == G2 implies (e Joins (x,y,G1) implies e Joins (x,y,G2)) & (e DJoins (x,y,G1) implies e DJoins (x,y,G2)) & (e SJoins (X,Y,G1) implies e SJoins (X,Y,G2)) & (e DSJoins (X,Y,G1) implies e DSJoins (X,Y,G2));

    theorem :: GLIB_000:89

    G1 == G2 implies (G1 is _finite implies G2 is _finite) & (G1 is loopless implies G2 is loopless) & (G1 is _trivial implies G2 is _trivial) & (G1 is non-multi implies G2 is non-multi) & (G1 is non-Dmulti implies G2 is non-Dmulti) & (G1 is simple implies G2 is simple) & (G1 is Dsimple implies G2 is Dsimple)

    proof

      assume

       A1: G1 == G2;

      then

       A2: ( the_Edges_of G1) = ( the_Edges_of G2);

      ( the_Vertices_of G1) = ( the_Vertices_of G2) by A1;

      hence G1 is _finite implies G2 is _finite by A2;

      

       A3: ( the_Source_of G1) = ( the_Source_of G2) & ( the_Target_of G1) = ( the_Target_of G2) by A1;

      

       A4: G1 is loopless implies G2 is loopless by A2, A3;

      hence G1 is loopless implies G2 is loopless;

      thus G1 is _trivial implies G2 is _trivial by A1;

       A5:

      now

        assume

         A6: G1 is non-multi;

        now

          let e1,e2,v1,v2 be object;

          assume e1 Joins (v1,v2,G2) & e2 Joins (v1,v2,G2);

          then e1 Joins (v1,v2,G1) & e2 Joins (v1,v2,G1) by A1;

          hence e1 = e2 by A6;

        end;

        hence G2 is non-multi;

      end;

      hence G1 is non-multi implies G2 is non-multi;

       A7:

      now

        assume

         A8: G1 is non-Dmulti;

        now

          let e1,e2,v1,v2 be object;

          assume e1 DJoins (v1,v2,G2) & e2 DJoins (v1,v2,G2);

          then e1 DJoins (v1,v2,G1) & e2 DJoins (v1,v2,G1) by A1;

          hence e1 = e2 by A8;

        end;

        hence G2 is non-Dmulti;

      end;

      hence G1 is non-Dmulti implies G2 is non-Dmulti;

      thus G1 is simple implies G2 is simple by A4, A5;

      thus thesis by A4, A7;

    end;

    theorem :: GLIB_000:90

    

     Th90: G1 == G2 implies (G1 .order() ) = (G2 .order() ) & (G1 .size() ) = (G2 .size() ) & (G1 .edgesInto X) = (G2 .edgesInto X) & (G1 .edgesOutOf X) = (G2 .edgesOutOf X) & (G1 .edgesInOut X) = (G2 .edgesInOut X) & (G1 .edgesBetween X) = (G2 .edgesBetween X) & (G1 .edgesDBetween (X,Y)) = (G2 .edgesDBetween (X,Y))

    proof

      assume

       A1: G1 == G2;

      hence (G1 .order() ) = (G2 .order() );

      thus (G1 .size() ) = (G2 .size() ) by A1;

      

       A2: ( the_Edges_of G1) = ( the_Edges_of G2) by A1;

      

       A3: ( the_Target_of G1) = ( the_Target_of G2) by A1;

       A4:

      now

        let e be object;

        e in (G1 .edgesInto X) iff e in ( the_Edges_of G2) & (( the_Target_of G2) . e) in X by A2, A3, Def26;

        hence e in (G1 .edgesInto X) iff e in (G2 .edgesInto X) by Def26;

      end;

      hence

       A5: (G1 .edgesInto X) = (G2 .edgesInto X) by TARSKI: 2;

      

       A6: ( the_Source_of G1) = ( the_Source_of G2) by A1;

       A7:

      now

        let e be object;

        e in (G1 .edgesOutOf X) iff e in ( the_Edges_of G2) & (( the_Source_of G2) . e) in X by A2, A6, Def27;

        hence e in (G1 .edgesOutOf X) iff e in (G2 .edgesOutOf X) by Def27;

      end;

      hence

       A8: (G1 .edgesOutOf X) = (G2 .edgesOutOf X) by TARSKI: 2;

      thus (G1 .edgesInOut X) = (G2 .edgesInOut X) by A5, A7, TARSKI: 2;

      thus (G1 .edgesBetween X) = (G2 .edgesBetween X) by A4, A8, TARSKI: 2;

      now

        let e be object;

        e in (G1 .edgesDBetween (X,Y)) iff e DSJoins (X,Y,G1) by Def31;

        then e in (G1 .edgesDBetween (X,Y)) iff e DSJoins (X,Y,G2) by A1;

        hence e in (G2 .edgesDBetween (X,Y)) iff e in (G1 .edgesDBetween (X,Y)) by Def31;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLIB_000:91

    

     Th91: G1 == G2 & G3 is Subgraph of G1 implies G3 is Subgraph of G2

    proof

      assume that

       A1: G1 == G2 and

       A2: G3 is Subgraph of G1;

      ( the_Vertices_of G3) c= ( the_Vertices_of G1) by A2, Def32;

      hence ( the_Vertices_of G3) c= ( the_Vertices_of G2) by A1;

      ( the_Edges_of G3) c= ( the_Edges_of G1) by A2, Def32;

      hence ( the_Edges_of G3) c= ( the_Edges_of G2) by A1;

      let e be set;

      assume

       A3: e in ( the_Edges_of G3);

      

      hence (( the_Source_of G3) . e) = (( the_Source_of G1) . e) by A2, Def32

      .= (( the_Source_of G2) . e) by A1;

      

      thus (( the_Target_of G3) . e) = (( the_Target_of G1) . e) by A2, A3, Def32

      .= (( the_Target_of G2) . e) by A1;

    end;

    theorem :: GLIB_000:92

    G1 == G2 & G1 is Subgraph of G3 implies G2 is Subgraph of G3

    proof

      assume that

       A1: G1 == G2 and

       A2: G1 is Subgraph of G3;

      

       A3: ( the_Edges_of G1) = ( the_Edges_of G2) by A1;

      

       A4: ( the_Source_of G1) = ( the_Source_of G2) & ( the_Target_of G1) = ( the_Target_of G2) by A1;

      ( the_Vertices_of G1) = ( the_Vertices_of G2) by A1;

      hence ( the_Vertices_of G2) c= ( the_Vertices_of G3) & ( the_Edges_of G2) c= ( the_Edges_of G3) by A2, A3, Def32;

      let e be set;

      assume e in ( the_Edges_of G2);

      hence thesis by A2, A3, A4, Def32;

    end;

    theorem :: GLIB_000:93

    for G1,G2 be inducedSubgraph of G, V, E holds G1 == G2

    proof

      let G1,G2 be inducedSubgraph of G, V, E;

      now

        per cases ;

          suppose

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

          then

           A2: ( the_Edges_of G1) = E & ( the_Edges_of G2) = E by Def37;

          ( the_Vertices_of G1) = V & ( the_Vertices_of G2) = V by A1, Def37;

          hence thesis by A2, Th86;

        end;

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

          then G1 == G & G2 == G by Def37;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:94

    for G1 be _Graph, G2 be inducedSubgraph of G1, ( the_Vertices_of G1) holds G1 == G2

    proof

      let G1 be _Graph, G2 be inducedSubgraph of G1, ( the_Vertices_of G1);

      

       A1: ( the_Vertices_of G1) c= ( the_Vertices_of G1);

      then ( the_Edges_of G2) = (G1 .edgesBetween ( the_Vertices_of G1)) by Def37;

      then

       A2: ( the_Edges_of G2) = ( the_Edges_of G1) by Th34;

      then ( the_Source_of G2) = (( the_Source_of G1) | ( the_Edges_of G1)) by Th45;

      then ( the_Source_of G2) = (( the_Source_of G1) | ( dom ( the_Source_of G1)));

      then

       A3: ( the_Source_of G2) = ( the_Source_of G1);

      ( the_Target_of G2) = (( the_Target_of G1) | ( the_Edges_of G1)) by A2, Th45;

      then ( the_Target_of G2) = (( the_Target_of G1) | ( dom ( the_Target_of G1)));

      then

       A4: ( the_Target_of G2) = ( the_Target_of G1);

      ( the_Vertices_of G2) = ( the_Vertices_of G1) by A1, Def37;

      hence thesis by A2, A3, A4;

    end;

    theorem :: GLIB_000:95

    for G1,G2 be _Graph, V,E be set, G3 be inducedSubgraph of G1, V, E st G1 == G2 holds G3 is inducedSubgraph of G2, V, E

    proof

      let G1,G2 be _Graph, V,E be set, G3 be inducedSubgraph of G1, V, E;

      assume

       A1: G1 == G2;

      now

        per cases ;

          suppose

           A2: V is non empty Subset of ( the_Vertices_of G1) & E c= (G1 .edgesBetween V);

          then

           A3: ( the_Vertices_of G3) = V & ( the_Edges_of G3) = E by Def37;

          

           A4: G3 is Subgraph of G2 by A1, Th91;

          V is non empty Subset of ( the_Vertices_of G2) & E c= (G2 .edgesBetween V) by A1, A2, Th90;

          hence thesis by A3, A4, Def37;

        end;

          suppose

           A5: not (V is non empty Subset of ( the_Vertices_of G1) & E c= (G1 .edgesBetween V));

          then

           A6: not (V is non empty Subset of ( the_Vertices_of G2) & E c= (G2 .edgesBetween V)) by A1, Th90;

          G3 == G1 by A5, Def37;

          then

           A7: G3 == G2 by A1;

          then G3 is Subgraph of G2 by Th87;

          hence thesis by A6, A7, Def37;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:96

    

     Th96: for v1 be Vertex of G1, v2 be Vertex of G2 st v1 = v2 & G1 == G2 holds (v1 .edgesIn() ) = (v2 .edgesIn() ) & (v1 .edgesOut() ) = (v2 .edgesOut() ) & (v1 .edgesInOut() ) = (v2 .edgesInOut() ) & (v1 .adj e) = (v2 .adj e) & (v1 .inDegree() ) = (v2 .inDegree() ) & (v1 .outDegree() ) = (v2 .outDegree() ) & (v1 .degree() ) = (v2 .degree() ) & (v1 .inNeighbors() ) = (v2 .inNeighbors() ) & (v1 .outNeighbors() ) = (v2 .outNeighbors() ) & (v1 .allNeighbors() ) = (v2 .allNeighbors() )

    proof

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

      assume that

       A1: v1 = v2 and

       A2: G1 == G2;

      thus

       A3: (v1 .edgesIn() ) = (v2 .edgesIn() ) by A1, A2, Th90;

      thus

       A4: (v1 .edgesOut() ) = (v2 .edgesOut() ) by A1, A2, Th90;

      thus (v1 .edgesInOut() ) = (v2 .edgesInOut() ) by A1, A2, Th90;

      now

        per cases ;

          suppose

           A5: e in ( the_Edges_of G1) & (( the_Target_of G1) . e) = v1;

          then

           A6: e in ( the_Edges_of G2) & (( the_Target_of G2) . e) = v2 by A1, A2;

          

          thus (v1 .adj e) = (( the_Source_of G1) . e) by A5, Def41

          .= (( the_Source_of G2) . e) by A2

          .= (v2 .adj e) by A6, Def41;

        end;

          suppose

           A7: e in ( the_Edges_of G1) & (( the_Source_of G1) . e) = v1 & not (( the_Target_of G1) . e) = v1;

          then

           A8: not (( the_Target_of G2) . e) = v2 by A1, A2;

          

           A9: e in ( the_Edges_of G2) & (( the_Source_of G2) . e) = v2 by A1, A2, A7;

          

          thus (v1 .adj e) = (( the_Target_of G1) . e) by A7, Def41

          .= (( the_Target_of G2) . e) by A2

          .= (v2 .adj e) by A9, A8, Def41;

        end;

          suppose

           A10: not (e in ( the_Edges_of G1) & (( the_Target_of G1) . e) = v1) & not (e in ( the_Edges_of G1) & (( the_Source_of G1) . e) = v1 & not (( the_Target_of G1) . e) = v1);

          then

           A11: ( not (e in ( the_Edges_of G2) & (( the_Target_of G2) . e) = v2)) & not (e in ( the_Edges_of G2) & (( the_Source_of G2) . e) = v2 & not (( the_Target_of G2) . e) = v2) by A1, A2;

          

          thus (v1 .adj e) = v2 by A1, A10, Def41

          .= (v2 .adj e) by A11, Def41;

        end;

      end;

      hence (v1 .adj e) = (v2 .adj e);

      thus (v1 .inDegree() ) = (v2 .inDegree() ) by A1, A2, Th90;

      thus (v1 .outDegree() ) = (v2 .outDegree() ) by A1, A2, Th90;

      hence (v1 .degree() ) = (v2 .degree() ) by A1, A2, Th90;

      thus (v1 .inNeighbors() ) = (v2 .inNeighbors() ) by A2, A3;

      thus (v1 .outNeighbors() ) = (v2 .outNeighbors() ) by A2, A4;

      hence thesis by A2, A3;

    end;

    theorem :: GLIB_000:97

    for v1 be Vertex of G1, v2 be Vertex of G2 st v1 = v2 & G1 == G2 holds (v1 is isolated implies v2 is isolated) & (v1 is endvertex implies v2 is endvertex)

    proof

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

      assume

       A1: v1 = v2 & G1 == G2;

      hence v1 is isolated implies v2 is isolated by Th96;

      assume v1 is endvertex;

      then

      consider e be object such that

       A2: (v1 .edgesInOut() ) = {e} & not e Joins (v1,v1,G1);

      (v2 .edgesInOut() ) = {e} & not e Joins (v2,v2,G2) by A1, A2, Th96;

      hence thesis;

    end;

    theorem :: GLIB_000:98

    

     Th98: for G be _Graph, G1,G2 be Subgraph of G st G1 c< G2 holds (( the_Vertices_of G1) c< ( the_Vertices_of G2) or ( the_Edges_of G1) c< ( the_Edges_of G2))

    proof

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

      assume

       A1: G1 c< G2;

      then G1 c= G2;

      then

       A2: G1 is Subgraph of G2;

      then

       A3: ( the_Vertices_of G1) c= ( the_Vertices_of G2) by Def32;

      

       A4: ( the_Edges_of G1) c= ( the_Edges_of G2) by A2, Def32;

      

       A5: not G1 == G2 by A1;

      now

        per cases by A5, Th86;

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

          hence thesis by A3, XBOOLE_0:def 8;

        end;

          suppose ( the_Edges_of G1) <> ( the_Edges_of G2);

          hence thesis by A4, XBOOLE_0:def 8;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_000:99

    for G be _Graph, G1,G2 be Subgraph of G st G1 c< G2 holds (ex v be object st v in ( the_Vertices_of G2) & not v in ( the_Vertices_of G1)) or ex e be object st e in ( the_Edges_of G2) & not e in ( the_Edges_of G1)

    proof

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

      assume G1 c< G2;

      then ( the_Vertices_of G1) c< ( the_Vertices_of G2) or ( the_Edges_of G1) c< ( the_Edges_of G2) by Th98;

      hence thesis by XBOOLE_0: 6;

    end;