:: Unification of Graphs and Relations in {M}izar
:: by Sebastian Koch
::
:: Received May 31, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users


definition
let G be _Graph;
func VertexDomRel G -> Relation of (the_Vertices_of G) equals :: GLUNIR00:def 1
((the_Source_of G) ~) * (the_Target_of G);
coherence
((the_Source_of G) ~) * (the_Target_of G) is Relation of (the_Vertices_of G)
proof end;
end;

:: deftheorem defines VertexDomRel GLUNIR00:def 1 :
for G being _Graph holds VertexDomRel G = ((the_Source_of G) ~) * (the_Target_of G);

theorem Th1: :: GLUNIR00:1
for G being _Graph
for v, w being object holds
( [v,w] in VertexDomRel G iff ex e being object st e DJoins v,w,G )
proof end;

theorem Th2: :: GLUNIR00:2
for G being _Graph
for v, w being object holds
( [v,w] in (VertexDomRel G) ~ iff ex e being object st e DJoins w,v,G )
proof end;

Lm1: for G being _Graph holds
( G is loopless iff VertexDomRel G misses id (the_Vertices_of G) )
proof end;

theorem Th3: :: GLUNIR00:3
for G being _Graph holds
( G is loopless iff VertexDomRel G is irreflexive )
proof end;

registration
let G be loopless _Graph;
cluster VertexDomRel G -> irreflexive ;
coherence
VertexDomRel G is irreflexive by Th3;
end;

registration
let G be non loopless _Graph;
cluster VertexDomRel G -> non irreflexive ;
coherence
not VertexDomRel G is irreflexive by Th3;
end;

registration
let G be non-multi _Graph;
cluster VertexDomRel G -> antisymmetric ;
coherence
VertexDomRel G is antisymmetric
proof end;
end;

registration
let G be simple _Graph;
cluster VertexDomRel G -> asymmetric ;
coherence
VertexDomRel G is asymmetric
proof end;
end;

theorem Th4: :: GLUNIR00:4
for G being _Graph st ex e1, e2, x, y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G ) holds
not VertexDomRel G is asymmetric
proof end;

registration
let G be non non-multi non-Dmulti _Graph;
cluster VertexDomRel G -> non asymmetric ;
coherence
not VertexDomRel G is asymmetric
proof end;
end;

:: means G is then without isolated vertices
theorem Th5: :: GLUNIR00:5
for G being loopless _Graph st field (VertexDomRel G) = the_Vertices_of G holds
for C being Component of G holds not C is _trivial
proof end;

:: means if G is without isolated vertices
theorem Th6: :: GLUNIR00:6
for G being _Graph st ( for C being Component of G holds not C is _trivial ) holds
field (VertexDomRel G) = the_Vertices_of G
proof end;

theorem :: GLUNIR00:7
for G being non _trivial connected _Graph holds field (VertexDomRel G) = the_Vertices_of G
proof end;

registration
let G be complete _Graph;
cluster VertexDomRel G -> connected ;
coherence
VertexDomRel G is connected
proof end;
end;

::registration
:: let G be non complete without_isolated_vertices _Graph;
:: cluster VertexDomRel(G) -> non connected;
:: coherence;
::end;
theorem Th8: :: GLUNIR00:8
for G being _Graph holds
( G is edgeless iff VertexDomRel G is empty )
proof end;

registration
let G be edgeless _Graph;
cluster VertexDomRel G -> empty ;
coherence
VertexDomRel G is empty ;
end;

registration
let G be non edgeless _Graph;
cluster VertexDomRel G -> non empty ;
coherence
not VertexDomRel G is empty by Th8;
end;

Lm2: for G being _Graph holds
( G is loopfull iff id (the_Vertices_of G) c= VertexDomRel G )
proof end;

theorem Th9: :: GLUNIR00:9
for G being _Graph holds
( G is loopfull iff ( VertexDomRel G is total & VertexDomRel G is reflexive ) )
proof end;

registration
let G be loopfull _Graph;
cluster VertexDomRel G -> total reflexive ;
coherence
( VertexDomRel G is reflexive & VertexDomRel G is total ) by Th9;
end;

::registration
:: let G be non loopfull without_isolated_vertices _Graph;
:: cluster VertexDomRel(G) -> non reflexive;
:: coherence;
::end;
registration
let G be vertex-finite _Graph;
cluster VertexDomRel G -> finite ;
coherence
VertexDomRel G is finite ;
end;

theorem Th10: :: GLUNIR00:10
for G being _Graph holds card (VertexDomRel G) = card (Class (DEdgeAdjEqRel G))
proof end;

theorem :: GLUNIR00:11
for G being _Graph holds card (VertexDomRel G) c= G .size()
proof end;

theorem Th12: :: GLUNIR00:12
for G being non-Dmulti _Graph holds G .size() = card (VertexDomRel G)
proof end;

theorem :: GLUNIR00:13
for G being _Graph
for v being Vertex of G holds Im ((VertexDomRel G),v) = v .outNeighbors()
proof end;

theorem :: GLUNIR00:14
for G being _Graph
for v being Vertex of G holds Coim ((VertexDomRel G),v) = v .inNeighbors()
proof end;

theorem Th15: :: GLUNIR00:15
for G being _Graph
for H being Subgraph of G holds VertexDomRel H c= VertexDomRel G
proof end;

theorem Th16: :: GLUNIR00:16
for G being _Graph
for H being removeDParallelEdges of G holds VertexDomRel H = VertexDomRel G
proof end;

theorem Th17: :: GLUNIR00:17
for G being _Graph
for H being removeLoops of G holds VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))
proof end;

theorem :: GLUNIR00:18
for G being _Graph
for H being DSimpleGraph of G holds VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))
proof end;

theorem Th19: :: GLUNIR00:19
for G1, G2 being _Graph st G1 == G2 holds
VertexDomRel G1 = VertexDomRel G2
proof end;

theorem Th20: :: GLUNIR00:20
for G being _Graph
for H being reverseEdgeDirections of G holds VertexDomRel H = (VertexDomRel G) ~
proof end;

theorem Th21: :: GLUNIR00:21
for G being _Graph
for V being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,V holds VertexDomRel H = (VertexDomRel G) /\ [:V,V:]
proof end;

theorem Th22: :: GLUNIR00:22
for G being _Graph
for V being set
for H being 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 end;

theorem Th23: :: GLUNIR00:23
for G being non _trivial _Graph
for v being Vertex of G
for H being removeVertex of G,v holds VertexDomRel H = (VertexDomRel G) \ ([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:])
proof end;

theorem Th24: :: GLUNIR00:24
for G being non _trivial _Graph
for v being Vertex of G
for H being removeVertex of G,v st v is isolated holds
VertexDomRel H = VertexDomRel G
proof end;

theorem Th25: :: GLUNIR00:25
for G being _Graph
for V being set
for H being addVertices of G,V holds VertexDomRel H = VertexDomRel G
proof end;

theorem Th26: :: GLUNIR00:26
for G being _Graph
for v, e, w being object
for H being addEdge of G,v,e,w st ex e0 being object st e0 DJoins v,w,G holds
VertexDomRel H = VertexDomRel G
proof end;

theorem Th27: :: GLUNIR00:27
for G being _Graph
for v, w being Vertex of G
for e being object
for H being addEdge of G,v,e,w st not e in the_Edges_of G holds
VertexDomRel H = (VertexDomRel G) \/ {[v,w]}
proof end;

theorem :: GLUNIR00:28
for G being _Graph
for v being Vertex of G
for e, w being object
for H being 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 end;

theorem :: GLUNIR00:29
for G being _Graph
for v, e being object
for w being Vertex of G
for H being 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 end;

:: In their current form addAdjVertexTo/FromAll seem like their definition
:: will be changed in the future to allow a more general edge set.
:: Therefore the following theorems will not be proven here at the the moment.
:: theorem
:: for v being object, V being Subset of the_Vertices_of G
:: for H being addAdjVertexToAll of G,v,V st not v in the_Vertices_of G
:: holds VertexDomRel(H) = VertexDomRel(G) \/ [: {v},V :];
::
:: theorem
:: for v being object, V being Subset of the_Vertices_of G
:: for H being addAdjVertexFromAll of G,v,V st not v in the_Vertices_of G
:: holds VertexDomRel(H) = VertexDomRel(G) \/ [: V,{v} :];
theorem Th30: :: GLUNIR00:30
for G being _Graph
for V being Subset of (the_Vertices_of G)
for H being addLoops of G,V holds VertexDomRel H = (VertexDomRel G) \/ (id V)
proof end;

theorem :: GLUNIR00:31
for G being _Graph
for H being DLGraphComplement of G holds VertexDomRel H = [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G)
proof end;

definition
let G be _Graph;
func VertexAdjSymRel G -> Relation of (the_Vertices_of G) equals :: GLUNIR00:def 2
(VertexDomRel G) \/ ((VertexDomRel G) ~);
coherence
(VertexDomRel G) \/ ((VertexDomRel G) ~) is Relation of (the_Vertices_of G) ;
end;

:: deftheorem defines VertexAdjSymRel GLUNIR00:def 2 :
for G being _Graph holds VertexAdjSymRel G = (VertexDomRel G) \/ ((VertexDomRel G) ~);

theorem Th32: :: GLUNIR00:32
for G being _Graph
for v, w being object holds
( [v,w] in VertexAdjSymRel G iff ex e being object st e Joins v,w,G )
proof end;

theorem Th33: :: GLUNIR00:33
for G being _Graph
for v, w being Vertex of G holds
( [v,w] in VertexAdjSymRel G iff v,w are_adjacent )
proof end;

theorem Th34: :: GLUNIR00:34
for G being _Graph holds VertexDomRel G c= VertexAdjSymRel G by XBOOLE_1:7;

theorem :: GLUNIR00:35
for G being _Graph holds VertexAdjSymRel G = (((the_Source_of G) ~) * (the_Target_of G)) \/ (((the_Target_of G) ~) * (the_Source_of G))
proof end;

registration
let G be _Graph;
cluster VertexAdjSymRel G -> symmetric ;
coherence
VertexAdjSymRel G is symmetric
proof end;
end;

Lm3: for G being _Graph holds
( G is loopless iff VertexAdjSymRel G misses id (the_Vertices_of G) )
proof end;

theorem Th36: :: GLUNIR00:36
for G being _Graph holds
( G is loopless iff VertexAdjSymRel G is irreflexive )
proof end;

registration
let G be loopless _Graph;
cluster VertexAdjSymRel G -> irreflexive ;
coherence
VertexAdjSymRel G is irreflexive ;
end;

registration
let G be non loopless _Graph;
cluster VertexAdjSymRel G -> non irreflexive ;
coherence
not VertexAdjSymRel G is irreflexive by Th36;
end;

:: means G is then without isolated vertices
theorem :: GLUNIR00:37
for G being loopless _Graph st VertexAdjSymRel G is total holds
for C being Component of G holds not C is _trivial
proof end;

:: means if G is without isolated vertices
theorem Th38: :: GLUNIR00:38
for G being _Graph st ( for C being Component of G holds not C is _trivial ) holds
VertexAdjSymRel G is total
proof end;

registration
let G be non _trivial connected _Graph;
cluster VertexAdjSymRel G -> total ;
coherence
VertexAdjSymRel G is total
proof end;
end;

registration
let G be complete _Graph;
cluster VertexAdjSymRel G -> connected ;
coherence
VertexAdjSymRel G is connected
proof end;
end;

:: registration
:: let G be non complete without_isolated_vertices _Graph;
:: cluster VertexAdjSymRel(G) -> non connected;
:: coherence;
:: end;
theorem :: GLUNIR00:39
for G being _Graph holds
( G is edgeless iff VertexAdjSymRel G is empty )
proof end;

registration
let G be edgeless _Graph;
cluster VertexAdjSymRel G -> empty ;
coherence
VertexAdjSymRel G is empty ;
end;

registration
let G be non edgeless _Graph;
cluster VertexAdjSymRel G -> non empty ;
coherence
not VertexAdjSymRel G is empty ;
end;

Lm4: for G being _Graph holds
( G is loopfull iff id (the_Vertices_of G) c= VertexAdjSymRel G )
proof end;

theorem Th40: :: GLUNIR00:40
for G being _Graph holds
( G is loopfull iff ( VertexAdjSymRel G is total & VertexAdjSymRel G is reflexive ) )
proof end;

registration
let G be loopfull _Graph;
cluster VertexAdjSymRel G -> total reflexive ;
coherence
( VertexAdjSymRel G is reflexive & VertexAdjSymRel G is total ) by Th40;
end;

:: registration
:: let G be non loopfull without_isolated_vertices _Graph;
:: cluster VertexAdjSymRel(G) -> non reflexive;
:: coherence;
:: end;
registration
let G be vertex-finite _Graph;
cluster VertexAdjSymRel G -> finite ;
coherence
VertexAdjSymRel G is finite ;
end;

theorem Th41: :: GLUNIR00:41
for G being _Graph holds card (Class (DEdgeAdjEqRel G)) c= card (VertexAdjSymRel G)
proof end;

theorem :: GLUNIR00:42
for G being _Graph holds card (Class (EdgeAdjEqRel G)) c= card (VertexAdjSymRel G)
proof end;

theorem :: GLUNIR00:43
for G being non-Dmulti _Graph holds G .size() c= card (VertexAdjSymRel G)
proof end;

theorem :: GLUNIR00:44
for G being _Graph
for v being Vertex of G holds Im ((VertexAdjSymRel G),v) = v .allNeighbors()
proof end;

theorem Th45: :: GLUNIR00:45
for G being _Graph
for H being Subgraph of G holds VertexAdjSymRel H c= VertexAdjSymRel G
proof end;

theorem Th46: :: GLUNIR00:46
for G being _Graph
for H being removeParallelEdges of G holds VertexAdjSymRel H = VertexAdjSymRel G
proof end;

theorem Th47: :: GLUNIR00:47
for G being _Graph
for H being removeLoops of G holds VertexAdjSymRel H = (VertexAdjSymRel G) \ (id (the_Vertices_of G))
proof end;

theorem :: GLUNIR00:48
for G being _Graph
for H being SimpleGraph of G holds VertexAdjSymRel H = (VertexAdjSymRel G) \ (id (the_Vertices_of G))
proof end;

theorem Th49: :: GLUNIR00:49
for G1, G2 being _Graph st G1 == G2 holds
VertexAdjSymRel G1 = VertexAdjSymRel G2
proof end;

theorem :: GLUNIR00:50
for G being _Graph
for E being set
for H being reverseEdgeDirections of G,E holds VertexAdjSymRel H = VertexAdjSymRel G
proof end;

theorem :: GLUNIR00:51
for G being _Graph
for V being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,V holds VertexAdjSymRel H = (VertexAdjSymRel G) /\ [:V,V:]
proof end;

theorem Th52: :: GLUNIR00:52
for G being _Graph
for V being set
for H being 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 end;

theorem :: GLUNIR00:53
for G being non _trivial _Graph
for v being Vertex of G
for H being removeVertex of G,v holds VertexAdjSymRel H = (VertexAdjSymRel G) \ ([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:])
proof end;

theorem :: GLUNIR00:54
for G being non _trivial _Graph
for v being Vertex of G
for H being removeVertex of G,v st v is isolated holds
VertexAdjSymRel H = VertexAdjSymRel G
proof end;

theorem Th55: :: GLUNIR00:55
for G being _Graph
for V being set
for H being addVertices of G,V holds VertexAdjSymRel H = VertexAdjSymRel G
proof end;

theorem :: GLUNIR00:56
for G being _Graph
for v, w being Vertex of G
for e being object
for H being addEdge of G,v,e,w st v,w are_adjacent holds
VertexAdjSymRel H = VertexAdjSymRel G
proof end;

theorem Th57: :: GLUNIR00:57
for G being _Graph
for v, w being Vertex of G
for e being object
for H being addEdge of G,v,e,w st not e in the_Edges_of G holds
VertexAdjSymRel H = (VertexAdjSymRel G) \/ {[v,w],[w,v]}
proof end;

theorem :: GLUNIR00:58
for G being _Graph
for v being Vertex of G
for e, w being object
for H being 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 end;

theorem :: GLUNIR00:59
for G being _Graph
for v, e being object
for w being Vertex of G
for H being 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 end;

theorem :: GLUNIR00:60
for G being _Graph
for v being object
for V being Subset of (the_Vertices_of G)
for H being addAdjVertexAll of G,v,V st not v in the_Vertices_of G holds
VertexAdjSymRel H = ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:]
proof end;

theorem :: GLUNIR00:61
for G being _Graph
for V being Subset of (the_Vertices_of G)
for H being addLoops of G,V holds VertexAdjSymRel H = (VertexAdjSymRel G) \/ (id V)
proof end;

theorem :: GLUNIR00:62
for G being _Graph
for H being LGraphComplement of G holds VertexAdjSymRel H = [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexAdjSymRel G)
proof end;

definition
let V be non empty set ;
let E be Relation of V;
func createGraph (V,E) -> _Graph equals :: GLUNIR00:def 3
 createGraph (V,E,((pr1 (V,V)) | E),((pr2 (V,V)) | E));
coherence
createGraph (V,E,((pr1 (V,V)) | E),((pr2 (V,V)) | E)) is _Graph ;
end;

:: deftheorem defines createGraph GLUNIR00:def 3 :
for V being non empty set
for E being Relation of V holds createGraph (V,E) = createGraph (V,E,((pr1 (V,V)) | E),((pr2 (V,V)) | E));

registration
let V be non empty set ;
let E be Relation of V;
cluster the_Edges_of (createGraph (V,E)) -> Relation-like ;
coherence
the_Edges_of (createGraph (V,E)) is Relation-like ;
end;

theorem Th63: :: GLUNIR00:63
for V being non empty set
for E being Relation of V
for v, w being object holds
( [v,w] in E iff [v,w] DJoins v,w, createGraph (V,E) )
proof end;

theorem Th64: :: GLUNIR00:64
for V being non empty set
for E being Relation of V
for e, v, w being object st e DJoins v,w, createGraph (V,E) holds
e = [v,w]
proof end;

theorem Th65: :: GLUNIR00:65
for V being non empty set
for E being Relation of V holds VertexDomRel (createGraph (V,E)) = E
proof end;

registration
let V be non empty set ;
let E be Relation of V;
reduce VertexDomRel (createGraph (V,E)) to E;
reducibility
VertexDomRel (createGraph (V,E)) = E by Th65;
end;

registration
let V be non empty set ;
let E be Relation of V;
cluster createGraph (V,E) -> non-Dmulti plain ;
coherence
( createGraph (V,E) is plain & createGraph (V,E) is non-Dmulti )
proof end;
end;

theorem Th66: :: GLUNIR00:66
for V being non empty set
for E being Relation of V holds
( V is trivial iff createGraph (V,E) is _trivial )
proof end;

registration
let V be non empty trivial set ;
let E be Relation of V;
cluster createGraph (V,E) -> _trivial ;
coherence
createGraph (V,E) is _trivial by Th66;
end;

registration
let V be non trivial set ;
let E be Relation of V;
cluster createGraph (V,E) -> non _trivial ;
coherence
not createGraph (V,E) is _trivial by Th66;
end;

theorem Th67: :: GLUNIR00:67
for V being non empty set
for E being Relation of V holds
( E is irreflexive iff createGraph (V,E) is loopless )
proof end;

registration
let V be non empty set ;
let E be irreflexive Relation of V;
cluster createGraph (V,E) -> loopless ;
coherence
createGraph (V,E) is loopless by Th67;
end;

registration
let V be non empty set ;
let E be non irreflexive Relation of V;
cluster createGraph (V,E) -> non loopless ;
coherence
not createGraph (V,E) is loopless by Th67;
end;

theorem Th68: :: GLUNIR00:68
for V being non empty set
for E being Relation of V holds
( E is antisymmetric iff createGraph (V,E) is non-multi )
proof end;

registration
let V be non empty set ;
let E be antisymmetric Relation of V;
cluster createGraph (V,E) -> non-multi ;
coherence
createGraph (V,E) is non-multi 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
not createGraph (V,E) is non-multi by Th68;
end;

registration
let V be non empty set ;
let E be asymmetric Relation of V;
cluster createGraph (V,E) -> simple ;
coherence
createGraph (V,E) is simple ;
end;

theorem Th69: :: GLUNIR00:69
for V being non empty set
for E being Relation of V st createGraph (V,E) is complete holds
E is connected
proof end;

registration
let V be non trivial set ;
let E be non connected Relation of V;
cluster createGraph (V,E) -> non complete ;
coherence
not createGraph (V,E) is complete by Th69;
end;

theorem Th70: :: GLUNIR00:70
for V being non empty set
for E being Relation of V holds
( E is empty iff createGraph (V,E) is edgeless )
proof end;

registration
let V be non empty set ;
let E be empty Relation of V;
cluster createGraph (V,E) -> edgeless ;
coherence
createGraph (V,E) is edgeless ;
end;

registration
let V be non empty set ;
let E be non empty Relation of V;
cluster createGraph (V,E) -> non edgeless ;
coherence
not createGraph (V,E) is edgeless by Th70;
end;

theorem Th71: :: GLUNIR00:71
for V being non empty set
for E being Relation of V holds
( ( E is total & E is reflexive ) iff createGraph (V,E) is loopfull )
proof end;

registration
let V be non empty set ;
let E be total reflexive Relation of V;
cluster createGraph (V,E) -> loopfull ;
coherence
createGraph (V,E) is loopfull by Th71;
end;

registration
let V be non empty set ;
let E be non total Relation of V;
cluster createGraph (V,E) -> non loopfull ;
coherence
not createGraph (V,E) is loopfull by Th71;
end;

registration
let V be non empty finite set ;
let E be Relation of V;
cluster createGraph (V,E) -> ;
coherence
createGraph (V,E) is finite ;
end;

registration
let V be non empty set ;
let E be finite Relation of V;
cluster createGraph (V,E) -> edge-finite ;
coherence
createGraph (V,E) is edge-finite ;
end;

theorem Th72: :: GLUNIR00:72
for V being non empty set
for E being Relation of V
for v being Vertex of (createGraph (V,E)) holds Im (E,v) = v .outNeighbors()
proof end;

theorem Th73: :: GLUNIR00:73
for V being non empty set
for E being Relation of V
for v being Vertex of (createGraph (V,E)) holds Coim (E,v) = v .inNeighbors()
proof end;

theorem Th74: :: GLUNIR00:74
for V being non empty set
for E being Relation of V
for X being set holds E | X = (createGraph (V,E)) .edgesOutOf X
proof end;

theorem Th75: :: GLUNIR00:75
for V being non empty set
for E being Relation of V
for Y being set holds Y |` E = (createGraph (V,E)) .edgesInto Y
proof end;

theorem Th76: :: GLUNIR00:76
for V being non empty set
for E being Relation of V
for X, Y being set holds (Y |` E) | X = (createGraph (V,E)) .edgesDBetween (X,Y)
proof end;

theorem Th77: :: GLUNIR00:77
for V being non empty set
for E being Relation of V
for X, Y being set holds ((Y |` E) | X) \/ ((X |` E) | Y) = (createGraph (V,E)) .edgesBetween (X,Y)
proof end;

theorem Th78: :: GLUNIR00:78
for V being non empty set
for E being Relation of V
for v being Vertex of (createGraph (V,E)) holds E | {v} = v .edgesOut()
proof end;

theorem Th79: :: GLUNIR00:79
for V being non empty set
for E being Relation of V
for v being Vertex of (createGraph (V,E)) holds {v} |` E = v .edgesIn()
proof end;

theorem Th80: :: GLUNIR00:80
for V being non empty set
for E being Relation of V
for X being set holds (E | X) \/ (X |` E) = (createGraph (V,E)) .edgesInOut X
proof end;

theorem :: GLUNIR00:81
for V being non empty set
for E being Relation of V holds dom E = rng (the_Source_of (createGraph (V,E)))
proof end;

theorem :: GLUNIR00:82
for V being non empty set
for E being Relation of V holds rng E = rng (the_Target_of (createGraph (V,E)))
proof end;

theorem Th83: :: GLUNIR00:83
for V being non empty set
for E being Relation of V
for v being Vertex of (createGraph (V,E)) holds
( v is isolated iff not v in field E )
proof end;

theorem :: GLUNIR00:84
for V being non empty set
for E being Relation of V holds
( E is symmetric iff VertexAdjSymRel (createGraph (V,E)) = E )
proof end;

theorem :: GLUNIR00:85
for V1 being non empty set
for V2 being non empty Subset of V1
for E1 being Relation of V1
for E2 being Relation of V2 st E2 c= E1 holds
createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2
proof end;

theorem Th86: :: GLUNIR00:86
for G being non-Dmulti _Graph ex F being PGraphMapping of G, createGraph ((the_Vertices_of G),(VertexDomRel G)) st
( F is Disomorphism & F _V = id (the_Vertices_of G) & ( for e being object st e in the_Edges_of G holds
(F _E) . e = [((the_Source_of G) . e),((the_Target_of G) . e)] ) )
proof end;

theorem :: GLUNIR00:87
for G being non-Dmulti _Graph holds createGraph ((the_Vertices_of G),(VertexDomRel G)) is G -Disomorphic
proof end;

definition
let V be non empty set ;
let E be symmetric Relation of V;
mode GraphFromSymRel of V,E is removeParallelEdges of createGraph (V,E);
end;

theorem Th88: :: GLUNIR00:88
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for v, w being object holds
( [v,w] in E iff ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G ) )
proof end;

theorem Th89: :: GLUNIR00:89
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for v, w being Vertex of G holds
( [v,w] in E iff v,w are_adjacent )
proof end;

registration
let V be non empty set ;
let E be symmetric Relation of V;
cluster -> non-multi for removeParallelEdges of createGraph (V,E);
coherence
for b1 being GraphFromSymRel of V,E holds b1 is non-multi ;
end;

theorem :: GLUNIR00:90
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E holds the_Edges_of G c= E ;

theorem :: GLUNIR00:91
for V being non empty set
for E being symmetric Relation of V
for G1, G2 being GraphFromSymRel of V,E holds the_Vertices_of G1 = the_Vertices_of G2
proof end;

theorem :: GLUNIR00:92
for V being non empty set
for E being symmetric Relation of V
for G1, G2 being GraphFromSymRel of V,E holds G2 is G1 -isomorphic by GLIB_010:169;

theorem :: GLUNIR00:93
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E holds
( V is trivial iff G is _trivial ) ;

registration
let V be non empty trivial set ;
let E be symmetric Relation of V;
cluster -> _trivial for removeParallelEdges of createGraph (V,E);
coherence
for b1 being GraphFromSymRel of V,E holds b1 is _trivial ;
end;

registration
let V be non trivial set ;
let E be symmetric Relation of V;
cluster -> non _trivial for removeParallelEdges of createGraph (V,E);
coherence
for b1 being GraphFromSymRel of V,E holds not b1 is _trivial ;
end;

theorem :: GLUNIR00:94
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E holds
( E is irreflexive iff G is loopless ) ;

registration
let V be non empty set ;
let E be irreflexive symmetric Relation of V;
cluster -> loopless for removeParallelEdges of createGraph (V,E);
coherence
for b1 being GraphFromSymRel of V,E holds b1 is loopless ;
end;

registration
let V be non empty set ;
let E be non irreflexive symmetric Relation of V;
cluster -> non loopless for removeParallelEdges of createGraph (V,E);
coherence
for b1 being GraphFromSymRel of V,E holds not b1 is loopless ;
end;

theorem :: GLUNIR00:95
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E st G is complete holds
E is connected
proof end;

registration
let V be non trivial set ;
let E be symmetric non connected Relation of V;
cluster -> non complete for removeParallelEdges of createGraph (V,E);
coherence
for b1 being GraphFromSymRel of V,E holds not b1 is complete ;
end;

theorem :: GLUNIR00:96
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E holds
( E is empty iff G is edgeless ) ;

registration
let V be non empty set ;
let E be empty Relation of V;
cluster -> edgeless for removeParallelEdges of createGraph (V,E);
coherence
for b1 being GraphFromSymRel of V,E holds b1 is edgeless ;
end;

registration
let V be non empty set ;
let E be non empty symmetric Relation of V;
cluster -> non edgeless for removeParallelEdges of createGraph (V,E);
coherence
for b1 being GraphFromSymRel of V,E holds not b1 is edgeless ;
end;

theorem :: GLUNIR00:97
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E holds
( ( E is total & E is reflexive ) iff G is loopfull )
proof end;

registration
let V be non empty set ;
let E be total reflexive symmetric Relation of V;
cluster -> loopfull for removeParallelEdges of createGraph (V,E);
coherence
for b1 being GraphFromSymRel of V,E holds b1 is loopfull ;
end;

registration
let V be non empty set ;
let E be non total symmetric Relation of V;
cluster -> non loopfull for removeParallelEdges of createGraph (V,E);
coherence
for b1 being GraphFromSymRel of V,E holds not b1 is loopfull ;
end;

registration
let V be non empty finite set ;
let E be symmetric Relation of V;
cluster -> finite for removeParallelEdges of createGraph (V,E);
coherence
for b1 being GraphFromSymRel of V,E holds b1 is finite ;
end;

theorem :: GLUNIR00:98
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for v being Vertex of G holds Im (E,v) = v .allNeighbors()
proof end;

theorem :: GLUNIR00:99
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for X being set holds G .edgesInOut X c= (E | X) \/ (X |` E)
proof end;

theorem :: GLUNIR00:100
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for X, Y being set holds G .edgesBetween (X,Y) c= ((Y |` E) | X) \/ ((X |` E) | Y)
proof end;

::theorem
:: for v being Vertex of G holds card(E|{v}) = card(v.edgesInOut());
theorem :: GLUNIR00:101
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for v being Vertex of G holds v .edgesOut() c= E | {v}
proof end;

theorem :: GLUNIR00:102
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for v being Vertex of G holds v .edgesIn() c= {v} |` E
proof end;

theorem :: GLUNIR00:103
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E
for v being Vertex of G holds
( v is isolated iff not v in field E )
proof end;

theorem :: GLUNIR00:104
for V being non empty set
for E being symmetric Relation of V
for G being GraphFromSymRel of V,E holds VertexAdjSymRel G = E
proof end;

theorem :: GLUNIR00:105
for V1 being non empty set
for V2 being non empty Subset of V1
for E1 being symmetric Relation of V1
for E2 being symmetric Relation of V2
for G1 being GraphFromSymRel of V1,E1
for G2 being GraphFromSymRel of V2,E2 st E2 c= E1 holds
ex F being PGraphMapping of G2,G1 st
( F is weak_SG-embedding & F _V = id V2 & ( for v, w being object holds
( not [v,w] in the_Edges_of G2 or (F _E) . [v,w] = [v,w] or (F _E) . [v,w] = [w,v] ) ) )
proof end;

theorem Th106: :: GLUNIR00:106
for G1 being non-multi _Graph
for G2 being GraphFromSymRel of (the_Vertices_of G1),(VertexAdjSymRel G1) ex F being PGraphMapping of G1,G2 st
( F is isomorphism & F _V = id (the_Vertices_of G1) & ( for e being object holds
( not e in the_Edges_of G1 or (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 end;

theorem :: GLUNIR00:107
for G1 being non-multi _Graph
for G2 being GraphFromSymRel of (the_Vertices_of G1),(VertexAdjSymRel G1) holds G2 is G1 -isomorphic
proof end;