glunir00.miz



    begin

    reserve G for _Graph;

    definition

      let G;

      :: GLUNIR00:def1

      func VertexDomRel (G) -> Relation of ( the_Vertices_of G) equals ((( the_Source_of G) qua Relation ~ ) * ( the_Target_of G));

      coherence

      proof

        reconsider S = ( the_Source_of G) as Relation;

        set T = ( the_Target_of G);

        set E = ( the_Edges_of G), V = ( the_Vertices_of G);

        for x be object holds x in ((S ~ ) * T) implies x in [:V, V:]

        proof

          let x be object;

          assume

           A1: x in ((S ~ ) * T);

          then

          consider y,z be object such that

           A2: x = [y, z] by RELAT_1:def 1;

          consider a be object such that

           A3: [y, a] in (S ~ ) & [a, z] in T by A1, A2, RELAT_1:def 8;

           [a, y] in S by A3, RELAT_1:def 7;

          then

           A4: y in V by ZFMISC_1: 87;

          z in V by A3, ZFMISC_1: 87;

          hence x in [:V, V:] by A2, A4, ZFMISC_1:def 2;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: GLUNIR00:1

    

     Th1: for v,w be object holds [v, w] in ( VertexDomRel G) iff ex e be object st e DJoins (v,w,G)

    proof

      let v,w be object;

      reconsider S = ( the_Source_of G) as Relation of ( the_Edges_of G), ( the_Vertices_of G);

      hereby

        assume [v, w] in ( VertexDomRel G);

        then

        consider e be object such that

         A1: [v, e] in (S ~ ) & [e, w] in ( the_Target_of G) by RELAT_1:def 8;

        take e;

         [e, v] in S by A1, RELAT_1:def 7;

        then

         A2: e in ( dom ( the_Source_of G)) & (( the_Source_of G) . e) = v by FUNCT_1: 1;

        (( the_Target_of G) . e) = w by A1, FUNCT_1: 1;

        hence e DJoins (v,w,G) by A2, GLIB_000:def 14;

      end;

      given e be object such that

       A3: e DJoins (v,w,G);

      e in ( the_Edges_of G) by A3, GLIB_000:def 14;

      then

       A4: e in ( dom ( the_Source_of G)) & e in ( dom ( the_Target_of G)) by FUNCT_2:def 1;

      (( the_Source_of G) . e) = v & (( the_Target_of G) . e) = w by A3, GLIB_000:def 14;

      then [e, v] in ( the_Source_of G) & [e, w] in ( the_Target_of G) by A4, FUNCT_1: 1;

      then [v, e] in (S ~ ) & [e, w] in ( the_Target_of G) by RELAT_1:def 7;

      hence [v, w] in ( VertexDomRel G) by RELAT_1:def 8;

    end;

    theorem :: GLUNIR00:2

    

     Th2: for v,w be object holds [v, w] in (( VertexDomRel G) ~ ) iff ex e be object st e DJoins (w,v,G)

    proof

      let v,w be object;

      thus [v, w] in (( VertexDomRel G) ~ ) implies ex e be object st e DJoins (w,v,G)

      proof

        assume [v, w] in (( VertexDomRel G) ~ );

        then [w, v] in ( VertexDomRel G) by RELAT_1:def 7;

        then

        consider e be object such that

         A1: e DJoins (w,v,G) by Th1;

        take e;

        thus thesis by A1;

      end;

      thus (ex e be object st e DJoins (w,v,G)) implies [v, w] in (( VertexDomRel G) ~ )

      proof

        assume ex e be object st e DJoins (w,v,G);

        then [w, v] in ( VertexDomRel G) by Th1;

        hence thesis by RELAT_1:def 7;

      end;

    end;

    

     Lm1: G is loopless iff ( VertexDomRel G) misses ( id ( the_Vertices_of G))

    proof

      set V = ( the_Vertices_of G);

      hereby

        assume

         A1: G is loopless;

        (( VertexDomRel G) /\ ( id V)) = {}

        proof

          assume (( VertexDomRel G) /\ ( id V)) <> {} ;

          then

          consider z be object such that

           A2: z in (( VertexDomRel G) /\ ( id V)) by XBOOLE_0:def 1;

          consider x,y be object such that

           A3: z = [x, y] by A2, RELAT_1:def 1;

          

           A4: [x, y] in ( VertexDomRel G) & [x, y] in ( id V) by A2, A3, XBOOLE_0:def 4;

          then x = y by RELAT_1:def 10;

          then ex e be object st e DJoins (x,x,G) by A4, Th1;

          hence contradiction by A1, GLIB_009: 17;

        end;

        hence ( VertexDomRel G) misses ( id V) by XBOOLE_0:def 7;

      end;

      assume ( VertexDomRel G) misses ( id V);

      then

       A5: (( VertexDomRel G) /\ ( id V)) = {} by XBOOLE_0:def 7;

      assume G is non loopless;

      then

      consider v,e be object such that

       A6: e DJoins (v,v,G) by GLIB_009: 17;

      

       A7: [v, v] in ( VertexDomRel G) by A6, Th1;

      e Joins (v,v,G) by A6, GLIB_000: 16;

      then v in ( the_Vertices_of G) by GLIB_000: 13;

      then [v, v] in ( id V) by RELAT_1:def 10;

      hence contradiction by A5, A7, XBOOLE_0:def 4;

    end;

    theorem :: GLUNIR00:3

    

     Th3: G is loopless iff ( VertexDomRel G) is irreflexive

    proof

      hereby

        assume G is loopless;

        then ( VertexDomRel G) misses ( id ( the_Vertices_of G)) by Lm1;

        hence ( VertexDomRel G) is irreflexive by GLIBPRE0: 11;

      end;

      assume ( VertexDomRel G) is irreflexive;

      then ( VertexDomRel G) misses ( id ( the_Vertices_of G)) by GLIBPRE0: 11;

      hence G is loopless by Lm1;

    end;

    registration

      let G be loopless _Graph;

      cluster ( VertexDomRel G) -> irreflexive;

      coherence by Th3;

    end

    registration

      let G be non loopless _Graph;

      cluster ( VertexDomRel G) -> non irreflexive;

      coherence by Th3;

    end

    registration

      let G be non-multi _Graph;

      cluster ( VertexDomRel G) -> antisymmetric;

      coherence

      proof

        set F = ( field ( VertexDomRel G));

        now

          let x,y be object;

          assume x in F & y in F;

          assume

           A1: [x, y] in ( VertexDomRel G) & [y, x] in ( VertexDomRel G);

          then

          consider e1 be object such that

           A2: e1 DJoins (x,y,G) by Th1;

          consider e2 be object such that

           A3: e2 DJoins (y,x,G) by A1, Th1;

          e1 Joins (x,y,G) & e2 Joins (x,y,G) by A2, A3, GLIB_000: 16;

          then e1 = e2 by GLIB_000:def 20;

          hence x = y by A2, A3, GLIB_009: 6;

        end;

        hence ( VertexDomRel G) is antisymmetric by RELAT_2:def 4, RELAT_2:def 12;

      end;

    end

    registration

      let G be simple _Graph;

      cluster ( VertexDomRel G) -> asymmetric;

      coherence

      proof

        set F = ( field ( VertexDomRel G));

        now

          let x,y be object;

          assume x in F & y in F;

          assume

           A1: [x, y] in ( VertexDomRel G) & [y, x] in ( VertexDomRel G);

          then

          consider e1 be object such that

           A2: e1 DJoins (x,y,G) by Th1;

          consider e2 be object such that

           A3: e2 DJoins (y,x,G) by A1, Th1;

          e1 Joins (x,y,G) & e2 Joins (x,y,G) by A2, A3, GLIB_000: 16;

          then e1 = e2 by GLIB_000:def 20;

          then x = y by A2, A3, GLIB_009: 6;

          hence contradiction by A2, GLIB_009: 17;

        end;

        hence ( VertexDomRel G) is asymmetric by RELAT_2:def 5, RELAT_2:def 13;

      end;

    end

    theorem :: GLUNIR00:4

    

     Th4: for G be _Graph st ex e1,e2,x,y be object st e1 DJoins (x,y,G) & e2 DJoins (y,x,G) holds ( VertexDomRel G) is non asymmetric

    proof

      let G be _Graph;

      given e1,e2,x,y be object such that

       A1: e1 DJoins (x,y,G) & e2 DJoins (y,x,G);

      set R = ( VertexDomRel G);

      ex x,y be object st x in ( field R) & y in ( field R) & [x, y] in R & [y, x] in R

      proof

        take x, y;

         [x, y] in R & [y, x] in R by A1, Th1;

        hence thesis by RELAT_1: 15;

      end;

      hence ( VertexDomRel G) is non asymmetric by RELAT_2:def 5, RELAT_2:def 13;

    end;

    registration

      let G be non non-multi non-Dmulti _Graph;

      cluster ( VertexDomRel G) -> non asymmetric;

      coherence

      proof

        ex e1,e2,x,y be object st e1 DJoins (x,y,G) & e2 DJoins (y,x,G)

        proof

          consider e1,e2,x,y be object such that

           A1: e1 Joins (x,y,G) & e2 Joins (x,y,G) & e1 <> e2 by GLIB_000:def 20;

          per cases by A1, GLIB_000: 16;

            suppose

             A2: e1 DJoins (x,y,G);

            then not e2 DJoins (x,y,G) by A1, GLIB_000:def 21;

            then

             A3: e2 DJoins (y,x,G) by A1, GLIB_000: 16;

            take e1, e2, x, y;

            thus thesis by A2, A3;

          end;

            suppose

             A4: e1 DJoins (y,x,G);

            then not e2 DJoins (y,x,G) by A1, GLIB_000:def 21;

            then

             A5: e2 DJoins (x,y,G) by A1, GLIB_000: 16;

            take e1, e2, y, x;

            thus thesis by A4, A5;

          end;

        end;

        hence thesis by Th4;

      end;

    end

    theorem :: GLUNIR00:5

    

     Th5: for G be loopless _Graph st ( field ( VertexDomRel G)) = ( the_Vertices_of G) holds for C be Component of G holds C is non _trivial

    proof

      let G be loopless _Graph;

      assume

       A1: ( field ( VertexDomRel G)) = ( the_Vertices_of G);

      let C be Component of G;

      assume C is _trivial;

      then

      consider v be Vertex of C such that

       A2: ( the_Vertices_of C) = {v} by GLIB_000: 22;

      

       A3: v in ( the_Vertices_of G) by A2, ZFMISC_1: 31;

      reconsider v0 = v as Vertex of G by A2, ZFMISC_1: 31;

      ( the_Vertices_of G) = (( dom ( VertexDomRel G)) \/ ( rng ( VertexDomRel G))) by A1, RELAT_1:def 6;

      per cases by A3, XBOOLE_0:def 3;

        suppose v in ( dom ( VertexDomRel G));

        then

        consider w be object such that

         A4: [v, w] in ( VertexDomRel G) by XTUPLE_0:def 12;

        consider e be object such that

         A5: e DJoins (v,w,G) by A4, Th1;

        e Joins (v,w,G) by A5, GLIB_000: 16;

        then w in (G .reachableFrom v0) by GLIB_002: 9, GLIB_002: 10;

        then w in ( the_Vertices_of C) by GLIB_002: 33;

        then w = v by A2, TARSKI:def 1;

        hence contradiction by A5, GLIB_009: 17;

      end;

        suppose v in ( rng ( VertexDomRel G));

        then

        consider w be object such that

         A6: [w, v] in ( VertexDomRel G) by XTUPLE_0:def 13;

        consider e be object such that

         A7: e DJoins (w,v,G) by A6, Th1;

        e Joins (v,w,G) by A7, GLIB_000: 16;

        then w in (G .reachableFrom v0) by GLIB_002: 9, GLIB_002: 10;

        then w in ( the_Vertices_of C) by GLIB_002: 33;

        then w = v by A2, TARSKI:def 1;

        hence contradiction by A7, GLIB_009: 17;

      end;

    end;

    theorem :: GLUNIR00:6

    

     Th6: for G be _Graph st for C be Component of G holds C is non _trivial holds ( field ( VertexDomRel G)) = ( the_Vertices_of G)

    proof

      let G be _Graph;

      assume

       A1: for C be Component of G holds C is non _trivial;

      

       A2: ( field ( VertexDomRel G)) c= (( the_Vertices_of G) \/ ( the_Vertices_of G)) by RELSET_1: 8;

      now

        let x be object;

        assume x in ( the_Vertices_of G);

        then

        reconsider v = x as Vertex of G;

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

        reconsider H0 = H as non _trivial _Graph by A1;

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

        then

        reconsider v0 = v as Vertex of H0 by GLIB_002: 9;

        (( the_Vertices_of H0) \ {v0}) is non empty by GLIB_000: 20;

        then

        consider w be object such that

         A3: w in (( the_Vertices_of H) \ {v0}) by XBOOLE_0:def 1;

        reconsider w as Vertex of H by A3, XBOOLE_0:def 5;

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

        then

        consider W be Walk of G such that

         A4: W is_Walk_from (v,w) by GLIB_002:def 5;

        

         A5: (W .first() ) = v & (W .last() ) = w by A4, GLIB_001:def 23;

         not w in {v} by A3, XBOOLE_0:def 5;

        then v <> w by TARSKI:def 1;

        then 3 <= ( len W) by A5, GLIB_001: 125, GLIB_001: 127;

        then 1 < ( len W) by XXREAL_0: 2;

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

        then (W . 2) Joins (v,(W . 3),G) by A5, GLIB_001:def 6;

        per cases by GLIB_000: 16;

          suppose (W . 2) DJoins (v,(W . 3),G);

          then [v, (W . 3)] in ( VertexDomRel G) by Th1;

          hence x in ( field ( VertexDomRel G)) by RELAT_1: 15;

        end;

          suppose (W . 2) DJoins ((W . 3),v,G);

          then [(W . 3), v] in ( VertexDomRel G) by Th1;

          hence x in ( field ( VertexDomRel G)) by RELAT_1: 15;

        end;

      end;

      then ( the_Vertices_of G) c= ( field ( VertexDomRel G)) by TARSKI:def 3;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: GLUNIR00:7

    for G be non _trivial connected _Graph holds ( field ( VertexDomRel G)) = ( the_Vertices_of G)

    proof

      let G be non _trivial connected _Graph;

      now

        let C be Component of G;

        set v = the Vertex of C;

        ( the_Vertices_of C) c= ( the_Vertices_of G);

        then v in ( the_Vertices_of G) & G is Component of G by GLIB_002: 30, TARSKI:def 3;

        then C == G by GLIB_002: 34;

        hence C is non _trivial by GLIB_000: 89;

      end;

      hence thesis by Th6;

    end;

    registration

      let G be complete _Graph;

      cluster ( VertexDomRel G) -> connected;

      coherence

      proof

        set F = ( field ( VertexDomRel G));

        now

          let x,y be object;

          assume

           A1: x in F & y in F & x <> y;

          F c= (( the_Vertices_of G) \/ ( the_Vertices_of G)) by RELSET_1: 8;

          then

          reconsider v = x, w = y as Vertex of G by A1;

          consider e be object such that

           A2: e Joins (v,w,G) by A1, CHORD:def 3, CHORD:def 6;

          per cases by A2, GLIB_000: 16;

            suppose e DJoins (v,w,G);

            hence [x, y] in ( VertexDomRel G) or [y, x] in ( VertexDomRel G) by Th1;

          end;

            suppose e DJoins (w,v,G);

            hence [x, y] in ( VertexDomRel G) or [y, x] in ( VertexDomRel G) by Th1;

          end;

        end;

        hence ( VertexDomRel G) is connected by RELAT_2:def 6, RELAT_2:def 14;

      end;

    end

    theorem :: GLUNIR00:8

    

     Th8: G is edgeless iff ( VertexDomRel G) is empty

    proof

      thus G is edgeless implies ( VertexDomRel G) is empty;

      thus ( VertexDomRel G) is empty implies G is edgeless

      proof

        assume

         A1: ( VertexDomRel G) is empty;

        thus G is edgeless

        proof

          assume not G is edgeless;

          then

          consider e be object such that

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

          e DJoins ((( the_Source_of G) . e),(( the_Target_of G) . e),G) by A2, GLIB_000:def 14;

          hence contradiction by A1, Th1;

        end;

      end;

    end;

    registration

      let G be edgeless _Graph;

      cluster ( VertexDomRel G) -> empty;

      coherence ;

    end

    registration

      let G be non edgeless _Graph;

      cluster ( VertexDomRel G) -> non empty;

      coherence by Th8;

    end

    

     Lm2: G is loopfull iff ( id ( the_Vertices_of G)) c= ( VertexDomRel G)

    proof

      hereby

        assume

         A1: G is loopfull;

        now

          let x,y be object;

          assume [x, y] in ( id ( the_Vertices_of G));

          then

           A2: x in ( the_Vertices_of G) & x = y by RELAT_1:def 10;

          then ex e be object st e DJoins (x,x,G) by A1, GLIB_012: 1;

          hence [x, y] in ( VertexDomRel G) by A2, Th1;

        end;

        hence ( id ( the_Vertices_of G)) c= ( VertexDomRel G) by RELAT_1:def 3;

      end;

      assume

       A3: ( id ( the_Vertices_of G)) c= ( VertexDomRel G);

      now

        let v be Vertex of G;

         [v, v] in ( id ( the_Vertices_of G)) by RELAT_1:def 10;

        hence ex e be object st e DJoins (v,v,G) by A3, Th1;

      end;

      hence thesis by GLIB_012: 1;

    end;

    theorem :: GLUNIR00:9

    

     Th9: G is loopfull iff ( VertexDomRel G) is total reflexive

    proof

      hereby

        assume G is loopfull;

        then ( id ( the_Vertices_of G)) c= ( VertexDomRel G) by Lm2;

        hence ( VertexDomRel G) is total reflexive by ROUGHS_1: 3;

      end;

      assume ( VertexDomRel G) is total reflexive;

      then ( id ( the_Vertices_of G)) c= ( VertexDomRel G) by ROUGHS_1: 3;

      hence G is loopfull by Lm2;

    end;

    registration

      let G be loopfull _Graph;

      cluster ( VertexDomRel G) -> reflexive total;

      coherence by Th9;

    end

    registration

      let G be vertex-finite _Graph;

      cluster ( VertexDomRel G) -> finite;

      coherence ;

    end

    theorem :: GLUNIR00:10

    

     Th10: ( card ( VertexDomRel G)) = ( card ( Class ( DEdgeAdjEqRel G)))

    proof

      set R = ( VertexDomRel G);

      defpred P[ object, object] means ex e be object st e DJoins (($1 `1 ),($1 `2 ),G) & $2 = ( Class (( DEdgeAdjEqRel G),e));

      

       A1: for x,y1,y2 be object st x in R & P[x, y1] & P[x, y2] holds y1 = y2

      proof

        let x,y1,y2 be object;

        assume

         A2: x in R & P[x, y1] & P[x, y2];

        then

        consider e1 be object such that

         A3: e1 DJoins ((x `1 ),(x `2 ),G) & y1 = ( Class (( DEdgeAdjEqRel G),e1));

        consider e2 be object such that

         A4: e2 DJoins ((x `1 ),(x `2 ),G) & y2 = ( Class (( DEdgeAdjEqRel G),e2)) by A2;

         [e1, e2] in ( DEdgeAdjEqRel G) by A3, A4, GLIB_009:def 4;

        then

         A5: e2 in ( Class (( DEdgeAdjEqRel G),e1)) by EQREL_1: 18;

        e1 in ( the_Edges_of G) by A3, GLIB_000:def 14;

        hence thesis by A3, A4, A5, EQREL_1: 23;

      end;

      

       A6: for x be object st x in R holds ex y be object st P[x, y]

      proof

        let x be object;

        assume

         A7: x in R;

        then

        consider v,w be object such that

         A8: x = [v, w] by RELAT_1:def 1;

        consider e be object such that

         A9: e DJoins (v,w,G) by A7, A8, Th1;

        take ( Class (( DEdgeAdjEqRel G),e)), e;

        thus thesis by A8, A9;

      end;

      consider f be Function such that

       A10: ( dom f) = R & for x be object st x in R holds P[x, (f . x)] from FUNCT_1:sch 2( A1, A6);

      now

        let y be object;

        hereby

          assume y in ( rng f);

          then

          consider x be object such that

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

          consider e be object such that

           A12: e DJoins ((x `1 ),(x `2 ),G) & y = ( Class (( DEdgeAdjEqRel G),e)) by A10, A11;

          e in ( the_Edges_of G) by A12, GLIB_000:def 14;

          hence y in ( Class ( DEdgeAdjEqRel G)) by A12, EQREL_1:def 3;

        end;

        assume y in ( Class ( DEdgeAdjEqRel G));

        then

        consider e be object such that

         A13: e in ( the_Edges_of G) & y = ( Class (( DEdgeAdjEqRel G),e)) by EQREL_1:def 3;

        set x = [(( the_Source_of G) . e), (( the_Target_of G) . e)];

        

         A14: e DJoins ((x `1 ),(x `2 ),G) by A13, GLIB_000:def 14;

        then P[x, (f . x)] by A10, Th1;

        then (f . x) = y by A1, A13, A14, Th1;

        hence y in ( rng f) by A10, A14, Th1, FUNCT_1: 3;

      end;

      then

       A16: ( rng f) = ( Class ( DEdgeAdjEqRel G)) by TARSKI: 2;

      for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

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

        then

        consider e1 be object such that

         A18: e1 DJoins ((x1 `1 ),(x1 `2 ),G) & (f . x1) = ( Class (( DEdgeAdjEqRel G),e1)) by A10;

        consider e2 be object such that

         A19: e2 DJoins ((x2 `1 ),(x2 `2 ),G) & (f . x2) = ( Class (( DEdgeAdjEqRel G),e2)) by A10, A17;

        e1 in ( the_Edges_of G) by A18, GLIB_000:def 14;

        then e2 in ( Class (( DEdgeAdjEqRel G),e1)) by A17, A18, A19, EQREL_1: 23;

        then [e1, e2] in ( DEdgeAdjEqRel G) by EQREL_1: 18;

        then

        consider v,w be object such that

         A20: e1 DJoins (v,w,G) & e2 DJoins (v,w,G) by GLIB_009:def 4;

        v = (x1 `1 ) & w = (x1 `2 ) & v = (x2 `1 ) & w = (x2 `2 ) by A18, A19, A20, GLIB_009: 6;

        then

         A21: [(x1 `1 ), (x1 `2 )] = [(x2 `1 ), (x2 `2 )];

        (ex a,b be object st x1 = [a, b]) & (ex a,b be object st x2 = [a, b]) by A10, A17, RELAT_1:def 1;

        hence thesis by A21;

      end;

      hence thesis by A10, A16, FUNCT_1:def 4, CARD_1: 70;

    end;

    theorem :: GLUNIR00:11

    ( card ( VertexDomRel G)) c= (G .size() )

    proof

      set E = the RepDEdgeSelection of G;

      ( card E) c= ( card ( the_Edges_of G)) by CARD_1: 11;

      then ( card E) c= (G .size() ) by GLIB_000:def 25;

      then ( card ( Class ( DEdgeAdjEqRel G))) c= (G .size() ) by GLIBPRE0: 71;

      hence thesis by Th10;

    end;

    theorem :: GLUNIR00:12

    

     Th12: for G be non-Dmulti _Graph holds (G .size() ) = ( card ( VertexDomRel G))

    proof

      let G be non-Dmulti _Graph;

      ( DEdgeAdjEqRel G) = ( id ( the_Edges_of G)) by GLIB_009: 71;

      then ( Class ( DEdgeAdjEqRel G)) = ( SmallestPartition ( the_Edges_of G)) by EQREL_1:def 5;

      then ( card ( Class ( DEdgeAdjEqRel G))) = ( card ( the_Edges_of G)) by TOPGEN_2: 12;

      then ( card ( VertexDomRel G)) = ( card ( the_Edges_of G)) by Th10;

      hence thesis by GLIB_000:def 25;

    end;

    theorem :: GLUNIR00:13

    for v be Vertex of G holds ( Im (( VertexDomRel G),v)) = (v .outNeighbors() )

    proof

      let v be Vertex of G;

      now

        let x be object;

        hereby

          assume x in (( VertexDomRel G) .: {v});

          then

          consider v0 be object such that

           A1: [v0, x] in ( VertexDomRel G) & v0 in {v} by RELAT_1:def 13;

           [v, x] in ( VertexDomRel G) by A1, TARSKI:def 1;

          then x is set & ex e be object st e DJoins (v,x,G) by Th1, TARSKI: 1;

          hence x in (v .outNeighbors() ) by GLIB_000: 70;

        end;

        assume x in (v .outNeighbors() );

        then ex e be object st e DJoins (v,x,G) by GLIB_000: 70;

        then [v, x] in ( VertexDomRel G) & v in {v} by Th1, TARSKI:def 1;

        hence x in (( VertexDomRel G) .: {v}) by RELAT_1:def 13;

      end;

      then (( VertexDomRel G) .: {v}) = (v .outNeighbors() ) by TARSKI: 2;

      hence thesis by RELAT_1:def 16;

    end;

    theorem :: GLUNIR00:14

    for v be Vertex of G holds ( Coim (( VertexDomRel G),v)) = (v .inNeighbors() )

    proof

      let v be Vertex of G;

      now

        let x be object;

        hereby

          assume x in (( VertexDomRel G) " {v});

          then

          consider v0 be object such that

           A1: [x, v0] in ( VertexDomRel G) & v0 in {v} by RELAT_1:def 14;

           [x, v] in ( VertexDomRel G) by A1, TARSKI:def 1;

          then x is set & ex e be object st e DJoins (x,v,G) by Th1, TARSKI: 1;

          hence x in (v .inNeighbors() ) by GLIB_000: 69;

        end;

        assume x in (v .inNeighbors() );

        then ex e be object st e DJoins (x,v,G) by GLIB_000: 69;

        then [x, v] in ( VertexDomRel G) & v in {v} by Th1, TARSKI:def 1;

        hence x in (( VertexDomRel G) " {v}) by RELAT_1:def 14;

      end;

      then (( VertexDomRel G) " {v}) = (v .inNeighbors() ) by TARSKI: 2;

      hence thesis by RELAT_1:def 17;

    end;

    theorem :: GLUNIR00:15

    

     Th15: for H be Subgraph of G holds ( VertexDomRel H) c= ( VertexDomRel G)

    proof

      let H be Subgraph of G;

      now

        let v,w be object;

        assume [v, w] in ( VertexDomRel H);

        then

        consider e be object such that

         A1: e DJoins (v,w,H) by Th1;

        e is set & v is set & w is set by TARSKI: 1;

        then e DJoins (v,w,G) by A1, GLIB_000: 72;

        hence [v, w] in ( VertexDomRel G) by Th1;

      end;

      hence thesis by RELAT_1:def 3;

    end;

    theorem :: GLUNIR00:16

    

     Th16: for H be removeDParallelEdges of G holds ( VertexDomRel H) = ( VertexDomRel G)

    proof

      let H be removeDParallelEdges of G;

      consider E be RepDEdgeSelection of G such that

       A1: H is inducedSubgraph of G, ( the_Vertices_of G), E by GLIB_009:def 8;

      

       A2: ( VertexDomRel H) c= ( VertexDomRel G) by Th15;

      now

        let v,w be object;

        assume [v, w] in ( VertexDomRel G);

        then

        consider e0 be object such that

         A3: e0 DJoins (v,w,G) by Th1;

        ( the_Edges_of G) = (G .edgesBetween ( the_Vertices_of G)) & ( the_Vertices_of G) c= ( the_Vertices_of G) by GLIB_000: 34;

        then

         A4: ( the_Edges_of H) = E by A1, GLIB_000:def 37;

        consider e be object such that

         A5: e DJoins (v,w,G) & e in E and for e9 be object st e9 DJoins (v,w,G) & e9 in E holds e9 = e by A3, GLIB_009:def 6;

        v is set & w is set by TARSKI: 1;

        then e DJoins (v,w,H) by A4, A5, GLIB_000: 73;

        hence [v, w] in ( VertexDomRel H) by Th1;

      end;

      then ( VertexDomRel G) c= ( VertexDomRel H) by RELAT_1:def 3;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: GLUNIR00:17

    

     Th17: for H be removeLoops of G holds ( VertexDomRel H) = (( VertexDomRel G) \ ( id ( the_Vertices_of G)))

    proof

      let H be removeLoops of G;

      now

        let v,w be object;

        hereby

          assume

           A1: [v, w] in ( VertexDomRel H);

          then

          consider e be object such that

           A2: e DJoins (v,w,H) by Th1;

          v <> w by A2, GLIB_009: 17;

          then

           A3: not [v, w] in ( id ( the_Vertices_of G)) by RELAT_1:def 10;

           [v, w] in ( VertexDomRel G) by A1, Th15, TARSKI:def 3;

          hence [v, w] in (( VertexDomRel G) \ ( id ( the_Vertices_of G))) by A3, XBOOLE_0:def 5;

        end;

        assume [v, w] in (( VertexDomRel G) \ ( id ( the_Vertices_of G)));

        then

         A4: [v, w] in ( VertexDomRel G) & not [v, w] in ( id ( the_Vertices_of G)) by XBOOLE_0:def 5;

        then

        consider e be object such that

         A5: e DJoins (v,w,G) by Th1;

        

         A6: e Joins (v,w,G) by A5, GLIB_000: 16;

        then v in ( the_Vertices_of G) by GLIB_000: 13;

        then v <> w by A4, RELAT_1:def 10;

        then

         A7: not e in (G .loops() ) by A6, GLIB_009: 46;

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

        then e in (( the_Edges_of G) \ (G .loops() )) by A7, XBOOLE_0:def 5;

        then

         A8: e in ( the_Edges_of H) by GLIB_000: 53;

        v is set & w is set & e is set by TARSKI: 1;

        then e DJoins (v,w,H) by A5, A8, GLIB_000: 73;

        hence [v, w] in ( VertexDomRel H) by Th1;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    theorem :: GLUNIR00:18

    for H be DSimpleGraph of G holds ( VertexDomRel H) = (( VertexDomRel G) \ ( id ( the_Vertices_of G)))

    proof

      let H be DSimpleGraph of G;

      consider G9 be removeDParallelEdges of G such that

       A1: H is removeLoops of G9 by GLIB_009: 120;

      

       A2: ( the_Vertices_of G9) = ( the_Vertices_of G) by GLIB_000:def 33;

      

      thus ( VertexDomRel H) = (( VertexDomRel G9) \ ( id ( the_Vertices_of G9))) by A1, Th17

      .= (( VertexDomRel G) \ ( id ( the_Vertices_of G))) by A2, Th16;

    end;

    theorem :: GLUNIR00:19

    

     Th19: for G1,G2 be _Graph st G1 == G2 holds ( VertexDomRel G1) = ( VertexDomRel G2)

    proof

      let G1,G2 be _Graph such that

       A1: G1 == G2;

      now

        let v,w be object;

        hereby

          assume [v, w] in ( VertexDomRel G1);

          then

          consider e be object such that

           A2: e DJoins (v,w,G1) by Th1;

          e DJoins (v,w,G2) by A1, A2, GLIB_000: 88;

          hence [v, w] in ( VertexDomRel G2) by Th1;

        end;

        assume [v, w] in ( VertexDomRel G2);

        then

        consider e be object such that

         A3: e DJoins (v,w,G2) by Th1;

        e DJoins (v,w,G1) by A1, A3, GLIB_000: 88;

        hence [v, w] in ( VertexDomRel G1) by Th1;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    theorem :: GLUNIR00:20

    

     Th20: for H be reverseEdgeDirections of G holds ( VertexDomRel H) = (( VertexDomRel G) ~ )

    proof

      let H be reverseEdgeDirections of G;

      now

        let w,v be object;

        hereby

          assume [w, v] in (( VertexDomRel G) ~ );

          then [v, w] in ( VertexDomRel G) by RELAT_1:def 7;

          then

          consider e be object such that

           A1: e DJoins (v,w,G) by Th1;

          e in ( the_Edges_of G) by A1, GLIB_000:def 14;

          then e DJoins (w,v,H) by A1, GLIB_007: 7;

          hence [w, v] in ( VertexDomRel H) by Th1;

        end;

        assume [w, v] in ( VertexDomRel H);

        then

        consider e be object such that

         A2: e DJoins (w,v,H) by Th1;

        e in ( the_Edges_of H) by A2, GLIB_000:def 14;

        then e in ( the_Edges_of G) by GLIB_007: 4;

        then e DJoins (v,w,G) by A2, GLIB_007: 7;

        then [v, w] in ( VertexDomRel G) by Th1;

        hence [w, v] in (( VertexDomRel G) ~ ) by RELAT_1:def 7;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    theorem :: GLUNIR00:21

    

     Th21: for V be non empty Subset of ( the_Vertices_of G) holds for H be inducedSubgraph of G, V holds ( VertexDomRel H) = (( VertexDomRel G) /\ [:V, V:])

    proof

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

      let H be inducedSubgraph of G, V;

      

       A1: ( the_Vertices_of H) = V & ( the_Edges_of H) = (G .edgesBetween V) by GLIB_000:def 37;

      now

        let v,w be object;

        hereby

          assume

           A2: [v, w] in ( VertexDomRel H);

          then

          consider e be object such that

           A3: e DJoins (v,w,H) by Th1;

          e Joins (v,w,H) by A3, GLIB_000: 16;

          then v in V & w in V by A1, GLIB_000: 13;

          then

           A4: [v, w] in [:V, V:] by ZFMISC_1: 87;

           [v, w] in ( VertexDomRel G) by A2, Th15, TARSKI:def 3;

          hence [v, w] in (( VertexDomRel G) /\ [:V, V:]) by A4, XBOOLE_0:def 4;

        end;

        assume [v, w] in (( VertexDomRel G) /\ [:V, V:]);

        then

         A5: [v, w] in ( VertexDomRel G) & [v, w] in [:V, V:] by XBOOLE_0:def 4;

        then

        consider e be object such that

         A6: e DJoins (v,w,G) by Th1;

        

         A7: e in ( the_Edges_of G) & (( the_Source_of G) . e) = v & (( the_Target_of G) . e) = w by A6, GLIB_000:def 14;

        v in V & w in V by A5, ZFMISC_1: 87;

        then

         A8: e in ( the_Edges_of H) by A1, A7, GLIB_000: 31;

        e is set & v is set & w is set by TARSKI: 1;

        then e DJoins (v,w,H) by A6, A8, GLIB_000: 73;

        hence [v, w] in ( VertexDomRel H) by Th1;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    theorem :: GLUNIR00:22

    

     Th22: for V be set, H be removeVertices of G, V st V c< ( the_Vertices_of G) holds ( VertexDomRel H) = (( VertexDomRel G) \ ( [:V, ( the_Vertices_of G):] \/ [:( the_Vertices_of G), V:]))

    proof

      let V be set, H be removeVertices of G, V;

      assume V c< ( the_Vertices_of G);

      then

       A1: ( the_Vertices_of H) = (( the_Vertices_of G) \ V) & ( the_Edges_of H) = (G .edgesBetween (( the_Vertices_of G) \ V)) by GLIB_000: 49;

      now

        let v,w be object;

        hereby

          assume

           A2: [v, w] in ( VertexDomRel H);

          then

           A3: [v, w] in ( VertexDomRel G) by Th15, TARSKI:def 3;

          consider e be object such that

           A4: e DJoins (v,w,H) by A2, Th1;

          e Joins (v,w,H) by A4, GLIB_000: 16;

          then v in ( the_Vertices_of H) & w in ( the_Vertices_of H) by GLIB_000: 13;

          then not v in V & not w in V by A1, XBOOLE_0:def 5;

          then not [v, w] in [:V, ( the_Vertices_of G):] & not [v, w] in [:( the_Vertices_of G), V:] by ZFMISC_1: 87;

          then not [v, w] in ( [:V, ( the_Vertices_of G):] \/ [:( the_Vertices_of G), V:]) by XBOOLE_0:def 3;

          hence [v, w] in (( VertexDomRel G) \ ( [:V, ( the_Vertices_of G):] \/ [:( the_Vertices_of G), V:])) by A3, XBOOLE_0:def 5;

        end;

        assume [v, w] in (( VertexDomRel G) \ ( [:V, ( the_Vertices_of G):] \/ [:( the_Vertices_of G), V:]));

        then

         A5: [v, w] in ( VertexDomRel G) & not [v, w] in ( [:V, ( the_Vertices_of G):] \/ [:( the_Vertices_of G), V:]) by XBOOLE_0:def 5;

        then

         A6: not [v, w] in [:V, ( the_Vertices_of G):] & not [v, w] in [:( the_Vertices_of G), V:] by XBOOLE_0:def 3;

        consider e be object such that

         A7: e DJoins (v,w,G) by A5, Th1;

        

         A8: e Joins (v,w,G) by A7, GLIB_000: 16;

        then

         A9: v in ( the_Vertices_of G) & w in ( the_Vertices_of G) by GLIB_000: 13;

        then not v in V & not w in V by A6, ZFMISC_1: 87;

        then v in (( the_Vertices_of G) \ V) & w in (( the_Vertices_of G) \ V) by A9, XBOOLE_0:def 5;

        then

         A10: e in ( the_Edges_of H) by A1, A8, GLIB_000: 32;

        e is set & v is set & w is set by TARSKI: 1;

        then e DJoins (v,w,H) by A7, A10, GLIB_000: 73;

        hence [v, w] in ( VertexDomRel H) by Th1;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    theorem :: GLUNIR00:23

    

     Th23: for G be non _trivial _Graph, v be Vertex of G holds for H be removeVertex of G, v holds ( VertexDomRel H) = (( VertexDomRel G) \ ( [: {v}, ( the_Vertices_of G):] \/ [:( the_Vertices_of G), {v}:]))

    proof

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

      let H be removeVertex of G, v;

      (( the_Vertices_of G) \ {v}) is non empty by GLIB_000: 20;

      then not ( the_Vertices_of G) c= {v} by XBOOLE_1: 37;

      hence thesis by Th22, XBOOLE_0:def 8;

    end;

    theorem :: GLUNIR00:24

    

     Th24: for G be non _trivial _Graph, v be Vertex of G holds for H be removeVertex of G, v st v is isolated holds ( VertexDomRel H) = ( VertexDomRel G)

    proof

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

      let H be removeVertex of G, v;

      assume

       A1: v is isolated;

      set V1 = [: {v}, ( the_Vertices_of G):];

      set V2 = [:( the_Vertices_of G), {v}:];

      ((V1 \/ V2) /\ ( VertexDomRel G)) = {}

      proof

        assume ((V1 \/ V2) /\ ( VertexDomRel G)) <> {} ;

        then

        consider z be object such that

         A2: z in ((V1 \/ V2) /\ ( VertexDomRel G)) by XBOOLE_0:def 1;

        consider u,w be object such that

         A3: z = [u, w] by A2, RELAT_1:def 1;

        

         A4: [u, w] in (V1 \/ V2) & [u, w] in ( VertexDomRel G) by A2, A3, XBOOLE_0:def 4;

        then

        consider e be object such that

         A5: e DJoins (u,w,G) by Th1;

        per cases by A4, XBOOLE_0:def 3;

          suppose [u, w] in V1;

          then u in {v} by ZFMISC_1: 87;

          then u = v by TARSKI:def 1;

          hence contradiction by A1, A5, GLIBPRE0: 22;

        end;

          suppose [u, w] in V2;

          then w in {v} by ZFMISC_1: 87;

          then w = v by TARSKI:def 1;

          hence contradiction by A1, A5, GLIBPRE0: 22;

        end;

      end;

      then ( VertexDomRel G) = (( VertexDomRel G) \ (V1 \/ V2)) by XBOOLE_1: 83, XBOOLE_0:def 7;

      hence thesis by Th23;

    end;

    theorem :: GLUNIR00:25

    

     Th25: for V be set, H be addVertices of G, V holds ( VertexDomRel H) = ( VertexDomRel G)

    proof

      let V be set, H be addVertices of G, V;

      G is Subgraph of H by GLIB_006: 57;

      then

       A1: ( VertexDomRel G) c= ( VertexDomRel H) by Th15;

      now

        let v,w be object;

        assume [v, w] in ( VertexDomRel H);

        then

        consider e be object such that

         A2: e DJoins (v,w,H) by Th1;

        e DJoins (v,w,G) by A2, GLIB_006: 85;

        hence [v, w] in ( VertexDomRel G) by Th1;

      end;

      then ( VertexDomRel H) c= ( VertexDomRel G) by RELAT_1:def 3;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: GLUNIR00:26

    

     Th26: for v,e,w be object, H be addEdge of G, v, e, w st ex e0 be object st e0 DJoins (v,w,G) holds ( VertexDomRel H) = ( VertexDomRel G)

    proof

      let v,e,w be object, H be addEdge of G, v, e, w;

      given e0 be object such that

       A1: e0 DJoins (v,w,G);

      per cases ;

        suppose

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

        G is Subgraph of H by GLIB_006: 57;

        then

         A3: ( VertexDomRel G) c= ( VertexDomRel H) by Th15;

        now

          let x,y be object;

          assume [x, y] in ( VertexDomRel H);

          then

          consider e9 be object such that

           A4: e9 DJoins (x,y,H) by Th1;

          per cases by A4, GLIB_006: 71;

            suppose e9 DJoins (x,y,G);

            hence [x, y] in ( VertexDomRel G) by Th1;

          end;

            suppose

             A5: not e9 in ( the_Edges_of G);

            

             A6: ( the_Edges_of H) = (( the_Edges_of G) \/ {e}) by A2, GLIB_006:def 11;

            e9 in ( the_Edges_of H) by A4, GLIB_000:def 14;

            then e9 in {e} by A5, A6, XBOOLE_0:def 3;

            then

             A7: e DJoins (x,y,H) by A4, TARSKI:def 1;

            e DJoins (v,w,H) by A2, GLIB_006: 105;

            then v = x & w = y by A7, GLIB_009: 6;

            hence [x, y] in ( VertexDomRel G) by A1, Th1;

          end;

        end;

        then ( VertexDomRel H) c= ( VertexDomRel G) by RELAT_1:def 3;

        hence thesis by A3, XBOOLE_0:def 10;

      end;

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

        then G == H by GLIB_006:def 11;

        hence thesis by Th19;

      end;

    end;

    theorem :: GLUNIR00:27

    

     Th27: for v,w be Vertex of G, e be object, H be addEdge of G, v, e, w st not e in ( the_Edges_of G) holds ( VertexDomRel H) = (( VertexDomRel G) \/ { [v, w]})

    proof

      let v,w be Vertex of G, e be object, H be addEdge of G, v, e, w;

      assume

       A1: not e in ( the_Edges_of G);

      now

        let x,y be object;

        hereby

          assume [x, y] in ( VertexDomRel H);

          then

          consider e0 be object such that

           A2: e0 DJoins (x,y,H) by Th1;

          per cases by A2, GLIB_006: 71;

            suppose e0 DJoins (x,y,G);

            then [x, y] in ( VertexDomRel G) by Th1;

            hence [x, y] in (( VertexDomRel G) \/ { [v, w]}) by XBOOLE_0:def 3;

          end;

            suppose

             A3: not e0 in ( the_Edges_of G);

            

             A4: ( the_Edges_of H) = (( the_Edges_of G) \/ {e}) by A1, GLIB_006:def 11;

            e0 in ( the_Edges_of H) by A2, GLIB_000:def 14;

            then e0 in {e} by A3, A4, XBOOLE_0:def 3;

            then

             A5: e DJoins (x,y,H) by A2, TARSKI:def 1;

            e DJoins (v,w,H) by A1, GLIB_006: 105;

            then x = v & y = w by A5, GLIB_009: 6;

            then [x, y] in { [v, w]} by TARSKI:def 1;

            hence [x, y] in (( VertexDomRel G) \/ { [v, w]}) by XBOOLE_0:def 3;

          end;

        end;

        assume [x, y] in (( VertexDomRel G) \/ { [v, w]});

        per cases by XBOOLE_0:def 3;

          suppose

           A6: [x, y] in ( VertexDomRel G);

          G is Subgraph of H by GLIB_006: 57;

          hence [x, y] in ( VertexDomRel H) by A6, Th15, TARSKI:def 3;

        end;

          suppose [x, y] in { [v, w]};

          then [x, y] = [v, w] by TARSKI:def 1;

          hence [x, y] in ( VertexDomRel H) by A1, Th1, GLIB_006: 105;

        end;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    theorem :: GLUNIR00:28

    for v be Vertex of G, e,w be object, H be addAdjVertex of G, v, e, w st not e in ( the_Edges_of G) & not w in ( the_Vertices_of G) holds ( VertexDomRel H) = (( VertexDomRel G) \/ { [v, w]})

    proof

      let v be Vertex of G, e,w be object, H be addAdjVertex of G, v, e, w;

      assume

       A1: not e in ( the_Edges_of G) & not w in ( the_Vertices_of G);

      then

      consider G9 be addVertex of G, w such that

       A2: H is addEdge of G9, v, e, w by GLIB_006: 125;

      

       A3: not e in ( the_Edges_of G9) by A1, GLIB_006:def 10;

      v is Vertex of G9 & w is Vertex of G9 by GLIB_006: 68, GLIB_006: 94;

      

      hence ( VertexDomRel H) = (( VertexDomRel G9) \/ { [v, w]}) by A2, A3, Th27

      .= (( VertexDomRel G) \/ { [v, w]}) by Th25;

    end;

    theorem :: GLUNIR00:29

    for v,e be object, w be Vertex of G, H be addAdjVertex of G, v, e, w st not e in ( the_Edges_of G) & not v in ( the_Vertices_of G) holds ( VertexDomRel H) = (( VertexDomRel G) \/ { [v, w]})

    proof

      let v,e be object, w be Vertex of G, H be addAdjVertex of G, v, e, w;

      assume

       A1: not e in ( the_Edges_of G) & not v in ( the_Vertices_of G);

      then

      consider G9 be addVertex of G, v such that

       A2: H is addEdge of G9, v, e, w by GLIB_006: 126;

      

       A3: not e in ( the_Edges_of G9) by A1, GLIB_006:def 10;

      v is Vertex of G9 & w is Vertex of G9 by GLIB_006: 68, GLIB_006: 94;

      

      hence ( VertexDomRel H) = (( VertexDomRel G9) \/ { [v, w]}) by A2, A3, Th27

      .= (( VertexDomRel G) \/ { [v, w]}) by Th25;

    end;

    theorem :: GLUNIR00:30

    

     Th30: for V be Subset of ( the_Vertices_of G), H be addLoops of G, V holds ( VertexDomRel H) = (( VertexDomRel G) \/ ( id V))

    proof

      let V be Subset of ( the_Vertices_of G), H be addLoops of G, V;

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

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

       A2: ( dom f) = E & ( rng f) = V and

       A3: ( the_Source_of H) = (( the_Source_of G) +* f) and

       A4: ( the_Target_of H) = (( the_Target_of G) +* f) by GLIB_012:def 5;

      now

        let v,w be object;

        hereby

          assume [v, w] in ( VertexDomRel H);

          then

          consider e be object such that

           A5: e DJoins (v,w,H) by Th1;

          per cases by A5, GLIB_006: 71;

            suppose e DJoins (v,w,G);

            then [v, w] in ( VertexDomRel G) by Th1;

            hence [v, w] in (( VertexDomRel G) \/ ( id V)) by XBOOLE_0:def 3;

          end;

            suppose

             A6: not e in ( the_Edges_of G);

            e in ( the_Edges_of H) by A5, GLIB_000:def 14;

            then

             A7: e in E by A1, A6, XBOOLE_0:def 3;

            

             A8: v = (( the_Source_of H) . e) by A5, GLIB_000:def 14

            .= (f . e) by A2, A3, A7, FUNCT_4: 13;

            w = (( the_Target_of H) . e) by A5, GLIB_000:def 14

            .= (f . e) by A2, A4, A7, FUNCT_4: 13;

            then

             A9: v = w by A8;

            v in V by A2, A7, A8, FUNCT_1: 3;

            then [v, w] in ( id V) by A9, RELAT_1:def 10;

            hence [v, w] in (( VertexDomRel G) \/ ( id V)) by XBOOLE_0:def 3;

          end;

        end;

        assume [v, w] in (( VertexDomRel G) \/ ( id V));

        per cases by XBOOLE_0:def 3;

          suppose

           A10: [v, w] in ( VertexDomRel G);

          G is Subgraph of H by GLIB_006: 57;

          hence [v, w] in ( VertexDomRel H) by A10, Th15, TARSKI:def 3;

        end;

          suppose [v, w] in ( id V);

          then

           A11: v = w & v in V by RELAT_1:def 10;

          then

          reconsider v0 = v as Vertex of H by GLIB_012:def 5;

          (v0,v0) are_adjacent by A11, GLIB_012: 18;

          then

          consider e be object such that

           A12: e Joins (v,v,H) by CHORD:def 3;

          e DJoins (v,v,H) by A12, GLIB_000: 16;

          hence [v, w] in ( VertexDomRel H) by A11, Th1;

        end;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    theorem :: GLUNIR00:31

    for H be DLGraphComplement of G holds ( VertexDomRel H) = ( [:( the_Vertices_of G), ( the_Vertices_of G):] \ ( VertexDomRel G))

    proof

      let H be DLGraphComplement of G;

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

      now

        let x,y be object;

        hereby

          assume

           A1: [x, y] in ( VertexDomRel H);

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

          then

           A2: [x, y] in N by A1;

          consider e2 be object such that

           A3: e2 DJoins (x,y,H) by A1, Th1;

          x in ( the_Vertices_of G) & y in ( the_Vertices_of G) by A2, ZFMISC_1: 87;

          then not ex e1 be object st e1 DJoins (x,y,G) by A3, GLIB_012:def 6;

          then not [x, y] in ( VertexDomRel G) by Th1;

          hence [x, y] in (N \ ( VertexDomRel G)) by A2, XBOOLE_0:def 5;

        end;

        assume [x, y] in (N \ ( VertexDomRel G));

        then

         A4: [x, y] in N & not [x, y] in ( VertexDomRel G) by XBOOLE_0:def 5;

        then

         A5: x in ( the_Vertices_of G) & y in ( the_Vertices_of G) by ZFMISC_1: 87;

         not ex e1 be object st e1 DJoins (x,y,G) by A4, Th1;

        then ex e2 be object st e2 DJoins (x,y,H) by A5, GLIB_012:def 6;

        hence [x, y] in ( VertexDomRel H) by Th1;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    definition

      let G;

      :: GLUNIR00:def2

      func VertexAdjSymRel (G) -> Relation of ( the_Vertices_of G) equals (( VertexDomRel G) \/ (( VertexDomRel G) ~ ));

      coherence ;

    end

    theorem :: GLUNIR00:32

    

     Th32: for v,w be object holds [v, w] in ( VertexAdjSymRel G) iff ex e be object st e Joins (v,w,G)

    proof

      let v,w be object;

      hereby

        assume [v, w] in ( VertexAdjSymRel G);

        per cases by XBOOLE_0:def 3;

          suppose [v, w] in ( VertexDomRel G);

          then

          consider e be object such that

           A1: e DJoins (v,w,G) by Th1;

          take e;

          thus e Joins (v,w,G) by A1, GLIB_000: 16;

        end;

          suppose [v, w] in (( VertexDomRel G) ~ );

          then

          consider e be object such that

           A2: e DJoins (w,v,G) by Th2;

          take e;

          thus e Joins (v,w,G) by A2, GLIB_000: 16;

        end;

      end;

      given e be object such that

       A3: e Joins (v,w,G);

      per cases by A3, GLIB_000: 16;

        suppose e DJoins (v,w,G);

        then [v, w] in ( VertexDomRel G) by Th1;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose e DJoins (w,v,G);

        then [v, w] in (( VertexDomRel G) ~ ) by Th2;

        hence thesis by XBOOLE_0:def 3;

      end;

    end;

    theorem :: GLUNIR00:33

    

     Th33: for v,w be Vertex of G holds [v, w] in ( VertexAdjSymRel G) iff (v,w) are_adjacent

    proof

      let v,w be Vertex of G;

      hereby

        assume [v, w] in ( VertexAdjSymRel G);

        then

        consider e be object such that

         A1: e Joins (v,w,G) by Th32;

        thus (v,w) are_adjacent by A1, CHORD:def 3;

      end;

      assume (v,w) are_adjacent ;

      then

      consider e be object such that

       A2: e Joins (v,w,G) by CHORD:def 3;

      thus [v, w] in ( VertexAdjSymRel G) by A2, Th32;

    end;

    theorem :: GLUNIR00:34

    

     Th34: ( VertexDomRel G) c= ( VertexAdjSymRel G) by XBOOLE_1: 7;

    theorem :: GLUNIR00:35

    ( VertexAdjSymRel G) = (((( the_Source_of G) qua Relation ~ ) * ( the_Target_of G)) \/ ((( the_Target_of G) qua Relation ~ ) * ( the_Source_of G)))

    proof

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

      

      thus ( VertexAdjSymRel G) = (((S qua Relation ~ ) * T) \/ ((T qua Relation ~ ) * ((S qua Relation ~ ) ~ ))) by RELAT_1: 35

      .= (((S qua Relation ~ ) * T) \/ ((T qua Relation ~ ) * S));

    end;

    registration

      let G;

      cluster ( VertexAdjSymRel G) -> symmetric;

      coherence

      proof

        (( VertexAdjSymRel G) ~ ) = ((( VertexDomRel G) ~ ) \/ ((( VertexDomRel G) ~ ) ~ )) by RELAT_1: 23

        .= ( VertexAdjSymRel G);

        hence thesis by RELAT_2: 13;

      end;

    end

    

     Lm3: G is loopless iff ( VertexAdjSymRel G) misses ( id ( the_Vertices_of G))

    proof

      hereby

        set H = the reverseEdgeDirections of G;

        

         A1: ( VertexDomRel H) = (( VertexDomRel G) ~ ) by Th20;

        assume

         A2: G is loopless;

        then

         A3: ( VertexDomRel G) misses ( id ( the_Vertices_of G)) by Lm1;

        ( VertexDomRel H) misses ( id ( the_Vertices_of H)) by A2, Lm1;

        then (( VertexDomRel G) ~ ) misses ( id ( the_Vertices_of G)) by A1, GLIB_007: 4;

        hence ( VertexAdjSymRel G) misses ( id ( the_Vertices_of G)) by A3, XBOOLE_1: 70;

      end;

      assume ( VertexAdjSymRel G) misses ( id ( the_Vertices_of G));

      then ( VertexDomRel G) misses ( id ( the_Vertices_of G)) by XBOOLE_1: 70;

      hence thesis by Lm1;

    end;

    theorem :: GLUNIR00:36

    

     Th36: G is loopless iff ( VertexAdjSymRel G) is irreflexive

    proof

      thus G is loopless implies ( VertexAdjSymRel G) is irreflexive;

      assume ( VertexAdjSymRel G) is irreflexive;

      then ( VertexAdjSymRel G) misses ( id ( the_Vertices_of G)) by GLIBPRE0: 11;

      hence G is loopless by Lm3;

    end;

    registration

      let G be loopless _Graph;

      cluster ( VertexAdjSymRel G) -> irreflexive;

      coherence ;

    end

    registration

      let G be non loopless _Graph;

      cluster ( VertexAdjSymRel G) -> non irreflexive;

      coherence by Th36;

    end

    theorem :: GLUNIR00:37

    for G be loopless _Graph st ( VertexAdjSymRel G) is total holds for C be Component of G holds C is non _trivial

    proof

      let G be loopless _Graph;

      assume ( VertexAdjSymRel G) is total;

      then

       A1: ( dom ( VertexAdjSymRel G)) = ( the_Vertices_of G) by PARTFUN1:def 2;

      ( field ( VertexDomRel G)) = (( field ( VertexDomRel G)) \/ ( field ( VertexDomRel G)))

      .= (( field ( VertexDomRel G)) \/ ( field (( VertexDomRel G) ~ ))) by RELAT_1: 21

      .= ( field ( VertexAdjSymRel G)) by RELAT_1: 18

      .= (( dom ( VertexAdjSymRel G)) \/ ( rng ( VertexAdjSymRel G))) by RELAT_1:def 6;

      then

       A2: ( the_Vertices_of G) c= ( field ( VertexDomRel G)) by A1, XBOOLE_1: 7;

      ( field ( VertexDomRel G)) c= (( the_Vertices_of G) \/ ( the_Vertices_of G)) by RELSET_1: 8;

      hence thesis by A2, Th5, XBOOLE_0:def 10;

    end;

    theorem :: GLUNIR00:38

    

     Th38: for G be _Graph st for C be Component of G holds C is non _trivial holds ( VertexAdjSymRel G) is total

    proof

      let G be _Graph;

      assume for C be Component of G holds C is non _trivial;

      then

       A1: ( field ( VertexDomRel G)) = ( the_Vertices_of G) by Th6;

      ( dom ( VertexAdjSymRel G)) = (( dom ( VertexDomRel G)) \/ ( dom (( VertexDomRel G) ~ ))) by XTUPLE_0: 23

      .= (( dom ( VertexDomRel G)) \/ ( rng ( VertexDomRel G))) by RELAT_1: 20

      .= ( the_Vertices_of G) by A1, RELAT_1:def 6;

      hence thesis by PARTFUN1:def 2;

    end;

    registration

      let G be non _trivial connected _Graph;

      cluster ( VertexAdjSymRel G) -> total;

      coherence

      proof

        now

          let C be Component of G;

          set v = the Vertex of C;

          ( the_Vertices_of C) c= ( the_Vertices_of G);

          then v in ( the_Vertices_of G) & G is Component of G by GLIB_002: 30, TARSKI:def 3;

          then C == G by GLIB_002: 34;

          hence C is non _trivial by GLIB_000: 89;

        end;

        hence thesis by Th38;

      end;

    end

    registration

      let G be complete _Graph;

      cluster ( VertexAdjSymRel G) -> connected;

      coherence

      proof

        set F = ( field ( VertexAdjSymRel G));

        now

          let x,y be object;

          assume

           A1: x in F & y in F & x <> y;

          F c= (( the_Vertices_of G) \/ ( the_Vertices_of G)) by RELSET_1: 8;

          then

          reconsider v = x, w = y as Vertex of G by A1;

          (v,w) are_adjacent by A1, CHORD:def 6;

          hence [x, y] in ( VertexAdjSymRel G) or [y, x] in ( VertexAdjSymRel G) by Th33;

        end;

        hence ( VertexAdjSymRel G) is connected by RELAT_2:def 6, RELAT_2:def 14;

      end;

    end

    theorem :: GLUNIR00:39

    G is edgeless iff ( VertexAdjSymRel G) is empty

    proof

      hereby

        assume G is edgeless;

        then ( VertexDomRel G) is empty;

        hence ( VertexAdjSymRel G) is empty;

      end;

      thus thesis;

    end;

    registration

      let G be edgeless _Graph;

      cluster ( VertexAdjSymRel G) -> empty;

      coherence ;

    end

    registration

      let G be non edgeless _Graph;

      cluster ( VertexAdjSymRel G) -> non empty;

      coherence ;

    end

    

     Lm4: G is loopfull iff ( id ( the_Vertices_of G)) c= ( VertexAdjSymRel G)

    proof

      hereby

        assume G is loopfull;

        then

         A1: ( id ( the_Vertices_of G)) c= ( VertexDomRel G) by Lm2;

        ( VertexDomRel G) c= ( VertexAdjSymRel G) by Th34;

        hence ( id ( the_Vertices_of G)) c= ( VertexAdjSymRel G) by A1, XBOOLE_1: 1;

      end;

      assume

       A2: ( id ( the_Vertices_of G)) c= ( VertexAdjSymRel G);

      now

        let v be Vertex of G;

         [v, v] in ( id ( the_Vertices_of G)) by RELAT_1:def 10;

        hence ex e be object st e Joins (v,v,G) by A2, Th32;

      end;

      hence thesis by GLIB_012:def 1;

    end;

    theorem :: GLUNIR00:40

    

     Th40: G is loopfull iff ( VertexAdjSymRel G) is total reflexive

    proof

      hereby

        assume G is loopfull;

        then ( id ( the_Vertices_of G)) c= ( VertexAdjSymRel G) by Lm4;

        hence ( VertexAdjSymRel G) is total reflexive by ROUGHS_1: 3;

      end;

      assume ( VertexAdjSymRel G) is total reflexive;

      then ( id ( the_Vertices_of G)) c= ( VertexAdjSymRel G) by ROUGHS_1: 3;

      hence G is loopfull by Lm4;

    end;

    registration

      let G be loopfull _Graph;

      cluster ( VertexAdjSymRel G) -> reflexive total;

      coherence by Th40;

    end

    registration

      let G be vertex-finite _Graph;

      cluster ( VertexAdjSymRel G) -> finite;

      coherence ;

    end

    theorem :: GLUNIR00:41

    

     Th41: ( card ( Class ( DEdgeAdjEqRel G))) c= ( card ( VertexAdjSymRel G))

    proof

      ( card ( VertexDomRel G)) c= ( card ( VertexAdjSymRel G)) by Th34, CARD_1: 11;

      hence thesis by Th10;

    end;

    theorem :: GLUNIR00:42

    ( card ( Class ( EdgeAdjEqRel G))) c= ( card ( VertexAdjSymRel G))

    proof

      set R = ( VertexAdjSymRel G);

      defpred P[ object, object] means ex e be object st e Joins (($1 `1 ),($1 `2 ),G) & $2 = ( Class (( EdgeAdjEqRel G),e));

      

       A1: for x,y1,y2 be object st x in R & P[x, y1] & P[x, y2] holds y1 = y2

      proof

        let x,y1,y2 be object;

        assume

         A2: x in R & P[x, y1] & P[x, y2];

        then

        consider e1 be object such that

         A3: e1 Joins ((x `1 ),(x `2 ),G) & y1 = ( Class (( EdgeAdjEqRel G),e1));

        consider e2 be object such that

         A4: e2 Joins ((x `1 ),(x `2 ),G) & y2 = ( Class (( EdgeAdjEqRel G),e2)) by A2;

         [e1, e2] in ( EdgeAdjEqRel G) by A3, A4, GLIB_009:def 3;

        then

         A5: e2 in ( Class (( EdgeAdjEqRel G),e1)) by EQREL_1: 18;

        e1 in ( the_Edges_of G) by A3, GLIB_000:def 13;

        hence thesis by A3, A4, A5, EQREL_1: 23;

      end;

      

       A6: for x be object st x in R holds ex y be object st P[x, y]

      proof

        let x be object;

        assume

         A7: x in R;

        then

        consider v,w be object such that

         A8: x = [v, w] by RELAT_1:def 1;

        consider e be object such that

         A9: e Joins (v,w,G) by A7, A8, Th32;

        take ( Class (( EdgeAdjEqRel G),e)), e;

        thus thesis by A8, A9;

      end;

      consider f be Function such that

       A10: ( dom f) = R & for x be object st x in R holds P[x, (f . x)] from FUNCT_1:sch 2( A1, A6);

      now

        let y be object;

        hereby

          assume y in ( rng f);

          then

          consider x be object such that

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

          consider e be object such that

           A12: e Joins ((x `1 ),(x `2 ),G) & y = ( Class (( EdgeAdjEqRel G),e)) by A10, A11;

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

          hence y in ( Class ( EdgeAdjEqRel G)) by A12, EQREL_1:def 3;

        end;

        assume y in ( Class ( EdgeAdjEqRel G));

        then

        consider e be object such that

         A13: e in ( the_Edges_of G) & y = ( Class (( EdgeAdjEqRel G),e)) by EQREL_1:def 3;

        set x = [(( the_Source_of G) . e), (( the_Target_of G) . e)];

        

         A14: e Joins ((x `1 ),(x `2 ),G) by A13, GLIB_000:def 13;

        then

         A15: x in R by Th32;

        then P[x, (f . x)] by A10;

        then (f . x) = y by A1, A13, A14, A15;

        hence y in ( rng f) by A10, A15, FUNCT_1: 3;

      end;

      then ( rng f) = ( Class ( EdgeAdjEqRel G)) by TARSKI: 2;

      hence thesis by A10, CARD_1: 12;

    end;

    theorem :: GLUNIR00:43

    for G be non-Dmulti _Graph holds (G .size() ) c= ( card ( VertexAdjSymRel G))

    proof

      let G be non-Dmulti _Graph;

      ( card ( VertexDomRel G)) = ( card ( Class ( DEdgeAdjEqRel G))) by Th10;

      then (G .size() ) = ( card ( Class ( DEdgeAdjEqRel G))) by Th12;

      hence (G .size() ) c= ( card ( VertexAdjSymRel G)) by Th41;

    end;

    theorem :: GLUNIR00:44

    for v be Vertex of G holds ( Im (( VertexAdjSymRel G),v)) = (v .allNeighbors() )

    proof

      let v be Vertex of G;

      now

        let x be object;

        hereby

          assume x in (( VertexAdjSymRel G) .: {v});

          then

          consider v0 be object such that

           A1: [v0, x] in ( VertexAdjSymRel G) & v0 in {v} by RELAT_1:def 13;

           [v, x] in ( VertexAdjSymRel G) by A1, TARSKI:def 1;

          then x is set & ex e be object st e Joins (v,x,G) by Th32, TARSKI: 1;

          hence x in (v .allNeighbors() ) by GLIB_000: 71;

        end;

        assume x in (v .allNeighbors() );

        then ex e be object st e Joins (v,x,G) by GLIB_000: 71;

        then [v, x] in ( VertexAdjSymRel G) & v in {v} by Th32, TARSKI:def 1;

        hence x in (( VertexAdjSymRel G) .: {v}) by RELAT_1:def 13;

      end;

      then (( VertexAdjSymRel G) .: {v}) = (v .allNeighbors() ) by TARSKI: 2;

      hence thesis by RELAT_1:def 16;

    end;

    theorem :: GLUNIR00:45

    

     Th45: for H be Subgraph of G holds ( VertexAdjSymRel H) c= ( VertexAdjSymRel G)

    proof

      let H be Subgraph of G;

      

       A1: ( VertexDomRel H) c= ( VertexDomRel G) by Th15;

      then (( VertexDomRel H) ~ ) c= (( VertexDomRel G) ~ ) by SYSREL: 11;

      hence thesis by A1, XBOOLE_1: 13;

    end;

    theorem :: GLUNIR00:46

    

     Th46: for H be removeParallelEdges of G holds ( VertexAdjSymRel H) = ( VertexAdjSymRel G)

    proof

      let H be removeParallelEdges of G;

      consider E be RepEdgeSelection of G such that

       A1: H is inducedSubgraph of G, ( the_Vertices_of G), E by GLIB_009:def 7;

      

       A2: ( VertexAdjSymRel H) c= ( VertexAdjSymRel G) by Th45;

      now

        let v,w be object;

        assume [v, w] in ( VertexAdjSymRel G);

        then

        consider e0 be object such that

         A3: e0 Joins (v,w,G) by Th32;

        ( the_Edges_of G) = (G .edgesBetween ( the_Vertices_of G)) & ( the_Vertices_of G) c= ( the_Vertices_of G) by GLIB_000: 34;

        then

         A4: ( the_Edges_of H) = E by A1, GLIB_000:def 37;

        consider e be object such that

         A5: e Joins (v,w,G) & e in E and for e9 be object st e9 Joins (v,w,G) & e9 in E holds e9 = e by A3, GLIB_009:def 5;

        v is set & w is set by TARSKI: 1;

        then e Joins (v,w,H) by A4, A5, GLIB_000: 73;

        hence [v, w] in ( VertexAdjSymRel H) by Th32;

      end;

      then ( VertexAdjSymRel G) c= ( VertexAdjSymRel H) by RELAT_1:def 3;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: GLUNIR00:47

    

     Th47: for H be removeLoops of G holds ( VertexAdjSymRel H) = (( VertexAdjSymRel G) \ ( id ( the_Vertices_of G)))

    proof

      let H be removeLoops of G;

      

       A1: ( VertexDomRel H) = (( VertexDomRel G) \ ( id ( the_Vertices_of G))) by Th17;

      

      then (( VertexDomRel H) ~ ) = ((( VertexDomRel G) ~ ) \ (( id ( the_Vertices_of G)) qua Relation ~ )) by RELAT_1: 24

      .= ((( VertexDomRel G) ~ ) \ ( id ( the_Vertices_of G)));

      hence thesis by A1, XBOOLE_1: 42;

    end;

    theorem :: GLUNIR00:48

    for H be SimpleGraph of G holds ( VertexAdjSymRel H) = (( VertexAdjSymRel G) \ ( id ( the_Vertices_of G)))

    proof

      let H be SimpleGraph of G;

      consider G9 be removeParallelEdges of G such that

       A1: H is removeLoops of G9 by GLIB_009: 119;

      

       A2: ( the_Vertices_of G9) = ( the_Vertices_of G) by GLIB_000:def 33;

      

      thus ( VertexAdjSymRel H) = (( VertexAdjSymRel G9) \ ( id ( the_Vertices_of G9))) by A1, Th47

      .= (( VertexAdjSymRel G) \ ( id ( the_Vertices_of G))) by A2, Th46;

    end;

    theorem :: GLUNIR00:49

    

     Th49: for G1,G2 be _Graph st G1 == G2 holds ( VertexAdjSymRel G1) = ( VertexAdjSymRel G2)

    proof

      let G1,G2 be _Graph such that

       A1: G1 == G2;

      

      thus ( VertexAdjSymRel G1) = (( VertexDomRel G2) \/ (( VertexDomRel G1) ~ )) by A1, Th19

      .= ( VertexAdjSymRel G2) by A1, Th19;

    end;

    theorem :: GLUNIR00:50

    for E be set, H be reverseEdgeDirections of G, E holds ( VertexAdjSymRel H) = ( VertexAdjSymRel G)

    proof

      let E be set, H be reverseEdgeDirections of G, E;

      now

        let v,w be object;

        hereby

          assume [v, w] in ( VertexAdjSymRel G);

          then

          consider e be object such that

           A1: e Joins (v,w,G) by Th32;

          e Joins (v,w,H) by A1, GLIB_007: 9;

          hence [v, w] in ( VertexAdjSymRel H) by Th32;

        end;

        assume [v, w] in ( VertexAdjSymRel H);

        then

        consider e be object such that

         A2: e Joins (v,w,H) by Th32;

        e Joins (v,w,G) by A2, GLIB_007: 9;

        hence [v, w] in ( VertexAdjSymRel G) by Th32;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    theorem :: GLUNIR00:51

    for V be non empty Subset of ( the_Vertices_of G) holds for H be inducedSubgraph of G, V holds ( VertexAdjSymRel H) = (( VertexAdjSymRel G) /\ [:V, V:])

    proof

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

      let H be inducedSubgraph of G, V;

      

       A1: ( VertexDomRel H) = (( VertexDomRel G) /\ [:V, V:]) by Th21;

      

      then (( VertexDomRel H) ~ ) = ((( VertexDomRel G) ~ ) /\ ( [:V, V:] ~ )) by RELAT_1: 22

      .= ((( VertexDomRel G) ~ ) /\ [:V, V:]) by SYSREL: 5;

      hence ( VertexAdjSymRel H) = (( VertexAdjSymRel G) /\ [:V, V:]) by A1, XBOOLE_1: 23;

    end;

    theorem :: GLUNIR00:52

    

     Th52: for V be set, H be removeVertices of G, V st V c< ( the_Vertices_of G) holds ( VertexAdjSymRel H) = (( VertexAdjSymRel G) \ ( [:V, ( the_Vertices_of G):] \/ [:( the_Vertices_of G), V:]))

    proof

      let V be set, H be removeVertices of G, V;

      assume

       A1: V c< ( the_Vertices_of G);

      set V1 = [:V, ( the_Vertices_of G):], V2 = [:( the_Vertices_of G), V:];

      

       A2: ( VertexDomRel H) = (( VertexDomRel G) \ (V1 \/ V2)) by A1, Th22;

      

      then (( VertexDomRel H) ~ ) = ((( VertexDomRel G) ~ ) \ ((V1 \/ V2) ~ )) by RELAT_1: 24

      .= ((( VertexDomRel G) ~ ) \ ((V1 ~ ) \/ (V2 ~ ))) by RELAT_1: 23

      .= ((( VertexDomRel G) ~ ) \ ((V1 ~ ) \/ V1)) by SYSREL: 5

      .= ((( VertexDomRel G) ~ ) \ (V2 \/ V1)) by SYSREL: 5;

      hence thesis by A2, XBOOLE_1: 42;

    end;

    theorem :: GLUNIR00:53

    for G be non _trivial _Graph, v be Vertex of G holds for H be removeVertex of G, v holds ( VertexAdjSymRel H) = (( VertexAdjSymRel G) \ ( [: {v}, ( the_Vertices_of G):] \/ [:( the_Vertices_of G), {v}:]))

    proof

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

      let H be removeVertex of G, v;

      (( the_Vertices_of G) \ {v}) is non empty by GLIB_000: 20;

      then not ( the_Vertices_of G) = {v} by XBOOLE_1: 37;

      hence thesis by Th52, XBOOLE_0:def 8;

    end;

    theorem :: GLUNIR00:54

    for G be non _trivial _Graph, v be Vertex of G holds for H be removeVertex of G, v st v is isolated holds ( VertexAdjSymRel H) = ( VertexAdjSymRel G)

    proof

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

      let H be removeVertex of G, v;

      assume v is isolated;

      then ( VertexDomRel H) = ( VertexDomRel G) by Th24;

      hence thesis;

    end;

    theorem :: GLUNIR00:55

    

     Th55: for V be set, H be addVertices of G, V holds ( VertexAdjSymRel H) = ( VertexAdjSymRel G)

    proof

      let V be set, H be addVertices of G, V;

      ( VertexDomRel H) = ( VertexDomRel G) by Th25;

      hence thesis;

    end;

    theorem :: GLUNIR00:56

    for v,w be Vertex of G, e be object, H be addEdge of G, v, e, w st (v,w) are_adjacent holds ( VertexAdjSymRel H) = ( VertexAdjSymRel G)

    proof

      let v,w be Vertex of G, e be object, H be addEdge of G, v, e, w;

      assume (v,w) are_adjacent ;

      then

      consider e0 be object such that

       A1: e0 Joins (v,w,G) by CHORD:def 3;

      per cases ;

        suppose

         A2: not e in ( the_Edges_of G);

        per cases by A1, GLIB_000: 16;

          suppose

           A3: e0 DJoins (v,w,G);

          

          thus ( VertexAdjSymRel H) = (( VertexDomRel G) \/ (( VertexDomRel H) ~ )) by A3, Th26

          .= ( VertexAdjSymRel G) by A3, Th26;

        end;

          suppose e0 DJoins (w,v,G);

          then

           A4: [w, v] in ( VertexDomRel G) by Th1;

          then

           A5: [v, w] in (( VertexDomRel G) ~ ) by RELAT_1:def 7;

          set R = ( VertexDomRel G), U = (R \/ { [v, w]});

          

           A6: (U ~ ) = ((R ~ ) \/ ( { [v, w]} qua Relation ~ )) by RELAT_1: 23;

          

          thus ( VertexAdjSymRel H) = (U \/ (( VertexDomRel H) ~ )) by A2, Th27

          .= (U \/ (U ~ )) by A2, Th27

          .= (U \/ ((R ~ ) \/ { [w, v]})) by A6, GLIBPRE0: 12

          .= ((U \/ { [w, v]}) \/ (R ~ )) by XBOOLE_1: 4

          .= (((R \/ { [w, v]}) \/ { [v, w]}) \/ (R ~ )) by XBOOLE_1: 4

          .= ((R \/ { [w, v]}) \/ ((R ~ ) \/ { [v, w]})) by XBOOLE_1: 4

          .= (R \/ ((R ~ ) \/ { [v, w]})) by A4, ZFMISC_1: 31, XBOOLE_1: 12

          .= ( VertexAdjSymRel G) by A5, ZFMISC_1: 31, XBOOLE_1: 12;

        end;

      end;

        suppose e in ( the_Edges_of G);

        then G == H by GLIB_006:def 11;

        hence thesis by Th49;

      end;

    end;

    theorem :: GLUNIR00:57

    

     Th57: for v,w be Vertex of G, e be object, H be addEdge of G, v, e, w st not e in ( the_Edges_of G) holds ( VertexAdjSymRel H) = (( VertexAdjSymRel G) \/ { [v, w], [w, v]})

    proof

      let v,w be Vertex of G, e be object, H be addEdge of G, v, e, w;

      assume

       A1: not e in ( the_Edges_of G);

      set R = ( VertexDomRel G), U = (R \/ { [v, w]});

      

       A2: (U ~ ) = ((R ~ ) \/ ( { [v, w]} qua Relation ~ )) by RELAT_1: 23;

      

      thus ( VertexAdjSymRel H) = (U \/ (( VertexDomRel H) ~ )) by A1, Th27

      .= (U \/ (U ~ )) by A1, Th27

      .= (U \/ ((R ~ ) \/ { [w, v]})) by A2, GLIBPRE0: 12

      .= ((U \/ (R ~ )) \/ { [w, v]}) by XBOOLE_1: 4

      .= (((R \/ (R ~ )) \/ { [v, w]}) \/ { [w, v]}) by XBOOLE_1: 4

      .= ((R \/ (R ~ )) \/ ( { [v, w]} \/ { [w, v]})) by XBOOLE_1: 4

      .= (( VertexAdjSymRel G) \/ { [v, w], [w, v]}) by ENUMSET1: 1;

    end;

    theorem :: GLUNIR00:58

    for v be Vertex of G, e,w be object, H be addAdjVertex of G, v, e, w st not e in ( the_Edges_of G) & not w in ( the_Vertices_of G) holds ( VertexAdjSymRel H) = (( VertexAdjSymRel G) \/ { [v, w], [w, v]})

    proof

      let v be Vertex of G, e,w be object, H be addAdjVertex of G, v, e, w;

      assume

       A1: not e in ( the_Edges_of G) & not w in ( the_Vertices_of G);

      then

      consider G9 be addVertex of G, w such that

       A2: H is addEdge of G9, v, e, w by GLIB_006: 125;

      

       A3: not e in ( the_Edges_of G9) by A1, GLIB_006:def 10;

      v is Vertex of G9 & w is Vertex of G9 by GLIB_006: 68, GLIB_006: 94;

      

      hence ( VertexAdjSymRel H) = (( VertexAdjSymRel G9) \/ { [v, w], [w, v]}) by A2, A3, Th57

      .= (( VertexAdjSymRel G) \/ { [v, w], [w, v]}) by Th55;

    end;

    theorem :: GLUNIR00:59

    for v,e be object, w be Vertex of G, H be addAdjVertex of G, v, e, w st not e in ( the_Edges_of G) & not v in ( the_Vertices_of G) holds ( VertexAdjSymRel H) = (( VertexAdjSymRel G) \/ { [v, w], [w, v]})

    proof

      let v,e be object, w be Vertex of G, H be addAdjVertex of G, v, e, w;

      assume

       A1: not e in ( the_Edges_of G) & not v in ( the_Vertices_of G);

      then

      consider G9 be addVertex of G, v such that

       A2: H is addEdge of G9, v, e, w by GLIB_006: 126;

      

       A3: not e in ( the_Edges_of G9) by A1, GLIB_006:def 10;

      v is Vertex of G9 & w is Vertex of G9 by GLIB_006: 68, GLIB_006: 94;

      

      hence ( VertexAdjSymRel H) = (( VertexAdjSymRel G9) \/ { [v, w], [w, v]}) by A2, A3, Th57

      .= (( VertexAdjSymRel G) \/ { [v, w], [w, v]}) by Th55;

    end;

    theorem :: GLUNIR00:60

    for v be object, V be Subset of ( the_Vertices_of G) holds for H be addAdjVertexAll of G, v, V st not v in ( the_Vertices_of G) holds ( VertexAdjSymRel H) = ((( VertexAdjSymRel G) \/ [: {v}, V:]) \/ [:V, {v}:])

    proof

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

      let H be addAdjVertexAll of G, v, V;

      assume

       A1: not v in ( the_Vertices_of G);

      then

      consider E be set such that

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

       A3: ( the_Edges_of H) = (( the_Edges_of G) \/ E) and

       A4: for v1 be object st v1 in V holds ex e1 be object st e1 in E & e1 Joins (v1,v,H) & for e2 be object st e2 Joins (v1,v,H) holds e1 = e2 by GLIB_007:def 4;

      set F = [: {v}, V:], L = [:V, {v}:];

      now

        let v1,v2 be object;

        hereby

          assume [v1, v2] in ( VertexAdjSymRel H);

          then

          consider e be object such that

           A5: e Joins (v1,v2,H) by Th32;

          per cases by A5, GLIB_006: 72;

            suppose e Joins (v1,v2,G);

            then [v1, v2] in ( VertexAdjSymRel G) by Th32;

            then [v1, v2] in (( VertexAdjSymRel G) \/ F) by XBOOLE_0:def 3;

            hence [v1, v2] in ((( VertexAdjSymRel G) \/ F) \/ L) by XBOOLE_0:def 3;

          end;

            suppose not e in ( the_Edges_of G);

            per cases by A1, A2, A3, A5, GLIB_007: 51;

              suppose v1 = v & v2 in V;

              then v1 in {v} & v2 in V by TARSKI:def 1;

              then [v1, v2] in F by ZFMISC_1: 87;

              then [v1, v2] in (( VertexAdjSymRel G) \/ F) by XBOOLE_0:def 3;

              hence [v1, v2] in ((( VertexAdjSymRel G) \/ F) \/ L) by XBOOLE_0:def 3;

            end;

              suppose v2 = v & v1 in V;

              then v2 in {v} & v1 in V by TARSKI:def 1;

              then [v1, v2] in L by ZFMISC_1: 87;

              hence [v1, v2] in ((( VertexAdjSymRel G) \/ F) \/ L) by XBOOLE_0:def 3;

            end;

          end;

        end;

        assume [v1, v2] in ((( VertexAdjSymRel G) \/ F) \/ L);

        then [v1, v2] in (( VertexAdjSymRel G) \/ F) or [v1, v2] in L by XBOOLE_0:def 3;

        per cases by XBOOLE_0:def 3;

          suppose

           A6: [v1, v2] in ( VertexAdjSymRel G);

          G is Subgraph of H by GLIB_006: 57;

          hence [v1, v2] in ( VertexAdjSymRel H) by A6, Th45, TARSKI:def 3;

        end;

          suppose [v1, v2] in F;

          then

           A7: v1 in {v} & v2 in V by ZFMISC_1: 87;

          then

          consider e1 be object such that

           A8: e1 in E & e1 Joins (v2,v,H) and for e2 be object st e2 Joins (v2,v,H) holds e1 = e2 by A4;

          e1 Joins (v2,v1,H) by A7, A8, TARSKI:def 1;

          then e1 Joins (v1,v2,H) by GLIB_000: 14;

          hence [v1, v2] in ( VertexAdjSymRel H) by Th32;

        end;

          suppose [v1, v2] in L;

          then

           A9: v2 in {v} & v1 in V by ZFMISC_1: 87;

          then

          consider e1 be object such that

           A10: e1 in E & e1 Joins (v1,v,H) and for e2 be object st e2 Joins (v1,v,H) holds e1 = e2 by A4;

          e1 Joins (v1,v2,H) by A9, A10, TARSKI:def 1;

          hence [v1, v2] in ( VertexAdjSymRel H) by Th32;

        end;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    theorem :: GLUNIR00:61

    for V be Subset of ( the_Vertices_of G), H be addLoops of G, V holds ( VertexAdjSymRel H) = (( VertexAdjSymRel G) \/ ( id V))

    proof

      let V be Subset of ( the_Vertices_of G), H be addLoops of G, V;

      set R = ( VertexDomRel G);

      reconsider I = ( id V) as Relation;

      

      thus ( VertexAdjSymRel H) = ((R \/ I) \/ (( VertexDomRel H) ~ )) by Th30

      .= ((R \/ I) \/ ((R \/ I) ~ )) by Th30

      .= ((R \/ I) \/ ((R ~ ) \/ (I ~ ))) by RELAT_1: 23

      .= ((R \/ ((R ~ ) \/ I)) \/ I) by XBOOLE_1: 4

      .= (((R \/ (R ~ )) \/ I) \/ I) by XBOOLE_1: 4

      .= ((R \/ (R ~ )) \/ (I \/ I)) by XBOOLE_1: 4

      .= (( VertexAdjSymRel G) \/ ( id V));

    end;

    theorem :: GLUNIR00:62

    for H be LGraphComplement of G holds ( VertexAdjSymRel H) = ( [:( the_Vertices_of G), ( the_Vertices_of G):] \ ( VertexAdjSymRel G))

    proof

      let H be LGraphComplement of G;

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

      now

        let x,y be object;

        hereby

          assume

           A1: [x, y] in ( VertexAdjSymRel H);

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

          then

           A2: [x, y] in N by A1;

          consider e2 be object such that

           A3: e2 Joins (x,y,H) by A1, Th32;

          x in ( the_Vertices_of G) & y in ( the_Vertices_of G) by A2, ZFMISC_1: 87;

          then not ex e1 be object st e1 Joins (x,y,G) by A3, GLIB_012:def 7;

          then not [x, y] in ( VertexAdjSymRel G) by Th32;

          hence [x, y] in (N \ ( VertexAdjSymRel G)) by A2, XBOOLE_0:def 5;

        end;

        assume [x, y] in (N \ ( VertexAdjSymRel G));

        then

         A4: [x, y] in N & not [x, y] in ( VertexAdjSymRel G) by XBOOLE_0:def 5;

        then

         A5: x in ( the_Vertices_of G) & y in ( the_Vertices_of G) by ZFMISC_1: 87;

         not ex e1 be object st e1 Joins (x,y,G) by A4, Th32;

        then ex e2 be object st e2 Joins (x,y,H) by A5, GLIB_012:def 7;

        hence [x, y] in ( VertexAdjSymRel H) by Th32;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    begin

    reserve V for non empty set,

E for Relation of V;

    definition

      let V, E;

      :: GLUNIR00:def3

      func createGraph (V,E) -> _Graph equals ( createGraph (V,E,(( pr1 (V,V)) | E),(( pr2 (V,V)) | E)));

      coherence ;

    end

    registration

      let V, E;

      cluster ( the_Edges_of ( createGraph (V,E))) -> Relation-like;

      coherence by GLIB_000: 6;

    end

    theorem :: GLUNIR00:63

    

     Th63: for v,w be object holds [v, w] in E iff [v, w] DJoins (v,w,( createGraph (V,E)))

    proof

      let v,w be object;

      set G0 = ( createGraph (V,E));

      hereby

        assume

         A1: [v, w] in E;

        then

         A2: [v, w] in ( the_Edges_of G0) by GLIB_000: 6;

        

         A3: v in V & w in V by A1, ZFMISC_1: 87;

        

         A4: (( the_Source_of G0) . [v, w]) = ((( pr1 (V,V)) | E) . [v, w]) by GLIB_000: 6

        .= (( pr1 (V,V)) . [v, w]) by A1, FUNCT_1: 49

        .= (( pr1 (V,V)) . (v,w)) by BINOP_1:def 1

        .= v by A3, FUNCT_3:def 4;

        (( the_Target_of G0) . [v, w]) = ((( pr2 (V,V)) | E) . [v, w]) by GLIB_000: 6

        .= (( pr2 (V,V)) . [v, w]) by A1, FUNCT_1: 49

        .= (( pr2 (V,V)) . (v,w)) by BINOP_1:def 1

        .= w by A3, FUNCT_3:def 5;

        hence [v, w] DJoins (v,w,G0) by A2, A4, GLIB_000:def 14;

      end;

      assume [v, w] DJoins (v,w,G0);

      then [v, w] in ( the_Edges_of G0) by GLIB_000:def 14;

      hence [v, w] in E by GLIB_000: 6;

    end;

    theorem :: GLUNIR00:64

    

     Th64: for e,v,w be object st e DJoins (v,w,( createGraph (V,E))) holds e = [v, w]

    proof

      let e,v,w be object;

      assume

       A1: e DJoins (v,w,( createGraph (V,E)));

      then e in ( the_Edges_of ( createGraph (V,E))) by GLIB_000:def 14;

      then

       A2: e in E by GLIB_000: 6;

      then

      consider v1,w1 be object such that

       A3: e = [v1, w1] by RELAT_1:def 1;

      e DJoins (v1,w1,( createGraph (V,E))) by A2, A3, Th63;

      then v1 = v & w1 = w by A1, GLIB_009: 6;

      hence thesis by A3;

    end;

    theorem :: GLUNIR00:65

    

     Th65: ( VertexDomRel ( createGraph (V,E))) = E

    proof

      set G0 = ( createGraph (V,E));

      now

        let v,w be object;

        hereby

          assume [v, w] in ( VertexDomRel G0);

          then

          consider e be object such that

           A1: e DJoins (v,w,G0) by Th1;

          e in ( the_Edges_of G0) by A1, GLIB_000:def 14;

          then

           A2: e in E by GLIB_000: 6;

          then

          consider v0,w0 be object such that

           A3: e = [v0, w0] by RELAT_1:def 1;

          e DJoins (v0,w0,G0) by A2, A3, Th63;

          then v0 = v & w0 = w by A1, GLIB_009: 6;

          hence [v, w] in E by A2, A3;

        end;

        assume [v, w] in E;

        then [v, w] DJoins (v,w,G0) by Th63;

        hence [v, w] in ( VertexDomRel G0) by Th1;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    registration

      let V, E;

      cluster ( createGraph (V,E)) -> plain non-Dmulti;

      coherence

      proof

        set G0 = ( createGraph (V,E));

        thus G0 is plain;

        now

          let e1,e2,v,w be object;

          assume e1 DJoins (v,w,G0) & e2 DJoins (v,w,G0);

          then e1 = [v, w] & e2 = [v, w] by Th64;

          hence e1 = e2;

        end;

        hence thesis by GLIB_000:def 21;

      end;

    end

    theorem :: GLUNIR00:66

    

     Th66: V is trivial iff ( createGraph (V,E)) is _trivial

    proof

      hereby

        assume V is trivial;

        then ( the_Vertices_of ( createGraph (V,E))) is trivial by GLIB_000: 6;

        then

        consider v be object such that

         A1: ( the_Vertices_of ( createGraph (V,E))) = {v} by ZFMISC_1: 131;

        ( card ( the_Vertices_of ( createGraph (V,E)))) = 1 by A1, CARD_1: 30;

        hence ( createGraph (V,E)) is _trivial by GLIB_000:def 19;

      end;

      assume ( createGraph (V,E)) is _trivial;

      then ( the_Vertices_of ( createGraph (V,E))) is trivial;

      hence V is trivial by GLIB_000: 6;

    end;

    registration

      let V be trivial non empty set;

      let E be Relation of V;

      cluster ( createGraph (V,E)) -> _trivial;

      coherence by Th66;

    end

    registration

      let V be non trivial set;

      let E be Relation of V;

      cluster ( createGraph (V,E)) -> non _trivial;

      coherence by Th66;

    end

    theorem :: GLUNIR00:67

    

     Th67: E is irreflexive iff ( createGraph (V,E)) is loopless

    proof

      hereby

        assume E is irreflexive;

        then ( VertexDomRel ( createGraph (V,E))) is irreflexive by Th65;

        hence ( createGraph (V,E)) is loopless;

      end;

      assume ( createGraph (V,E)) is loopless;

      then ( VertexDomRel ( createGraph (V,E))) is irreflexive;

      hence thesis by Th65;

    end;

    registration

      let V;

      let E be irreflexive Relation of V;

      cluster ( createGraph (V,E)) -> loopless;

      coherence by Th67;

    end

    registration

      let V;

      let E be non irreflexive Relation of V;

      cluster ( createGraph (V,E)) -> non loopless;

      coherence by Th67;

    end

    theorem :: GLUNIR00:68

    

     Th68: E is antisymmetric iff ( createGraph (V,E)) is non-multi

    proof

      set G0 = ( createGraph (V,E));

      hereby

        assume E is antisymmetric;

        then

         A1: E is_antisymmetric_in ( field E) by RELAT_2:def 12;

        assume G0 is non non-multi;

        then

        consider e1,e2,v,w be object such that

         A2: e1 Joins (v,w,G0) & e2 Joins (v,w,G0) & e1 <> e2 by GLIB_000:def 20;

        e1 in ( the_Edges_of G0) & e2 in ( the_Edges_of G0) by A2, GLIB_000:def 13;

        then

         A3: e1 in E & e2 in E by GLIB_000: 6;

        per cases by A2, GLIB_000: 16;

          suppose e1 DJoins (v,w,G0) & e2 DJoins (v,w,G0);

          then e1 = [v, w] & e2 = [v, w] by Th64;

          hence contradiction by A2;

        end;

          suppose e1 DJoins (v,w,G0) & e2 DJoins (w,v,G0);

          then

           A4: e1 = [v, w] & e2 = [w, v] by Th64;

          then v in ( field E) & w in ( field E) by A3, RELAT_1: 15;

          then v = w by A1, A3, A4, RELAT_2:def 4;

          hence contradiction by A2, A4;

        end;

          suppose e1 DJoins (w,v,G0) & e2 DJoins (v,w,G0);

          then

           A5: e1 = [w, v] & e2 = [v, w] by Th64;

          then v in ( field E) & w in ( field E) by A3, RELAT_1: 15;

          then v = w by A1, A3, A5, RELAT_2:def 4;

          hence contradiction by A2, A5;

        end;

          suppose e1 DJoins (w,v,G0) & e2 DJoins (w,v,G0);

          then e1 = [w, v] & e2 = [w, v] by Th64;

          hence contradiction by A2;

        end;

      end;

      assume G0 is non-multi;

      then ( VertexDomRel G0) is antisymmetric;

      hence thesis by Th65;

    end;

    registration

      let V;

      let E be antisymmetric Relation of V;

      cluster ( createGraph (V,E)) -> non-multi;

      coherence by Th68;

    end

    registration

      let V be non trivial set;

      let E be non antisymmetric Relation of V;

      cluster ( createGraph (V,E)) -> non non-multi;

      coherence by Th68;

    end

    registration

      let V;

      let E be asymmetric Relation of V;

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

      coherence ;

    end

    theorem :: GLUNIR00:69

    

     Th69: ( createGraph (V,E)) is complete implies E is connected

    proof

      assume ( createGraph (V,E)) is complete;

      then ( VertexDomRel ( createGraph (V,E))) is connected;

      hence thesis by Th65;

    end;

    registration

      let V be non trivial set;

      let E be non connected Relation of V;

      cluster ( createGraph (V,E)) -> non complete;

      coherence by Th69;

    end

    theorem :: GLUNIR00:70

    

     Th70: E is empty iff ( createGraph (V,E)) is edgeless

    proof

      thus E is empty implies ( createGraph (V,E)) is edgeless;

      assume ( createGraph (V,E)) is edgeless;

      then ( VertexDomRel ( createGraph (V,E))) is empty;

      hence thesis by Th65;

    end;

    registration

      let V;

      let E be empty Relation of V;

      cluster ( createGraph (V,E)) -> edgeless;

      coherence ;

    end

    registration

      let V;

      let E be non empty Relation of V;

      cluster ( createGraph (V,E)) -> non edgeless;

      coherence by Th70;

    end

    theorem :: GLUNIR00:71

    

     Th71: E is total reflexive iff ( createGraph (V,E)) is loopfull

    proof

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

      hereby

        assume E is total reflexive;

        then ( id V) c= E by ROUGHS_1: 3;

        then ( id ( the_Vertices_of G)) c= E by GLIB_000: 6;

        then ( id ( the_Vertices_of G)) c= ( VertexDomRel G) by Th65;

        hence ( createGraph (V,E)) is loopfull by Lm2;

      end;

      assume G is loopfull;

      then ( id ( the_Vertices_of G)) c= ( VertexDomRel G) by Lm2;

      then ( id ( the_Vertices_of G)) c= E by Th65;

      then ( id V) c= E by GLIB_000: 6;

      hence thesis by ROUGHS_1: 3;

    end;

    registration

      let V;

      let E be total reflexive Relation of V;

      cluster ( createGraph (V,E)) -> loopfull;

      coherence by Th71;

    end

    registration

      let V;

      let E be non total Relation of V;

      cluster ( createGraph (V,E)) -> non loopfull;

      coherence by Th71;

    end

    registration

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

      cluster ( createGraph (V,E)) -> finite;

      coherence ;

    end

    registration

      let V;

      let E be finite Relation of V;

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

      coherence ;

    end

    theorem :: GLUNIR00:72

    

     Th72: for v be Vertex of ( createGraph (V,E)) holds ( Im (E,v)) = (v .outNeighbors() )

    proof

      let v be Vertex of ( createGraph (V,E));

      now

        let y be object;

        hereby

          assume y in ( Im (E,v));

          then y in (E .: {v}) by RELAT_1:def 16;

          then

          consider x be object such that

           A1: [x, y] in E & x in {v} by RELAT_1:def 13;

          x = v by A1, TARSKI:def 1;

          then

           A2: [x, y] DJoins (v,y,( createGraph (V,E))) by A1, Th63;

          y is set by TARSKI: 1;

          hence y in (v .outNeighbors() ) by A2, GLIB_000: 70;

        end;

        assume y in (v .outNeighbors() );

        then

        consider e be object such that

         A3: e DJoins (v,y,( createGraph (V,E))) by GLIB_000: 70;

        e = [v, y] by A3, Th64;

        then

         A4: [v, y] in E by A3, Th63;

        v in {v} by TARSKI:def 1;

        then y in (E .: {v}) by A4, RELAT_1:def 13;

        hence y in ( Im (E,v)) by RELAT_1:def 16;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLUNIR00:73

    

     Th73: for v be Vertex of ( createGraph (V,E)) holds ( Coim (E,v)) = (v .inNeighbors() )

    proof

      let v be Vertex of ( createGraph (V,E));

      now

        let x be object;

        hereby

          assume x in ( Coim (E,v));

          then x in (E " {v}) by RELAT_1:def 17;

          then

          consider y be object such that

           A1: [x, y] in E & y in {v} by RELAT_1:def 14;

          y = v by A1, TARSKI:def 1;

          then

           A2: [x, y] DJoins (x,v,( createGraph (V,E))) by A1, Th63;

          x is set by TARSKI: 1;

          hence x in (v .inNeighbors() ) by A2, GLIB_000: 69;

        end;

        assume x in (v .inNeighbors() );

        then

        consider e be object such that

         A3: e DJoins (x,v,( createGraph (V,E))) by GLIB_000: 69;

        e = [x, v] by A3, Th64;

        then

         A4: [x, v] in E by A3, Th63;

        v in {v} by TARSKI:def 1;

        then x in (E " {v}) by A4, RELAT_1:def 14;

        hence x in ( Coim (E,v)) by RELAT_1:def 17;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLUNIR00:74

    

     Th74: for X be set holds (E | X) = (( createGraph (V,E)) .edgesOutOf X)

    proof

      let X be set;

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

      now

        let z be object;

        hereby

          assume

           A1: z in (E | X);

          then

          consider x,y be object such that

           A2: z = [x, y] by RELAT_1:def 1;

          

           A3: x in X & [x, y] in E by A1, A2, RELAT_1:def 11;

          then [x, y] DJoins (x,y,G) by Th63;

          then [x, y] in ( the_Edges_of G) & (( the_Source_of G) . [x, y]) = x by GLIB_000:def 14;

          hence z in (G .edgesOutOf X) by A2, A3, GLIB_000:def 27;

        end;

        set x = (( the_Source_of G) . z), y = (( the_Target_of G) . z);

        assume z in (G .edgesOutOf X);

        then

         A4: z in ( the_Edges_of G) & x in X by GLIB_000:def 27;

        then z DJoins (x,y,G) by GLIB_000:def 14;

        then

         A5: z = [x, y] by Th64;

        z in E by A4, GLIB_000: 6;

        hence z in (E | X) by A4, A5, RELAT_1:def 11;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLUNIR00:75

    

     Th75: for Y be set holds (Y |` E) = (( createGraph (V,E)) .edgesInto Y)

    proof

      let Y be set;

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

      now

        let z be object;

        hereby

          assume

           A1: z in (Y |` E);

          then

          consider x,y be object such that

           A2: z = [x, y] by RELAT_1:def 1;

          

           A3: y in Y & [x, y] in E by A1, A2, RELAT_1:def 12;

          then [x, y] DJoins (x,y,G) by Th63;

          then [x, y] in ( the_Edges_of G) & (( the_Target_of G) . [x, y]) = y by GLIB_000:def 14;

          hence z in (G .edgesInto Y) by A2, A3, GLIB_000:def 26;

        end;

        set x = (( the_Source_of G) . z), y = (( the_Target_of G) . z);

        assume z in (G .edgesInto Y);

        then

         A4: z in ( the_Edges_of G) & y in Y by GLIB_000:def 26;

        then z DJoins (x,y,G) by GLIB_000:def 14;

        then

         A5: z = [x, y] by Th64;

        z in E by A4, GLIB_000: 6;

        hence z in (Y |` E) by A4, A5, RELAT_1:def 12;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLUNIR00:76

    

     Th76: for X,Y be set holds ((Y |` E) | X) = (( createGraph (V,E)) .edgesDBetween (X,Y))

    proof

      let X,Y be set;

      

      thus ((Y |` E) | X) = ((Y |` E) /\ (E | X)) by GLIBPRE0: 9

      .= ((( createGraph (V,E)) .edgesInto Y) /\ (E | X)) by Th75

      .= ((( createGraph (V,E)) .edgesInto Y) /\ (( createGraph (V,E)) .edgesOutOf X)) by Th74

      .= (( createGraph (V,E)) .edgesDBetween (X,Y)) by GLIBPRE0: 30;

    end;

    theorem :: GLUNIR00:77

    

     Th77: for X,Y be set holds (((Y |` E) | X) \/ ((X |` E) | Y)) = (( createGraph (V,E)) .edgesBetween (X,Y))

    proof

      let X,Y be set;

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

      

      thus (((Y |` E) | X) \/ ((X |` E) | Y)) = (((Y |` E) | X) \/ (G .edgesDBetween (Y,X))) by Th76

      .= ((G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X))) by Th76

      .= (G .edgesBetween (X,Y)) by GLIBPRE0: 28;

    end;

    theorem :: GLUNIR00:78

    

     Th78: for v be Vertex of ( createGraph (V,E)) holds (E | {v}) = (v .edgesOut() )

    proof

      let v be Vertex of ( createGraph (V,E));

      

      thus (E | {v}) = (( createGraph (V,E)) .edgesOutOf {v}) by Th74

      .= (v .edgesOut() ) by GLIB_000:def 39;

    end;

    theorem :: GLUNIR00:79

    

     Th79: for v be Vertex of ( createGraph (V,E)) holds ( {v} |` E) = (v .edgesIn() )

    proof

      let v be Vertex of ( createGraph (V,E));

      

      thus ( {v} |` E) = (( createGraph (V,E)) .edgesInto {v}) by Th75

      .= (v .edgesIn() ) by GLIB_000:def 38;

    end;

    theorem :: GLUNIR00:80

    

     Th80: for X be set holds ((E | X) \/ (X |` E)) = (( createGraph (V,E)) .edgesInOut X)

    proof

      let X be set;

      

      thus ((E | X) \/ (X |` E)) = ((( createGraph (V,E)) .edgesOutOf X) \/ (X |` E)) by Th74

      .= ((( createGraph (V,E)) .edgesOutOf X) \/ (( createGraph (V,E)) .edgesInto X)) by Th75

      .= (( createGraph (V,E)) .edgesInOut X) by GLIB_000:def 28;

    end;

    theorem :: GLUNIR00:81

    ( dom E) = ( rng ( the_Source_of ( createGraph (V,E))))

    proof

      now

        let v be object;

        hereby

          assume v in ( dom E);

          then

          consider w be object such that

           A1: [v, w] in E by XTUPLE_0:def 12;

           [v, w] DJoins (v,w,( createGraph (V,E))) by A1, Th63;

          then

           A2: [v, w] in ( the_Edges_of ( createGraph (V,E))) & (( the_Source_of ( createGraph (V,E))) . [v, w]) = v by GLIB_000:def 14;

          then [v, w] in ( dom ( the_Source_of ( createGraph (V,E)))) by FUNCT_2:def 1;

          hence v in ( rng ( the_Source_of ( createGraph (V,E)))) by A2, FUNCT_1: 3;

        end;

        assume v in ( rng ( the_Source_of ( createGraph (V,E))));

        then

        consider e be object such that

         A3: e in ( dom ( the_Source_of ( createGraph (V,E)))) & (( the_Source_of ( createGraph (V,E))) . e) = v by FUNCT_1:def 3;

        

         A4: e in ( the_Edges_of ( createGraph (V,E))) by A3;

        set w = (( the_Target_of ( createGraph (V,E))) . e);

        e DJoins (v,w,( createGraph (V,E))) by A3, GLIB_000:def 14;

        then

         A5: e = [v, w] by Th64;

        e in E by A4, GLIB_000: 6;

        hence v in ( dom E) by A5, XTUPLE_0:def 12;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLUNIR00:82

    ( rng E) = ( rng ( the_Target_of ( createGraph (V,E))))

    proof

      now

        let w be object;

        hereby

          assume w in ( rng E);

          then

          consider v be object such that

           A1: [v, w] in E by XTUPLE_0:def 13;

           [v, w] DJoins (v,w,( createGraph (V,E))) by A1, Th63;

          then

           A2: [v, w] in ( the_Edges_of ( createGraph (V,E))) & (( the_Target_of ( createGraph (V,E))) . [v, w]) = w by GLIB_000:def 14;

          then [v, w] in ( dom ( the_Target_of ( createGraph (V,E)))) by FUNCT_2:def 1;

          hence w in ( rng ( the_Target_of ( createGraph (V,E)))) by A2, FUNCT_1: 3;

        end;

        assume w in ( rng ( the_Target_of ( createGraph (V,E))));

        then

        consider e be object such that

         A3: e in ( dom ( the_Target_of ( createGraph (V,E)))) & (( the_Target_of ( createGraph (V,E))) . e) = w by FUNCT_1:def 3;

        

         A4: e in ( the_Edges_of ( createGraph (V,E))) by A3;

        set v = (( the_Source_of ( createGraph (V,E))) . e);

        e DJoins (v,w,( createGraph (V,E))) by A3, GLIB_000:def 14;

        then

         A5: e = [v, w] by Th64;

        e in E by A4, GLIB_000: 6;

        hence w in ( rng E) by A5, XTUPLE_0:def 13;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GLUNIR00:83

    

     Th83: for v be Vertex of ( createGraph (V,E)) holds v is isolated iff not v in ( field E)

    proof

      let v be Vertex of ( createGraph (V,E));

      hereby

        assume

         A1: v is isolated;

        assume v in ( field E);

        then v in (( dom E) \/ ( rng E)) by RELAT_1:def 6;

        per cases by XBOOLE_0:def 3;

          suppose v in ( dom E);

          then

          consider w be object such that

           A2: [v, w] in E by XTUPLE_0:def 12;

          thus contradiction by A1, A2, Th63, GLIBPRE0: 22;

        end;

          suppose v in ( rng E);

          then

          consider w be object such that

           A3: [w, v] in E by XTUPLE_0:def 13;

          thus contradiction by A1, A3, Th63, GLIBPRE0: 22;

        end;

      end;

      assume

       A4: not v in ( field E);

      assume not v is isolated;

      then (v .edgesInOut() ) <> {} by GLIB_000:def 49;

      then

      consider e be object such that

       A5: e in (v .edgesInOut() ) by XBOOLE_0:def 1;

      e in ((v .edgesIn() ) \/ (v .edgesOut() )) by A5, GLIB_000: 60;

      per cases by XBOOLE_0:def 3;

        suppose e in (v .edgesIn() );

        then

        consider w be set such that

         A6: e DJoins (w,v,( createGraph (V,E))) by GLIB_000: 57;

        e = [w, v] by A6, Th64;

        then [w, v] in E by A6, Th63;

        hence contradiction by A4, RELAT_1: 15;

      end;

        suppose e in (v .edgesOut() );

        then

        consider w be set such that

         A7: e DJoins (v,w,( createGraph (V,E))) by GLIB_000: 59;

        e = [v, w] by A7, Th64;

        then [v, w] in E by A7, Th63;

        hence contradiction by A4, RELAT_1: 15;

      end;

    end;

    theorem :: GLUNIR00:84

    E is symmetric iff ( VertexAdjSymRel ( createGraph (V,E))) = E

    proof

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

      hereby

        assume E is symmetric;

        then

         A1: E = (E ~ ) by RELAT_2: 13;

        

        thus ( VertexAdjSymRel G) = (E \/ (( VertexDomRel G) ~ )) by Th65

        .= (E \/ (E ~ )) by Th65

        .= E by A1;

      end;

      assume ( VertexAdjSymRel G) = E;

      

      then E = (E \/ (( VertexDomRel G) ~ )) by Th65

      .= (E \/ (E ~ )) by Th65;

      then

       A2: (E ~ ) c= E by XBOOLE_1: 7;

      then ((E ~ ) ~ ) c= (E ~ ) by SYSREL: 11;

      hence thesis by A2, XBOOLE_0:def 10, RELAT_2: 13;

    end;

    theorem :: GLUNIR00:85

    for V1 be non empty set, V2 be non empty Subset of V1 holds for E1 be Relation of V1, E2 be Relation of V2 st E2 c= E1 holds ( createGraph (V2,E2)) is inducedSubgraph of ( createGraph (V1,E1)), V2, E2

    proof

      let V1 be non empty set, V2 be non empty Subset of V1;

      let E1 be Relation of V1, E2 be Relation of V2;

      assume

       A1: E2 c= E1;

      set G1 = ( createGraph (V1,E1)), G2 = ( createGraph (V2,E2));

      

       A2: ( the_Vertices_of G2) = V2 & ( the_Edges_of G2) = E2 by GLIB_000: 6;

      

       A3: V2 is non empty Subset of ( the_Vertices_of G1) by GLIB_000: 6;

      now

        let e be object;

        set v = (( the_Source_of G2) . e), w = (( the_Target_of G2) . e);

        assume

         A4: e in E2;

        then e in ( the_Edges_of G2) by GLIB_000: 6;

        then

         A5: e DJoins (v,w,G2) by GLIB_000:def 14;

        then e Joins (v,w,G2) by GLIB_000: 16;

        then v in ( the_Vertices_of G2) & w in ( the_Vertices_of G2) by GLIB_000: 13;

        then

         A6: v in V2 & w in V2 by GLIB_000: 6;

        e = [v, w] by A5, Th64;

        then e DJoins (v,w,G1) by A1, A4, Th63;

        then e in ( the_Edges_of G1) & (( the_Source_of G1) . e) = v & (( the_Target_of G1) . e) = w by GLIB_000:def 14;

        hence e in (G1 .edgesBetween V2) by A6, GLIB_000: 31;

      end;

      then

       A7: E2 c= (G1 .edgesBetween V2) by TARSKI:def 3;

      G2 is Subgraph of G1

      proof

        V2 c= V1;

        then

         A8: ( the_Vertices_of G2) c= ( the_Vertices_of G1) by A2, GLIB_000: 6;

        

         A9: ( the_Edges_of G2) c= ( the_Edges_of G1) by A1, A2, GLIB_000: 6;

        now

          let e be set;

          assume

           A10: e in ( the_Edges_of G2);

          set v = (( the_Source_of G2) . e), w = (( the_Target_of G2) . e);

          e DJoins (v,w,G2) by A10, GLIB_000:def 14;

          then

           A11: e = [v, w] by Th64;

          e in E2 by A10, GLIB_000: 6;

          then e DJoins (v,w,G1) by A1, A11, Th63;

          hence v = (( the_Source_of G1) . e) & w = (( the_Target_of G1) . e) by GLIB_000:def 14;

        end;

        hence thesis by A8, A9, GLIB_000:def 32;

      end;

      hence thesis by A2, A3, A7, GLIB_000:def 37;

    end;

    theorem :: GLUNIR00:86

    

     Th86: for G be non-Dmulti _Graph holds ex F be PGraphMapping of G, ( createGraph (( the_Vertices_of G),( VertexDomRel G))) st F is Disomorphism & (F _V ) = ( id ( the_Vertices_of G)) & for e be object st e in ( the_Edges_of G) holds ((F _E ) . e) = [(( the_Source_of G) . e), (( the_Target_of G) . e)]

    proof

      let G be non-Dmulti _Graph;

      set G9 = ( createGraph (( the_Vertices_of G),( VertexDomRel G)));

      reconsider f = ( id ( the_Vertices_of G)) as PartFunc of ( the_Vertices_of G), ( the_Vertices_of G9) by GLIB_000: 6;

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

      consider g be Function such that

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

       A2: for x be object st x in ( the_Edges_of G) holds (g . x) = G(x) from FUNCT_1:sch 3;

      now

        let y be object;

        hereby

          assume y in ( rng g);

          then

          consider x be object such that

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

          

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

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

          then y in ( VertexDomRel G) by A4, Th1;

          hence y in ( the_Edges_of G9) by GLIB_000: 6;

        end;

        assume y in ( the_Edges_of G9);

        then

         A5: y in ( VertexDomRel G) by GLIB_000: 6;

        then

        consider v,w be object such that

         A6: y = [v, w] by RELAT_1:def 1;

        consider e be object such that

         A7: e DJoins (v,w,G) by A5, A6, Th1;

        

         A8: e in ( the_Edges_of G) & (( the_Source_of G) . e) = v & (( the_Target_of G) . e) = w by A7, GLIB_000:def 14;

        then (g . e) = y by A2, A6;

        hence y in ( rng g) by A1, A8, FUNCT_1: 3;

      end;

      then

       A9: ( rng g) = ( the_Edges_of G9) by TARSKI: 2;

      then

      reconsider g as PartFunc of ( the_Edges_of G), ( the_Edges_of G9) by A1, RELSET_1: 4;

      now

        thus for e be object st e in ( dom g) holds (( the_Source_of G) . e) in ( dom f) & (( the_Target_of G) . e) in ( dom f) by FUNCT_2: 5;

        let e,v,w be object;

        assume

         A10: e in ( dom g) & v in ( dom f) & w in ( dom f) & e DJoins (v,w,G);

        then

         A11: (( the_Source_of G) . e) = v & (( the_Target_of G) . e) = w by GLIB_000:def 14;

        

         A12: (g . e) = [v, w] by A2, A10, A11;

        (g . e) in ( rng g) by A10, FUNCT_1: 3;

        then (g . e) in ( the_Edges_of G9);

        then (g . e) in ( VertexDomRel G) by GLIB_000: 6;

        then (g . e) DJoins (v,w,G9) by A12, Th63;

        then (g . e) DJoins ((f . v),w,G9) by A10, FUNCT_1: 18;

        hence (g . e) DJoins ((f . v),(f . w),G9) by A10, FUNCT_1: 18;

      end;

      then

      reconsider F = [f, g] as directed PGraphMapping of G, G9 by GLIB_010: 30;

      take F;

      now

        let x1,x2 be object;

        assume

         A13: x1 in ( dom g) & x2 in ( dom g) & (g . x1) = (g . x2);

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

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

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

        hence x1 = x2 by GLIB_000:def 21;

      end;

      then

       A14: g is one-to-one by FUNCT_1:def 4;

      f is one-to-one & (F _V ) = f & (F _E ) = g;

      then

       A15: F is one-to-one by A14, GLIB_010:def 13;

      

       A16: ( dom f) = ( the_Vertices_of G) & ( rng f) = ( the_Vertices_of G9) by GLIB_000: 6;

      (F _V ) = f & (F _E ) = g;

      then

       A17: F is total onto by A1, A9, A16, GLIB_010:def 11, GLIB_010:def 12;

      thus F is Disomorphism by A15, A17;

      thus (F _V ) = ( id ( the_Vertices_of G));

      let e be object;

      assume e in ( the_Edges_of G);

      hence ((F _E ) . e) = [(( the_Source_of G) . e), (( the_Target_of G) . e)] by A2;

    end;

    theorem :: GLUNIR00:87

    for G be non-Dmulti _Graph holds ( createGraph (( the_Vertices_of G),( VertexDomRel G))) is G -Disomorphic

    proof

      let G be non-Dmulti _Graph;

      set G9 = ( createGraph (( the_Vertices_of G),( VertexDomRel G)));

      consider F be PGraphMapping of G, G9 such that

       A1: F is Disomorphism and (F _V ) = ( id ( the_Vertices_of G)) & for e be object st e in ( the_Edges_of G) holds ((F _E ) . e) = [(( the_Source_of G) . e), (( the_Target_of G) . e)] by Th86;

      thus thesis by A1, GLIB_010:def 24;

    end;

    begin

    reserve E for symmetric Relation of V;

    definition

      let V, E;

      mode GraphFromSymRel of V,E is removeParallelEdges of ( createGraph (V,E));

    end

    reserve G for GraphFromSymRel of V, E;

    theorem :: GLUNIR00:88

    

     Th88: for v,w be object holds [v, w] in E iff [v, w] DJoins (v,w,G) or [w, v] DJoins (w,v,G)

    proof

      let v,w be object;

      

       A1: v is set & w is set by TARSKI: 1;

      set G0 = ( createGraph (V,E));

      consider E0 be RepEdgeSelection of G0 such that

       A2: G is inducedSubgraph of G0, ( the_Vertices_of G0), E0 by GLIB_009:def 7;

      hereby

        assume [v, w] in E;

        then

         A3: [v, w] DJoins (v,w,G0) & [w, v] DJoins (w,v,G0) by Th63, GLIBPRE0: 13;

         [v, w] Joins (v,w,G0) by A3, GLIB_000: 16;

        then

        consider e be object such that

         A4: e Joins (v,w,G0) & e in E0 and for e9 be object st e9 Joins (v,w,G0) & e9 in E0 holds e9 = e by GLIB_009:def 5;

        e in ( the_Edges_of G0) by A4;

        then

         A5: e in E by GLIB_000: 6;

        then

        consider v0,w0 be object such that

         A6: e = [v0, w0] by RELAT_1:def 1;

        

         A7: e DJoins (v0,w0,G0) by A5, A6, Th63;

        

         A8: ( the_Edges_of G0) = (G0 .edgesBetween ( the_Vertices_of G0)) by GLIB_000: 34;

        ( the_Vertices_of G0) c= ( the_Vertices_of G0);

        then

         A9: E0 = ( the_Edges_of G) by A2, A8, GLIB_000:def 37;

        e is set & v0 is set & w0 is set by TARSKI: 1;

        then

         A10: e DJoins (v0,w0,G) by A4, A7, A9, GLIB_000: 73;

        e Joins (v0,w0,G0) by A7, GLIB_000: 16;

        per cases by A4, GLIB_000: 15;

          suppose v = v0 & w = w0;

          hence [v, w] DJoins (v,w,G) or [w, v] DJoins (w,v,G) by A6, A10;

        end;

          suppose v = w0 & w = v0;

          hence [v, w] DJoins (v,w,G) or [w, v] DJoins (w,v,G) by A6, A10;

        end;

      end;

      assume [v, w] DJoins (v,w,G) or [w, v] DJoins (w,v,G);

      per cases ;

        suppose [v, w] DJoins (v,w,G);

        hence [v, w] in E by A1, Th63, GLIB_000: 72;

      end;

        suppose [w, v] DJoins (w,v,G);

        then [w, v] DJoins (w,v,G0) by A1, GLIB_000: 72;

        hence [v, w] in E by Th63, GLIBPRE0: 13;

      end;

    end;

    theorem :: GLUNIR00:89

    

     Th89: for v,w be Vertex of G holds [v, w] in E iff (v,w) are_adjacent

    proof

      let v,w be Vertex of G;

      hereby

        assume [v, w] in E;

        per cases by Th88;

          suppose [v, w] DJoins (v,w,G);

          then [v, w] Joins (v,w,G) by GLIB_000: 16;

          hence (v,w) are_adjacent by CHORD:def 3;

        end;

          suppose [w, v] DJoins (w,v,G);

          then [w, v] Joins (v,w,G) by GLIB_000: 16;

          hence (v,w) are_adjacent by CHORD:def 3;

        end;

      end;

      set G0 = ( createGraph (V,E));

      consider E0 be RepEdgeSelection of G0 such that

       A1: G is inducedSubgraph of G0, ( the_Vertices_of G0), E0 by GLIB_009:def 7;

      

       A2: ( the_Edges_of G0) = (G0 .edgesBetween ( the_Vertices_of G0)) by GLIB_000: 34;

      ( the_Vertices_of G0) c= ( the_Vertices_of G0);

      then

       A3: ( the_Edges_of G) = E0 by A1, A2, GLIB_000:def 37;

      assume (v,w) are_adjacent ;

      then

      consider e be object such that

       A4: e Joins (v,w,G) by CHORD:def 3;

      e in E0 by A3, A4, GLIB_000:def 13;

      then e in ( the_Edges_of G0);

      then

       A5: e in E by GLIB_000: 6;

      then

      consider v0,w0 be object such that

       A6: e = [v0, w0] by RELAT_1:def 1;

      e DJoins (v0,w0,G0) by A5, A6, Th63;

      then

       A7: e Joins (v0,w0,G0) by GLIB_000: 16;

      e Joins (v,w,G0) by A4, GLIB_000: 72;

      per cases by A7, GLIB_000: 15;

        suppose v = v0 & w = w0;

        hence [v, w] in E by A5, A6;

      end;

        suppose v = w0 & w = v0;

        hence [v, w] in E by A5, A6, GLIBPRE0: 13;

      end;

    end;

    registration

      let V, E;

      cluster -> non-multi for GraphFromSymRel of V, E;

      coherence ;

    end

    theorem :: GLUNIR00:90

    

     Th90: ( the_Edges_of G) c= E

    proof

      set G0 = ( createGraph (V,E));

      ( the_Edges_of G) c= ( the_Edges_of G0);

      hence thesis by GLIB_000: 6;

    end;

    theorem :: GLUNIR00:91

    for G1,G2 be GraphFromSymRel of V, E holds ( the_Vertices_of G1) = ( the_Vertices_of G2)

    proof

      let G1,G2 be GraphFromSymRel of V, E;

      set G0 = ( createGraph (V,E));

      ( the_Vertices_of G1) = ( the_Vertices_of G0) & ( the_Vertices_of G2) = ( the_Vertices_of G0) by GLIB_000:def 33;

      hence thesis;

    end;

    theorem :: GLUNIR00:92

    for G1,G2 be GraphFromSymRel of V, E holds G2 is G1 -isomorphic by GLIB_010: 169;

    theorem :: GLUNIR00:93

    V is trivial iff G is _trivial;

    registration

      let V be trivial non empty set;

      let E be symmetric Relation of V;

      cluster -> _trivial for GraphFromSymRel of V, E;

      coherence ;

    end

    registration

      let V be non trivial set;

      let E be symmetric Relation of V;

      cluster -> non _trivial for GraphFromSymRel of V, E;

      coherence ;

    end

    theorem :: GLUNIR00:94

    E is irreflexive iff G is loopless;

    registration

      let V;

      let E be symmetric irreflexive Relation of V;

      cluster -> loopless for GraphFromSymRel of V, E;

      coherence ;

    end

    registration

      let V;

      let E be symmetric non irreflexive Relation of V;

      cluster -> non loopless for GraphFromSymRel of V, E;

      coherence ;

    end

    theorem :: GLUNIR00:95

    G is complete implies E is connected

    proof

      assume G is complete;

      then ( createGraph (V,E)) is complete;

      hence E is connected by Th69;

    end;

    registration

      let V be non trivial set;

      let E be symmetric non connected Relation of V;

      cluster -> non complete for GraphFromSymRel of V, E;

      coherence ;

    end

    theorem :: GLUNIR00:96

    E is empty iff G is edgeless;

    registration

      let V;

      let E be empty Relation of V;

      cluster -> edgeless for GraphFromSymRel of V, E;

      coherence ;

    end

    registration

      let V;

      let E be symmetric non empty Relation of V;

      cluster -> non edgeless for GraphFromSymRel of V, E;

      coherence ;

    end

    theorem :: GLUNIR00:97

    E is total reflexive iff G is loopfull

    proof

      thus E is total reflexive implies G is loopfull;

      assume G is loopfull;

      then ( createGraph (V,E)) is loopfull;

      hence E is total reflexive by Th71;

    end;

    registration

      let V;

      let E be total reflexive symmetric Relation of V;

      cluster -> loopfull for GraphFromSymRel of V, E;

      coherence ;

    end

    registration

      let V;

      let E be symmetric non total Relation of V;

      cluster -> non loopfull for GraphFromSymRel of V, E;

      coherence ;

    end

    registration

      let V be finite non empty set, E be symmetric Relation of V;

      cluster -> finite for GraphFromSymRel of V, E;

      coherence ;

    end

    theorem :: GLUNIR00:98

    for v be Vertex of G holds ( Im (E,v)) = (v .allNeighbors() )

    proof

      let v be Vertex of G;

      set G0 = ( createGraph (V,E));

      consider E0 be RepEdgeSelection of G0 such that

       A1: G is inducedSubgraph of G0, ( the_Vertices_of G0), E0 by GLIB_009:def 7;

      

       A2: ( the_Edges_of G0) = (G0 .edgesBetween ( the_Vertices_of G0)) by GLIB_000: 34;

      ( the_Vertices_of G0) c= ( the_Vertices_of G0);

      then

      reconsider v0 = v as Vertex of G0 by A1, A2, GLIB_000:def 37;

      

      thus ( Im (E,v)) = (( Im (E,v)) \/ ( Im (E,v)))

      .= (( Im (E,v)) \/ ( Coim (E,v))) by GLIBPRE0: 10

      .= ((v0 .outNeighbors() ) \/ ( Coim (E,v))) by Th72

      .= ((v0 .outNeighbors() ) \/ (v0 .inNeighbors() )) by Th73

      .= (v0 .allNeighbors() ) by GLIB_000:def 48

      .= (v .allNeighbors() ) by GLIBPRE0: 66;

    end;

    theorem :: GLUNIR00:99

    for X be set holds (G .edgesInOut X) c= ((E | X) \/ (X |` E))

    proof

      let X be set;

      ((E | X) \/ (X |` E)) = (( createGraph (V,E)) .edgesInOut X) by Th80;

      hence thesis by GLIB_000: 76;

    end;

    theorem :: GLUNIR00:100

    for X,Y be set holds (G .edgesBetween (X,Y)) c= (((Y |` E) | X) \/ ((X |` E) | Y))

    proof

      let X,Y be set;

      (((Y |` E) | X) \/ ((X |` E) | Y)) = (( createGraph (V,E)) .edgesBetween (X,Y)) by Th77;

      hence thesis by GLIB_000: 77;

    end;

    theorem :: GLUNIR00:101

    for v be Vertex of G holds (v .edgesOut() ) c= (E | {v})

    proof

      let v be Vertex of G;

      set G0 = ( createGraph (V,E));

      consider E0 be RepEdgeSelection of G0 such that

       A1: G is inducedSubgraph of G0, ( the_Vertices_of G0), E0 by GLIB_009:def 7;

      

       A2: ( the_Edges_of G0) = (G0 .edgesBetween ( the_Vertices_of G0)) by GLIB_000: 34;

      ( the_Vertices_of G0) c= ( the_Vertices_of G0);

      then

      reconsider v0 = v as Vertex of G0 by A1, A2, GLIB_000:def 37;

      (v0 .edgesOut() ) = (E | {v}) by Th78;

      hence thesis by GLIB_000: 78;

    end;

    theorem :: GLUNIR00:102

    for v be Vertex of G holds (v .edgesIn() ) c= ( {v} |` E)

    proof

      let v be Vertex of G;

      set G0 = ( createGraph (V,E));

      consider E0 be RepEdgeSelection of G0 such that

       A1: G is inducedSubgraph of G0, ( the_Vertices_of G0), E0 by GLIB_009:def 7;

      

       A2: ( the_Edges_of G0) = (G0 .edgesBetween ( the_Vertices_of G0)) by GLIB_000: 34;

      ( the_Vertices_of G0) c= ( the_Vertices_of G0);

      then

      reconsider v0 = v as Vertex of G0 by A1, A2, GLIB_000:def 37;

      (v0 .edgesIn() ) = ( {v} |` E) by Th79;

      hence thesis by GLIB_000: 78;

    end;

    theorem :: GLUNIR00:103

    for v be Vertex of G holds v is isolated iff not v in ( field E)

    proof

      let v be Vertex of G;

      set G0 = ( createGraph (V,E));

      consider E0 be RepEdgeSelection of G0 such that

       A1: G is inducedSubgraph of G0, ( the_Vertices_of G0), E0 by GLIB_009:def 7;

      

       A2: ( the_Edges_of G0) = (G0 .edgesBetween ( the_Vertices_of G0)) by GLIB_000: 34;

      ( the_Vertices_of G0) c= ( the_Vertices_of G0);

      then

      reconsider v0 = v as Vertex of G0 by A1, A2, GLIB_000:def 37;

      v is isolated iff v0 is isolated by GLIB_009: 111;

      hence thesis by Th83;

    end;

    theorem :: GLUNIR00:104

    for G be GraphFromSymRel of V, E holds ( VertexAdjSymRel G) = E

    proof

      let G be GraphFromSymRel of V, E;

      now

        let x,y be object;

        hereby

          assume

           A1: [x, y] in ( VertexAdjSymRel G);

          then

          reconsider v = x, w = y as Vertex of G by ZFMISC_1: 87;

          (v,w) are_adjacent by A1, Th33;

          hence [x, y] in E by Th89;

        end;

        set G0 = ( createGraph (V,E));

        consider E0 be RepEdgeSelection of G0 such that

         A2: G is inducedSubgraph of G0, ( the_Vertices_of G0), E0 by GLIB_009:def 7;

        

         A3: ( the_Edges_of G0) = (G0 .edgesBetween ( the_Vertices_of G0)) by GLIB_000: 34;

        ( the_Vertices_of G0) c= ( the_Vertices_of G0);

        

        then

         A4: ( the_Vertices_of G) = ( the_Vertices_of G0) by A2, A3, GLIB_000:def 37

        .= V by GLIB_000: 6;

        assume

         A5: [x, y] in E;

        then

        reconsider v = x, w = y as Vertex of G by A4, ZFMISC_1: 87;

        (v,w) are_adjacent by A5, Th89;

        hence [x, y] in ( VertexAdjSymRel G) by Th33;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    theorem :: GLUNIR00:105

    for V1 be non empty set, V2 be non empty Subset of V1 holds for E1 be symmetric Relation of V1 holds for E2 be symmetric Relation of V2 holds for G1 be GraphFromSymRel of V1, E1, G2 be GraphFromSymRel of V2, E2 st E2 c= E1 holds ex F be PGraphMapping of G2, G1 st F is weak_SG-embedding & (F _V ) = ( id V2) & for v,w be object st [v, w] in ( the_Edges_of G2) holds ((F _E ) . [v, w]) = [v, w] or ((F _E ) . [v, w]) = [w, v]

    proof

      let V1 be non empty set, V2 be non empty Subset of V1;

      let E1 be symmetric Relation of V1;

      let E2 be symmetric Relation of V2;

      let G1 be GraphFromSymRel of V1, E1, G2 be GraphFromSymRel of V2, E2;

      assume

       A1: E2 c= E1;

      set G3 = ( createGraph (V1,E1)), G4 = ( createGraph (V2,E2));

      set f = ( id V2);

      ( the_Vertices_of G1) = ( the_Vertices_of G3) & ( the_Vertices_of G2) = ( the_Vertices_of G4) by GLIB_000:def 33;

      then

       A2: ( the_Vertices_of G1) = V1 & ( the_Vertices_of G2) = V2 by GLIB_000: 6;

      then ( dom ( id V2)) = ( the_Vertices_of G2) & ( rng ( id V2)) c= ( the_Vertices_of G1);

      then

      reconsider f as PartFunc of ( the_Vertices_of G2), ( the_Vertices_of G1) by RELSET_1: 4;

      defpred P[ object, object] means ex v,w be object st $1 = [v, w] & $2 in ( the_Edges_of G1) & ($2 = [v, w] or $2 = [w, v]);

      

       A3: for x,y1,y2 be object st x in ( the_Edges_of G2) & P[x, y1] & P[x, y2] holds y1 = y2

      proof

        let x,y1,y2 be object;

        assume

         A4: x in ( the_Edges_of G2) & P[x, y1] & P[x, y2];

        then

        consider v,w be object such that

         A5: x = [v, w] & y1 in ( the_Edges_of G1) & (y1 = [v, w] or y1 = [w, v]);

        consider v0,w0 be object such that

         A6: x = [v0, w0] & y2 in ( the_Edges_of G1) & (y2 = [v0, w0] or y2 = [w0, v0]) by A4;

        

         A7: v = v0 & w = w0 by A5, A6, XTUPLE_0: 1;

        per cases by A5, A6, A7;

          suppose y1 = [v, w] & y2 = [v, w];

          hence thesis;

        end;

          suppose

           A8: y1 = [v, w] & y2 = [w, v];

          y1 in E1 & y2 in E1 by A5, A6, Th90, TARSKI:def 3;

          then

           A9: y1 DJoins (v,w,G3) & y2 DJoins (w,v,G3) by A8, Th63;

          G3 is Supergraph of G1 by GLIB_006: 57;

          then y1 DJoins (v,w,G1) & y2 DJoins (w,v,G1) by A5, A6, A9, GLIB_006: 71;

          then y1 Joins (v,w,G1) & y2 Joins (v,w,G1) by GLIB_000: 16;

          hence thesis by GLIB_000:def 20;

        end;

          suppose

           A10: y1 = [w, v] & y2 = [v, w];

          y1 in E1 & y2 in E1 by A5, A6, Th90, TARSKI:def 3;

          then

           A11: y1 DJoins (w,v,G3) & y2 DJoins (v,w,G3) by A10, Th63;

          G3 is Supergraph of G1 by GLIB_006: 57;

          then y1 DJoins (w,v,G1) & y2 DJoins (v,w,G1) by A5, A6, A11, GLIB_006: 71;

          then y1 Joins (v,w,G1) & y2 Joins (v,w,G1) by GLIB_000: 16;

          hence thesis by GLIB_000:def 20;

        end;

          suppose y1 = [w, v] & y2 = [w, v];

          hence thesis;

        end;

      end;

      

       A12: for x be object st x in ( the_Edges_of G2) holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in ( the_Edges_of G2);

        then

         A13: x in E2 by Th90, TARSKI:def 3;

        then

        consider v,w be object such that

         A14: x = [v, w] by RELAT_1:def 1;

        per cases by A1, A13, A14, Th88;

          suppose

           A15: [v, w] DJoins (v,w,G1);

          take [v, w], v, w;

          thus thesis by A14, A15, GLIB_000:def 14;

        end;

          suppose

           A16: [w, v] DJoins (w,v,G1);

          take [w, v], v, w;

          thus thesis by A14, A16, GLIB_000:def 14;

        end;

      end;

      consider g be Function such that

       A17: ( dom g) = ( the_Edges_of G2) and

       A18: for x be object st x in ( the_Edges_of G2) holds P[x, (g . x)] from FUNCT_1:sch 2( A3, A12);

      now

        let y be object;

        assume y in ( rng g);

        then

        consider x be object such that

         A19: x in ( dom g) & (g . x) = y by FUNCT_1:def 3;

        consider v,w be object such that

         A20: x = [v, w] & y in ( the_Edges_of G1) & (y = [v, w] or y = [w, v]) by A17, A18, A19;

        thus y in ( the_Edges_of G1) by A20;

      end;

      then ( rng g) c= ( the_Edges_of G1) by TARSKI:def 3;

      then

      reconsider g as PartFunc of ( the_Edges_of G2), ( the_Edges_of G1) by A17, RELSET_1: 4;

      now

        hereby

          let e be object;

          assume e in ( dom g);

          then e Joins ((( the_Source_of G2) . e),(( the_Target_of G2) . e),G2) by GLIB_000:def 13;

          hence (( the_Source_of G2) . e) in ( dom f) & (( the_Target_of G2) . e) in ( dom f) by A2, GLIB_000: 13;

        end;

        let e,v,w be object;

        assume

         A21: e in ( dom g) & v in ( dom f) & w in ( dom f);

        assume

         A22: e Joins (v,w,G2);

        consider v0,w0 be object such that

         A23: e = [v0, w0] & (g . e) in ( the_Edges_of G1) and

         A24: (g . e) = [v0, w0] or (g . e) = [w0, v0] by A18, A21;

        e in E2 by A21, Th90, TARSKI:def 3;

        then e DJoins (v0,w0,G4) by A23, Th63;

        then

         A25: e Joins (v0,w0,G4) by GLIB_000: 16;

        

         A26: e in ( the_Edges_of G2) & e is set & v is set & w is set by A21;

        then e Joins (v,w,G4) by A22, GLIB_000: 72;

        then v = v0 & w = w0 or v = w0 & w = v0 by A25, GLIB_000: 15;

        per cases by A24;

          suppose

           A27: (g . e) = [v, w];

          (g . e) in E1 by A23, Th90, TARSKI:def 3;

          then (g . e) DJoins (v,w,G3) by A27, Th63;

          then (g . e) DJoins (v,w,G1) by A23, A26, GLIB_000: 73;

          then (g . e) Joins (v,w,G1) by GLIB_000: 16;

          then (g . e) Joins (v,(f . w),G1) by A21, FUNCT_1: 18;

          hence (g . e) Joins ((f . v),(f . w),G1) by A21, FUNCT_1: 18;

        end;

          suppose

           A28: (g . e) = [w, v];

          (g . e) in E1 by A23, Th90, TARSKI:def 3;

          then (g . e) DJoins (w,v,G3) by A28, Th63;

          then (g . e) DJoins (w,v,G1) by A23, A26, GLIB_000: 73;

          then (g . e) Joins (v,w,G1) by GLIB_000: 16;

          then (g . e) Joins (v,(f . w),G1) by A21, FUNCT_1: 18;

          hence (g . e) Joins ((f . v),(f . w),G1) by A21, FUNCT_1: 18;

        end;

      end;

      then

      reconsider F = [f, g] as PGraphMapping of G2, G1 by GLIB_010: 8;

      take F;

      for x1,x2 be object st x1 in ( dom g) & x2 in ( dom g) & (g . x1) = (g . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A29: x1 in ( dom g) & x2 in ( dom g) & (g . x1) = (g . x2);

        then

        consider v1,w1 be object such that

         A30: x1 = [v1, w1] & (g . x1) in ( the_Edges_of G1) and

         A31: (g . x1) = [v1, w1] or (g . x1) = [w1, v1] by A18;

        consider v2,w2 be object such that

         A32: x2 = [v2, w2] & (g . x2) in ( the_Edges_of G1) and

         A33: (g . x2) = [v2, w2] or (g . x2) = [w2, v2] by A18, A29;

        per cases by A31, A33;

          suppose (g . x1) = [v1, w1] & (g . x2) = [v2, w2] or (g . x1) = [w1, v1] & (g . x2) = [w2, v2];

          then v1 = v2 & w1 = w2 by A29, XTUPLE_0: 1;

          hence thesis by A30, A32;

        end;

          suppose (g . x1) = [v1, w1] & (g . x2) = [w2, v2] or (g . x1) = [w1, v1] & (g . x2) = [v2, w2];

          then

           A34: v1 = w2 & w1 = v2 by A29, XTUPLE_0: 1;

          x1 in E2 & x2 in E2 by A29, Th90, TARSKI:def 3;

          then

           A35: x1 DJoins (v1,w1,G4) & x2 DJoins (w1,v1,G4) by A30, A32, A34, Th63;

          x1 in ( the_Edges_of G2) & x2 in ( the_Edges_of G2) & x1 is set & x2 is set & v1 is set & w1 is set by A29, TARSKI: 1;

          then x1 DJoins (v1,w1,G2) & x2 DJoins (w1,v1,G2) by A35, GLIB_000: 73;

          then x1 Joins (v1,w1,G2) & x2 Joins (v1,w1,G2) by GLIB_000: 16;

          hence thesis by GLIB_000:def 20;

        end;

      end;

      then

       A36: (F _E ) is one-to-one by FUNCT_1:def 4;

      (F _V ) is one-to-one;

      then

       A37: F is one-to-one by A36, GLIB_010:def 13;

      ( dom (F _V )) = ( the_Vertices_of G2) & ( dom (F _E )) = ( the_Edges_of G2) by A2, A17;

      then F is total by GLIB_010:def 11;

      hence F is weak_SG-embedding by A37;

      thus (F _V ) = ( id V2);

      let v,w be object;

      assume [v, w] in ( the_Edges_of G2);

      then

      consider v0,w0 be object such that

       A38: [v, w] = [v0, w0] & (g . [v, w]) in ( the_Edges_of G1) and

       A39: (g . [v, w]) = [v0, w0] or (g . [v, w]) = [w0, v0] by A18;

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

      hence ((F _E ) . [v, w]) = [v, w] or ((F _E ) . [v, w]) = [w, v] by A39;

    end;

    theorem :: GLUNIR00:106

    

     Th106: for G1 be non-multi _Graph holds for G2 be GraphFromSymRel of ( the_Vertices_of G1), ( VertexAdjSymRel G1) holds ex F be PGraphMapping of G1, G2 st F is isomorphism & (F _V ) = ( id ( the_Vertices_of G1)) & for e be object st e in ( the_Edges_of G1) holds ((F _E ) . e) = [(( the_Source_of G1) . e), (( the_Target_of G1) . e)] or ((F _E ) . e) = [(( the_Target_of G1) . e), (( the_Source_of G1) . e)]

    proof

      let G be non-multi _Graph;

      set E0 = ( VertexAdjSymRel G), G0 = ( createGraph (( the_Vertices_of G),E0));

      let G9 be GraphFromSymRel of ( the_Vertices_of G), E0;

      ( the_Vertices_of G9) = ( the_Vertices_of G0) by GLIB_000:def 33

      .= ( the_Vertices_of G) by GLIB_000: 6;

      then

      reconsider f = ( id ( the_Vertices_of G)) as PartFunc of ( the_Vertices_of G), ( the_Vertices_of G9);

      consider E9 be RepEdgeSelection of G0 such that

       A1: G9 is inducedSubgraph of G0, ( the_Vertices_of G0), E9 by GLIB_009:def 7;

      ( the_Edges_of G0) = (G0 .edgesBetween ( the_Vertices_of G0)) & ( the_Vertices_of G0) c= ( the_Vertices_of G0) by GLIB_000: 34;

      then

       A2: ( the_Edges_of G9) = E9 by A1, GLIB_000:def 37;

      defpred P[ object, object] means $2 in E9 & ($2 = [(( the_Source_of G) . $1), (( the_Target_of G) . $1)] or $2 = [(( the_Target_of G) . $1), (( the_Source_of G) . $1)]);

      

       A3: for x,y1,y2 be object st x in ( the_Edges_of G) & P[x, y1] & P[x, y2] holds y1 = y2

      proof

        let x,y1,y2 be object;

        assume

         A4: x in ( the_Edges_of G) & P[x, y1] & P[x, y2];

        set v = (( the_Source_of G) . x), w = (( the_Target_of G) . x);

        per cases by A4;

          suppose y1 = [v, w] & y2 = [v, w];

          hence thesis;

        end;

          suppose

           A5: y1 = [v, w] & y2 = [w, v];

          

           A6: y1 in ( the_Edges_of G9) & y2 in ( the_Edges_of G9) by A2, A4;

          then y1 in ( the_Edges_of G0) & y2 in ( the_Edges_of G0);

          then y1 in E0 & y2 in E0 by GLIB_000: 6;

          then y1 DJoins (v,w,G0) & y2 DJoins (w,v,G0) by A5, Th63;

          then

           A7: y1 Joins (v,w,G0) & y2 Joins (v,w,G0) by GLIB_000: 16;

          then

          consider y0 be object such that y0 Joins (v,w,G0) & y0 in E9 and

           A8: for y9 be object st y9 Joins (v,w,G0) & y9 in E9 holds y9 = y0 by GLIB_009:def 5;

          y1 = y0 & y2 = y0 by A2, A6, A7, A8;

          hence thesis;

        end;

          suppose

           A9: y1 = [w, v] & y2 = [v, w];

          

           A10: y1 in ( the_Edges_of G9) & y2 in ( the_Edges_of G9) by A2, A4;

          then y1 in ( the_Edges_of G0) & y2 in ( the_Edges_of G0);

          then y1 in E0 & y2 in E0 by GLIB_000: 6;

          then y1 DJoins (w,v,G0) & y2 DJoins (v,w,G0) by A9, Th63;

          then

           A11: y1 Joins (v,w,G0) & y2 Joins (v,w,G0) by GLIB_000: 16;

          then

          consider y0 be object such that y0 Joins (v,w,G0) & y0 in E9 and

           A12: for y9 be object st y9 Joins (v,w,G0) & y9 in E9 holds y9 = y0 by GLIB_009:def 5;

          y1 = y0 & y2 = y0 by A2, A10, A11, A12;

          hence thesis;

        end;

          suppose y1 = [w, v] & y2 = [w, v];

          hence thesis;

        end;

      end;

      

       A13: for x be object st x in ( the_Edges_of G) holds ex y be object st P[x, y]

      proof

        let x be object;

        assume

         A14: x in ( the_Edges_of G);

        set v = (( the_Source_of G) . x), w = (( the_Target_of G) . x);

        x Joins (v,w,G) & x Joins (w,v,G) by A14, GLIB_000:def 13;

        then

         A15: [v, w] DJoins (v,w,G0) & [w, v] DJoins (w,v,G0) by Th32, Th63;

        then [v, w] Joins (v,w,G0) by GLIB_000: 16;

        then

        consider z be object such that

         A16: z Joins (v,w,G0) & z in E9 and for e9 be object st e9 Joins (v,w,G0) & e9 in E9 holds e9 = z by GLIB_009:def 5;

        take z;

        per cases by A16, GLIB_000: 16;

          suppose z DJoins (v,w,G0);

          hence thesis by A15, A16, GLIB_000:def 21;

        end;

          suppose z DJoins (w,v,G0);

          hence thesis by A15, A16, GLIB_000:def 21;

        end;

      end;

      consider g be Function such that

       A17: ( dom g) = ( the_Edges_of G) and

       A18: for x be object st x in ( the_Edges_of G) holds P[x, (g . x)] from FUNCT_1:sch 2( A3, A13);

      now

        let y be object;

        hereby

          assume y in ( rng g);

          then

          consider x be object such that

           A19: x in ( dom g) & (g . x) = y by FUNCT_1:def 3;

          thus y in ( the_Edges_of G9) by A2, A17, A18, A19;

        end;

        assume

         A20: y in ( the_Edges_of G9);

        set v = (( the_Source_of G9) . y), w = (( the_Target_of G9) . y);

        y DJoins (v,w,G9) by A20, GLIB_000:def 14;

        then

         A21: y DJoins (v,w,G0) by GLIB_000: 72;

        then

         A22: y = [v, w] by Th64;

        then

        consider x be object such that

         A23: x Joins (v,w,G) by A21, Th32, Th63;

        

         A24: x in ( the_Edges_of G) by A23, GLIB_000:def 13;

        per cases by A23, GLIB_000:def 13;

          suppose (( the_Source_of G) . x) = v & (( the_Target_of G) . x) = w;

          then

           A25: P[x, y] by A2, A20, A22;

           P[x, (g . x)] by A18, A24;

          then y = (g . x) by A3, A24, A25;

          hence y in ( rng g) by A17, A24, FUNCT_1: 3;

        end;

          suppose (( the_Source_of G) . x) = w & (( the_Target_of G) . x) = v;

          then

           A26: P[x, y] by A2, A20, A22;

           P[x, (g . x)] by A18, A24;

          then y = (g . x) by A3, A24, A26;

          hence y in ( rng g) by A17, A24, FUNCT_1: 3;

        end;

      end;

      then

       A27: ( rng g) = ( the_Edges_of G9) by TARSKI: 2;

      then

      reconsider g as PartFunc of ( the_Edges_of G), ( the_Edges_of G9) by A17, RELSET_1: 4;

      now

        thus for e be object st e in ( dom g) holds (( the_Source_of G) . e) in ( dom f) & (( the_Target_of G) . e) in ( dom f) by FUNCT_2: 5;

        let e,v,w be object;

        assume

         A28: e in ( dom g) & v in ( dom f) & w in ( dom f) & e Joins (v,w,G);

        then

         A29: e in ( the_Edges_of G);

        per cases by A28, GLIB_000:def 13;

          suppose

           A30: (( the_Source_of G) . e) = v & (( the_Target_of G) . e) = w;

          per cases by A18, A28;

            suppose (g . e) in E9 & (g . e) = [(( the_Source_of G) . e), (( the_Target_of G) . e)];

            then

             A31: (g . e) = [v, w] by A30;

            (g . e) in ( rng g) by A28, FUNCT_1: 3;

            then

             A32: (g . e) in ( the_Edges_of G9);

            e Joins (v,w,G) by A30, A29, GLIB_000:def 13;

            then [v, w] in E0 by Th32;

            then (g . e) DJoins (v,w,G0) & v is set & w is set by A31, Th63, TARSKI: 1;

            then (g . e) DJoins (v,w,G9) by A32, GLIB_000: 73;

            then (g . e) Joins (v,w,G9) by GLIB_000: 16;

            then (g . e) Joins ((f . v),w,G9) by A28, FUNCT_1: 18;

            hence (g . e) Joins ((f . v),(f . w),G9) by A28, FUNCT_1: 18;

          end;

            suppose (g . e) in E9 & (g . e) = [(( the_Target_of G) . e), (( the_Source_of G) . e)];

            then

             A33: (g . e) = [w, v] by A30;

            (g . e) in ( rng g) by A28, FUNCT_1: 3;

            then

             A34: (g . e) in ( the_Edges_of G9);

            e Joins (w,v,G) by A30, A29, GLIB_000:def 13;

            then (g . e) DJoins (w,v,G0) & v is set & w is set by A33, Th63, TARSKI: 1, Th32;

            then (g . e) DJoins (w,v,G9) by A34, GLIB_000: 73;

            then (g . e) Joins (v,w,G9) by GLIB_000: 16;

            then (g . e) Joins ((f . v),w,G9) by A28, FUNCT_1: 18;

            hence (g . e) Joins ((f . v),(f . w),G9) by A28, FUNCT_1: 18;

          end;

        end;

          suppose

           A35: (( the_Source_of G) . e) = w & (( the_Target_of G) . e) = v;

          per cases by A18, A28;

            suppose (g . e) in E9 & (g . e) = [(( the_Source_of G) . e), (( the_Target_of G) . e)];

            then

             A36: (g . e) = [w, v] by A35;

            (g . e) in ( rng g) by A28, FUNCT_1: 3;

            then

             A37: (g . e) in ( the_Edges_of G9);

            e Joins (w,v,G) by A35, A29, GLIB_000:def 13;

            then [w, v] in E0 by Th32;

            then (g . e) DJoins (w,v,G0) & v is set & w is set by A36, Th63, TARSKI: 1;

            then (g . e) DJoins (w,v,G9) by A37, GLIB_000: 73;

            then (g . e) Joins (v,w,G9) by GLIB_000: 16;

            then (g . e) Joins ((f . v),w,G9) by A28, FUNCT_1: 18;

            hence (g . e) Joins ((f . v),(f . w),G9) by A28, FUNCT_1: 18;

          end;

            suppose (g . e) in E9 & (g . e) = [(( the_Target_of G) . e), (( the_Source_of G) . e)];

            then

             A38: (g . e) = [v, w] by A35;

            (g . e) in ( rng g) by A28, FUNCT_1: 3;

            then

             A39: (g . e) in ( the_Edges_of G9);

            e Joins (v,w,G) by A35, A29, GLIB_000:def 13;

            then (g . e) DJoins (v,w,G0) & v is set & w is set by A38, Th63, TARSKI: 1, Th32;

            then (g . e) DJoins (v,w,G9) by A39, GLIB_000: 73;

            then (g . e) Joins (v,w,G9) by GLIB_000: 16;

            then (g . e) Joins ((f . v),w,G9) by A28, FUNCT_1: 18;

            hence (g . e) Joins ((f . v),(f . w),G9) by A28, FUNCT_1: 18;

          end;

        end;

      end;

      then

      reconsider F = [f, g] as PGraphMapping of G, G9 by GLIB_010: 8;

      take F;

      now

        let x1,x2 be object;

        assume

         A40: x1 in ( dom g) & x2 in ( dom g) & (g . x1) = (g . x2);

        per cases by A18, A40;

          suppose (g . x1) = [(( the_Source_of G) . x1), (( the_Target_of G) . x1)] & (g . x2) = [(( the_Source_of G) . x2), (( the_Target_of G) . x2)];

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

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

          hence x1 = x2 by GLIB_000:def 21;

        end;

          suppose (g . x1) = [(( the_Source_of G) . x1), (( the_Target_of G) . x1)] & (g . x2) = [(( the_Target_of G) . x2), (( the_Source_of G) . x2)];

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

          then x1 Joins ((( the_Source_of G) . x1),(( the_Target_of G) . x1),G) & x2 Joins ((( the_Source_of G) . x1),(( the_Target_of G) . x1),G) by A40, GLIB_000:def 13;

          hence x1 = x2 by GLIB_000:def 20;

        end;

          suppose (g . x1) = [(( the_Target_of G) . x1), (( the_Source_of G) . x1)] & (g . x2) = [(( the_Source_of G) . x2), (( the_Target_of G) . x2)];

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

          then x1 Joins ((( the_Source_of G) . x1),(( the_Target_of G) . x1),G) & x2 Joins ((( the_Source_of G) . x1),(( the_Target_of G) . x1),G) by A40, GLIB_000:def 13;

          hence x1 = x2 by GLIB_000:def 20;

        end;

          suppose (g . x1) = [(( the_Target_of G) . x1), (( the_Source_of G) . x1)] & (g . x2) = [(( the_Target_of G) . x2), (( the_Source_of G) . x2)];

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

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

          hence x1 = x2 by GLIB_000:def 21;

        end;

      end;

      then

       A41: g is one-to-one by FUNCT_1:def 4;

      f is one-to-one & (F _V ) = f & (F _E ) = g;

      then

       A42: F is one-to-one by A41, GLIB_010:def 13;

      ( the_Vertices_of G) = ( the_Vertices_of G0) by GLIB_000: 6

      .= ( the_Vertices_of G9) by GLIB_000:def 33;

      then

       A43: ( dom f) = ( the_Vertices_of G) & ( rng f) = ( the_Vertices_of G9);

      (F _V ) = f & (F _E ) = g;

      then

       A44: F is total onto by A17, A27, A43, GLIB_010:def 11, GLIB_010:def 12;

      thus F is isomorphism by A42, A44;

      thus (F _V ) = ( id ( the_Vertices_of G));

      thus thesis by A18;

    end;

    theorem :: GLUNIR00:107

    for G1 be non-multi _Graph holds for G2 be GraphFromSymRel of ( the_Vertices_of G1), ( VertexAdjSymRel G1) holds G2 is G1 -isomorphic

    proof

      let G1 be non-multi _Graph;

      let G2 be GraphFromSymRel of ( the_Vertices_of G1), ( VertexAdjSymRel G1);

      consider F be PGraphMapping of G1, G2 such that

       A1: F is isomorphism and (F _V ) = ( id ( the_Vertices_of G1)) & for e be object st e in ( the_Edges_of G1) holds ((F _E ) . e) = [(( the_Source_of G1) . e), (( the_Target_of G1) . e)] or ((F _E ) . e) = [(( the_Target_of G1) . e), (( the_Source_of G1) . e)] by Th106;

      thus thesis by A1, GLIB_010:def 23;

    end;