:: Underlying Simple Graphs
:: by Sebastian Koch
::
:: Received August 29, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


:: into XBOOLE_1 ?
theorem Th1: :: GLIB_009:1
for X, Y being set st Y c= X holds
X \ (X \ Y) = Y
proof end;

Lm1: for R being Relation
for X being set holds (R | X) ~ = X |` (R ~)
proof end;

:: into RELAT_1 ?
theorem Th2: :: GLIB_009:2
for R being Relation
for X being set holds
( (R | X) ~ = X |` (R ~) & (X |` R) ~ = (R ~) | X )
proof end;

theorem :: GLIB_009:3
canceled;

::$CT
:: into FUNCT_1 ?
:: reformulation of FUNCT_1:113
theorem :: GLIB_009:4
for f being Function
for Y being set holds Y |` f = f | (dom (Y |` f))
proof end;

:: into FUNCT_1 ?
theorem :: GLIB_009:5
for f being one-to-one Function
for X being set holds
( (f | X) " = X |` (f ") & (X |` f) " = (f ") | X )
proof end;

:: BEGIN into GLIB_000 ?
theorem Th6: :: GLIB_009:6
for G being _Graph
for e, x1, y1, x2, y2 being object st e DJoins x1,y1,G & e DJoins x2,y2,G holds
( x1 = x2 & y1 = y2 )
proof end;

registration
let G be _trivial _Graph;
cluster the_Vertices_of G -> trivial ;
coherence
the_Vertices_of G is trivial
proof end;
end;

registration
cluster Relation-like NAT -defined Function-like V42() [Graph-like] _trivial non-Dmulti -> non-multi for set ;
coherence
for b1 being _Graph st b1 is _trivial & b1 is non-Dmulti holds
b1 is non-multi
proof end;
let G be _trivial non-Dmulti _Graph;
cluster the_Edges_of G -> trivial ;
coherence
the_Edges_of G is trivial
proof end;
end;

theorem Th7: :: GLIB_009:7
for G being _Graph
for X, Y being set
for e, x, y being object st e DJoins x,y,G & x in X & y in Y holds
e DSJoins X,Y,G
proof end;

theorem :: GLIB_009:8
for G being _trivial _Graph
for H being _Graph st the_Vertices_of H c= the_Vertices_of G & the_Edges_of H c= the_Edges_of G holds
( H is _trivial & H is Subgraph of G )
proof end;

theorem Th9: :: GLIB_009:9
for G being _Graph holds G == G | _GraphSelectors
proof end;

theorem Th10: :: GLIB_009:10
for G being _Graph
for X, Y being set
for e being object holds
( e SJoins X,Y,G iff e SJoins Y,X,G )
proof end;

theorem Th11: :: GLIB_009:11
for G being _Graph
for X, Y being set
for e being object holds
( e SJoins X,Y,G iff ( e DSJoins X,Y,G or e DSJoins Y,X,G ) )
proof end;

theorem Th12: :: GLIB_009:12
for G being _Graph
for e, v, w being object st e SJoins {v},{w},G holds
e Joins v,w,G
proof end;

theorem Th13: :: GLIB_009:13
for G being _Graph
for e, v, w being object st e DSJoins {v},{w},G holds
e DJoins v,w,G
proof end;

theorem :: GLIB_009:14
for G being _Graph
for v, w being object st v <> w holds
( G .edgesDBetween ({v},{w}) misses G .edgesDBetween ({w},{v}) & G .edgesBetween ({v},{w}) = (G .edgesDBetween ({v},{w})) \/ (G .edgesDBetween ({w},{v})) )
proof end;

theorem :: GLIB_009:15
for G being _Graph
for X being set holds G .edgesBetween (X,X) = G .edgesDBetween (X,X)
proof end;

theorem :: GLIB_009:16
for G being _Graph
for X, Y being set holds G .edgesBetween (X,Y) = G .edgesBetween (Y,X)
proof end;

theorem :: GLIB_009:17
for G being _Graph holds
( G is loopless iff for v, e being object holds not e DJoins v,v,G )
proof end;

theorem Th18: :: GLIB_009:18
for G being _Graph holds
( G is loopless iff for v, e being object holds not e SJoins {v},{v},G )
proof end;

theorem Th19: :: GLIB_009:19
for G being _Graph holds
( G is loopless iff for v, e being object holds not e DSJoins {v},{v},G )
proof end;

theorem Th20: :: GLIB_009:20
for G being _Graph holds
( G is loopless iff for v being object holds G .edgesBetween ({v},{v}) = {} )
proof end;

theorem Th21: :: GLIB_009:21
for G being _Graph holds
( G is loopless iff for v being object holds G .edgesDBetween ({v},{v}) = {} )
proof end;

registration
let G be loopless _Graph;
let v be object ;
cluster G .edgesBetween ({v},{v}) -> empty ;
coherence
G .edgesBetween ({v},{v}) is empty by Th20;
cluster G .edgesDBetween ({v},{v}) -> empty ;
coherence
G .edgesDBetween ({v},{v}) is empty by Th21;
end;

theorem Th22: :: GLIB_009:22
for G being _Graph holds
( G is non-multi iff for v, w being object holds G .edgesBetween ({v},{w}) is trivial )
proof end;

registration
let G be non-multi _Graph;
let v, w be object ;
cluster G .edgesBetween ({v},{w}) -> trivial ;
coherence
G .edgesBetween ({v},{w}) is trivial by Th22;
end;

theorem Th23: :: GLIB_009:23
for G being _Graph holds
( G is non-Dmulti iff for v, w being object holds G .edgesDBetween ({v},{w}) is trivial )
proof end;

registration
let G be non-Dmulti _Graph;
let v, w be object ;
cluster G .edgesDBetween ({v},{w}) -> trivial ;
coherence
G .edgesDBetween ({v},{w}) is trivial by Th23;
end;

registration
let G be non _trivial _Graph;
cluster spanning -> non _trivial for Subgraph of G;
coherence
for b1 being Subgraph of G st b1 is spanning holds
not b1 is _trivial
proof end;
end;

registration
let G be _Graph;
cluster isolated -> non endvertex for Element of the_Vertices_of G;
coherence
for b1 being Vertex of G st b1 is isolated holds
not b1 is endvertex
proof end;
end;

:: END into GLIB_000 ?
:: into GLIB_001 ?
theorem Th24: :: GLIB_009:24
for G being _Graph
for v being Vertex of G holds (G .walkOf v) .edgeSeq() = <*> (the_Edges_of G)
proof end;

:: into GLIB_001 ?
theorem Th25: :: GLIB_009:25
for G being _Graph
for v being Vertex of G holds (G .walkOf v) .edges() = {}
proof end;

:: into GLIB_001
registration
let G be _Graph;
let W be V5() Walk of G;
cluster W .edges() -> empty trivial ;
coherence
( W .edges() is empty & W .edges() is trivial )
proof end;
end;

:: into GLIB_001 ?
registration
let G be _Graph;
let W be Walk of G;
cluster W .vertices() -> non empty ;
coherence
not W .vertices() is empty
proof end;
end;

:: into GLIB_001 ?
theorem :: GLIB_009:26
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() holds
W1 = W2
proof end;

:: into GLIB_001 ?
theorem :: GLIB_009:27
for G being _Graph
for p being FinSequence of the_Vertices_of G
for q being FinSequence of the_Edges_of G st len p = 1 + (len q) & ( for n being Element of NAT st 1 <= n & n + 1 <= len p holds
q . n Joins p . n,p . (n + 1),G ) holds
ex W being Walk of G st
( W .vertexSeq() = p & W .edgeSeq() = q )
proof end;

Lm2: for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 holds
( len W1 = len W2 iff W1 .length() = W2 .length() )
proof end;

:: into GLIB_001 ?
theorem :: GLIB_009:28
for G being _Graph
for W being Walk of G holds len (W .vertexSeq()) = (W .length()) + 1
proof end;

Lm3: for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds
len W1 = len W2
proof end;

:: into GLIB_001 ?
theorem Th29: :: GLIB_009:29
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2
for n being odd Nat st W1 .vertexSeq() = W2 .vertexSeq() holds
W1 . n = W2 . n
proof end;

:: into GLIB_001 ?
theorem Th30: :: GLIB_009:30
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds
( len W1 = len W2 & W1 .length() = W2 .length() & W1 .first() = W2 .first() & W1 .last() = W2 .last() & W2 is_Walk_from W1 .first() ,W1 .last() )
proof end;

:: into GLIB_001 ?
theorem Th31: :: GLIB_009:31
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds
( ( W1 is V5() implies not W2 is V5() ) & ( W1 is closed implies W2 is closed ) )
proof end;

:: into GLIB_001 ?
:: in the case len W1 = 5, W1 could be the Path in a dipole visiting both
:: edges while W2 goes back on the same edge it came from
theorem Th32: :: GLIB_009:32
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & len W1 <> 5 holds
( ( W1 is Path-like implies W2 is Path-like ) & ( W1 is Cycle-like implies W2 is Cycle-like ) )
proof end;

:: into GLIB_001 ?
scheme :: GLIB_009:sch 1
IndWalk{ F1() -> _Graph, P1[ Walk of F1()] } :
for W being Walk of F1() holds P1[W]
provided
A1: for W being V5() Walk of F1() holds P1[W] and
A2: for W being Walk of F1()
for e being object st e in (W .last()) .edgesInOut() & P1[W] holds
P1[W .addEdge e]
proof end;

:: into GLIB_001 ?
scheme :: GLIB_009:sch 2
IndDWalk{ F1() -> _Graph, P1[ Walk of F1()] } :
for W being DWalk of F1() holds P1[W]
provided
A1: for W being V5() DWalk of F1() holds P1[W] and
A2: for W being DWalk of F1()
for e being object st e in (W .last()) .edgesOut() & P1[W] holds
P1[W .addEdge e]
proof end;

:: into GLIB_002 ?
theorem Th33: :: GLIB_009:33
for G1 being _Graph
for E being Subset of (the_Edges_of G1)
for G2 being inducedSubgraph of G1, the_Vertices_of G1,E st G2 is connected holds
G1 is connected
proof end;

:: into GLIB_002 ?
theorem :: GLIB_009:34
for G1 being _Graph
for E being set
for G2 being removeEdges of G1,E st G2 is connected holds
G1 is connected by Th33;

:: into GLIB_002 ?
registration
let G1 be non connected _Graph;
let E be set ;
cluster -> non connected for inducedSubgraph of G1, the_Vertices_of G1,(the_Edges_of G1) \ E;
coherence
for b1 being removeEdges of G1,E holds not b1 is connected by Th33;
end;

:: into GLIB_002 ?
theorem Th35: :: GLIB_009:35
for G1 being _Graph
for G2 being Subgraph of G1 st ( for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last() ) holds
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
proof end;

:: into GLIB_002 ?
theorem Th36: :: GLIB_009:36
for G1 being _Graph
for G2 being Subgraph of G1 st ( for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last() ) & G1 is connected holds
G2 is connected
proof end;

:: into GLIB_002 ?
theorem Th37: :: GLIB_009:37
for G1 being _Graph
for G2 being spanning Subgraph of G1 st ( for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2 ) holds
G1 .componentSet() = G2 .componentSet()
proof end;

:: into GLIB_002 ?
theorem Th38: :: GLIB_009:38
for G1 being _Graph
for G2 being spanning Subgraph of G1 st ( for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2 ) holds
G1 .numComponents() = G2 .numComponents()
proof end;

:: into CHORD ?
theorem :: GLIB_009:39
for G being _Graph holds
( G is loopless iff for v being Vertex of G holds not v,v are_adjacent )
proof end;

registration
let G be non complete _Graph;
cluster spanning -> non complete for Subgraph of G;
coherence
for b1 being Subgraph of G st b1 is spanning holds
not b1 is complete
proof end;
end;

:: into GLIB_006 ?
theorem Th40: :: GLIB_009:40
for G2, G3 being _Graph
for G1 being Supergraph of G3 st G1 == G2 holds
G2 is Supergraph of G3
proof end;

theorem Th41: :: GLIB_009:41
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for x, y being set
for e being object holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
proof end;

:: into GLIB_007 ?
theorem Th42: :: GLIB_009:42
for G1, G2 being _Graph st G1 == G2 holds
G2 is reverseEdgeDirections of G1, {}
proof end;

:: into GLIB_007 ?
theorem :: GLIB_009:43
for G being _Graph holds G is reverseEdgeDirections of G, {} by Th42;

definition
let G be _Graph;
attr G is plain means :Def1: :: GLIB_009:def 1
 dom G = _GraphSelectors ;
end;

:: deftheorem Def1 defines plain GLIB_009:def 1 :
for G being _Graph holds
( G is plain iff dom G = _GraphSelectors );

registration
let G be _Graph;
cluster G | _GraphSelectors -> plain ;
coherence
G | _GraphSelectors is plain
proof end;
end;

registration
let V be non empty set ;
let E be set ;
let S, T be Function of E,V;
cluster createGraph (V,E,S,T) -> plain ;
coherence
createGraph (V,E,S,T) is plain
proof end;
end;

registration
let G be _Graph;
let X be set ;
cluster G .set (WeightSelector,X) -> non plain ;
coherence
not G .set (WeightSelector,X) is plain
proof end;
cluster G .set (ELabelSelector,X) -> non plain ;
coherence
not G .set (ELabelSelector,X) is plain
proof end;
cluster G .set (VLabelSelector,X) -> non plain ;
coherence
not G .set (VLabelSelector,X) is plain
proof end;
end;

registration
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for set ;
existence
ex b1 being _Graph st b1 is plain
proof end;
end;

theorem :: GLIB_009:44
for G1, G2 being plain _Graph st G1 == G2 holds
G1 = G2
proof end;

:: existence clusters for plain graph modes
registration
let G be _Graph;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for Subgraph of G;
existence
ex b1 being Subgraph of G st b1 is plain
proof end;
let V be set ;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for inducedSubgraph of G,(the_Vertices_of G) \ V,G .edgesBetween ((the_Vertices_of G) \ V);
existence
ex b1 being removeVertices of G,V st b1 is plain
proof end;
let E be set ;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for inducedSubgraph of G,V,E;
existence
ex b1 being inducedSubgraph of G,V,E st b1 is plain
proof end;
end;

registration
let G be _Graph;
let E be set ;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] spanning plain for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E;
existence
ex b1 being removeEdges of G,E st b1 is plain
proof end;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for reverseEdgeDirections of G,E;
existence
ex b1 being reverseEdgeDirections of G,E st b1 is plain
proof end;
end;

registration
let G be _Graph;
let v be set ;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for inducedSubgraph of G,(the_Vertices_of G) \ {v},G .edgesBetween ((the_Vertices_of G) \ {v});
existence
ex b1 being removeVertex of G,v st b1 is plain
proof end;
end;

registration
let G be _Graph;
let e be set ;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] spanning plain for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {e};
existence
ex b1 being removeEdge of G,e st b1 is plain
proof end;
end;

registration
let G be _Graph;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for Supergraph of G;
existence
ex b1 being Supergraph of G st b1 is plain
proof end;
let V be set ;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addVertices of G,V;
existence
ex b1 being addVertices of G,V st b1 is plain
proof end;
end;

registration
let G be _Graph;
let v, e, w be object ;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addEdge of G,v,e,w;
existence
ex b1 being addEdge of G,v,e,w st b1 is plain
proof end;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addAdjVertex of G,v,e,w;
existence
ex b1 being addAdjVertex of G,v,e,w st b1 is plain
proof end;
end;

registration
let G be _Graph;
let v be object ;
let V be set ;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addAdjVertexFromAll of G,v,V;
existence
ex b1 being addAdjVertexFromAll of G,v,V st b1 is plain
proof end;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addAdjVertexToAll of G,v,V;
existence
ex b1 being addAdjVertexToAll of G,v,V st b1 is plain
proof end;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addAdjVertexAll of G,v,V;
existence
ex b1 being addAdjVertexAll of G,v,V st b1 is plain
proof end;
end;

definition
let G be _Graph;
func G .loops() -> Subset of (the_Edges_of G) means :Def2: :: GLIB_009:def 2
 for e being object holds
( e in it iff ex v being object st e Joins v,v,G );
existence
ex b1 being Subset of (the_Edges_of G) st
for e being object holds
( e in b1 iff ex v being object st e Joins v,v,G )
proof end;
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e being object holds
( e in b1 iff ex v being object st e Joins v,v,G ) ) & ( for e being object holds
( e in b2 iff ex v being object st e Joins v,v,G ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines .loops() GLIB_009:def 2 :
for G being _Graph
for b2 being Subset of (the_Edges_of G) holds
( b2 = G .loops() iff for e being object holds
( e in b2 iff ex v being object st e Joins v,v,G ) );

theorem Th45: :: GLIB_009:45
for G being _Graph
for e being object holds
( e in G .loops() iff ex v being object st e DJoins v,v,G )
proof end;

theorem Th46: :: GLIB_009:46
for G being _Graph
for e, v, w being object st e Joins v,w,G & v <> w holds
not e in G .loops()
proof end;

theorem Th47: :: GLIB_009:47
for G being _Graph holds
( G is loopless iff G .loops() = {} )
proof end;

registration
let G be loopless _Graph;
cluster G .loops() -> empty ;
coherence
G .loops() is empty by Th47;
end;

registration
let G be non loopless _Graph;
cluster G .loops() -> non empty ;
coherence
not G .loops() is empty by Th47;
end;

theorem Th48: :: GLIB_009:48
for G1 being _Graph
for G2 being Subgraph of G1 holds G2 .loops() c= G1 .loops()
proof end;

theorem Th49: :: GLIB_009:49
for G2 being _Graph
for G1 being Supergraph of G2 holds G2 .loops() c= G1 .loops()
proof end;

theorem Th50: :: GLIB_009:50
for G1, G2 being _Graph st G1 == G2 holds
G1 .loops() = G2 .loops()
proof end;

theorem :: GLIB_009:51
for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds G1 .loops() = G2 .loops()
proof end;

theorem :: GLIB_009:52
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds G1 .loops() = G2 .loops()
proof end;

theorem :: GLIB_009:53
for G2 being _Graph
for v1, e, v2 being object
for G1 being addEdge of G2,v1,e,v2 st v1 <> v2 holds
G1 .loops() = G2 .loops()
proof end;

theorem :: GLIB_009:54
for G2 being _Graph
for v being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,v st not e in the_Edges_of G2 holds
G1 .loops() = (G2 .loops()) \/ {e}
proof end;

theorem :: GLIB_009:55
for G2 being _Graph
for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 holds G1 .loops() = G2 .loops()
proof end;

theorem :: GLIB_009:56
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V holds G1 .loops() = G2 .loops()
proof end;

theorem Th57: :: GLIB_009:57
for G being _Graph
for P being Path of G holds
( P .edges() misses G .loops() or ex v, e being object st
( e Joins v,v,G & P = G .walkOf (v,e,v) ) )
proof end;

definition
let G be _Graph;
mode removeLoops of G is removeEdges of G,(G .loops());
end;

theorem Th58: :: GLIB_009:58
for G1 being loopless _Graph
for G2 being _Graph holds
( G1 == G2 iff G2 is removeLoops of G1 )
proof end;

theorem Th59: :: GLIB_009:59
for G1, G2 being _Graph
for G3 being removeLoops of G1 holds
( G2 == G3 iff G2 is removeLoops of G1 ) by GLIB_006:16, GLIB_000:93;

theorem Th60: :: GLIB_009:60
for G1, G2 being _Graph
for G3 being removeLoops of G1 st G1 == G2 holds
G3 is removeLoops of G2
proof end;

registration
let G be _Graph;
cluster -> loopless for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());
coherence
for b1 being removeLoops of G holds b1 is loopless
proof end;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] spanning plain for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());
existence
ex b1 being removeLoops of G st b1 is plain
proof end;
end;

registration
let G be non-multi _Graph;
cluster -> simple for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());
coherence
for b1 being removeLoops of G holds b1 is simple ;
end;

registration
let G be non-Dmulti _Graph;
cluster -> Dsimple for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());
coherence
for b1 being removeLoops of G holds b1 is Dsimple ;
end;

registration
let G be complete _Graph;
cluster -> complete for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());
coherence
for b1 being removeLoops of G holds b1 is complete
proof end;
end;

theorem Th61: :: GLIB_009:61
for G1 being _Graph
for G2 being removeLoops of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()
proof end;

theorem Th62: :: GLIB_009:62
for G1 being _Graph
for G2 being removeLoops of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
proof end;

registration
let G be connected _Graph;
cluster -> connected for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());
coherence
for b1 being removeLoops of G holds b1 is connected
proof end;
end;

registration
let G be non connected _Graph;
cluster -> non connected for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());
coherence
for b1 being removeLoops of G holds not b1 is connected ;
end;

theorem :: GLIB_009:63
for G1 being _Graph
for G2 being removeLoops of G1 holds G1 .componentSet() = G2 .componentSet()
proof end;

theorem Th64: :: GLIB_009:64
for G1 being _Graph
for G2 being removeLoops of G1 holds G1 .numComponents() = G2 .numComponents()
proof end;

theorem Th65: :: GLIB_009:65
for G1 being _Graph
for G2 being removeLoops of G1 holds
( G1 is chordal iff G2 is chordal )
proof end;

:: non chordal cluster after non chordal has been clustered with cycles
registration
let G be chordal _Graph;
cluster -> chordal for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());
coherence
for b1 being removeLoops of G holds b1 is chordal by Th65;
end;

:: More theorems of this kind can be produced with other
:: subgraph modes. This particular example was needed
:: to show that the cut-vertex property prevails in graphs
:: with removed loops
theorem Th66: :: GLIB_009:66
for G1 being _Graph
for v being set
for G2 being removeLoops of G1
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is removeLoops of G3
proof end;

theorem Th67: :: GLIB_009:67
for G1 being _Graph
for G2 being removeLoops of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is cut-vertex iff v2 is cut-vertex )
proof end;

theorem Th68: :: GLIB_009:68
for G1 being _Graph
for G2 being removeLoops of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds
v2 is endvertex
proof end;

definition
let G be _Graph;
func EdgeAdjEqRel G -> Equivalence_Relation of (the_Edges_of G) means :Def3: :: GLIB_009:def 3
 for e1, e2 being object holds
( [e1,e2] in it iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) );
existence
ex b1 being Equivalence_Relation of (the_Edges_of G) st
for e1, e2 being object holds
( [e1,e2] in b1 iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of (the_Edges_of G) st ( for e1, e2 being object holds
( [e1,e2] in b1 iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) ) & ( for e1, e2 being object holds
( [e1,e2] in b2 iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) ) holds
b1 = b2
proof end;
func DEdgeAdjEqRel G -> Equivalence_Relation of (the_Edges_of G) means :Def4: :: GLIB_009:def 4
 for e1, e2 being object holds
( [e1,e2] in it iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) );
existence
ex b1 being Equivalence_Relation of (the_Edges_of G) st
for e1, e2 being object holds
( [e1,e2] in b1 iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of (the_Edges_of G) st ( for e1, e2 being object holds
( [e1,e2] in b1 iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) ) & ( for e1, e2 being object holds
( [e1,e2] in b2 iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines EdgeAdjEqRel GLIB_009:def 3 :
for G being _Graph
for b2 being Equivalence_Relation of (the_Edges_of G) holds
( b2 = EdgeAdjEqRel G iff for e1, e2 being object holds
( [e1,e2] in b2 iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) );

:: deftheorem Def4 defines DEdgeAdjEqRel GLIB_009:def 4 :
for G being _Graph
for b2 being Equivalence_Relation of (the_Edges_of G) holds
( b2 = DEdgeAdjEqRel G iff for e1, e2 being object holds
( [e1,e2] in b2 iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) );

theorem :: GLIB_009:69
for G being _Graph holds DEdgeAdjEqRel G c= EdgeAdjEqRel G
proof end;

theorem :: GLIB_009:70
for G being _Graph holds
( G is non-multi iff EdgeAdjEqRel G = id (the_Edges_of G) )
proof end;

theorem :: GLIB_009:71
for G being _Graph holds
( G is non-Dmulti iff DEdgeAdjEqRel G = id (the_Edges_of G) )
proof end;

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

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

definition
let G be _Graph;
mode RepEdgeSelection of G -> Subset of (the_Edges_of G) means :Def5: :: GLIB_009:def 5
 for v, w, e0 being object st e0 Joins v,w,G holds
ex e being object st
( e Joins v,w,G & e in it & ( for e9 being object st e9 Joins v,w,G & e9 in it holds
e9 = e ) );
existence
ex b1 being Subset of (the_Edges_of G) st
for v, w, e0 being object st e0 Joins v,w,G holds
ex e being object st
( e Joins v,w,G & e in b1 & ( for e9 being object st e9 Joins v,w,G & e9 in b1 holds
e9 = e ) )
proof end;
mode RepDEdgeSelection of G -> Subset of (the_Edges_of G) means :Def6: :: GLIB_009:def 6
 for v, w, e0 being object st e0 DJoins v,w,G holds
ex e being object st
( e DJoins v,w,G & e in it & ( for e9 being object st e9 DJoins v,w,G & e9 in it holds
e9 = e ) );
existence
ex b1 being Subset of (the_Edges_of G) st
for v, w, e0 being object st e0 DJoins v,w,G holds
ex e being object st
( e DJoins v,w,G & e in b1 & ( for e9 being object st e9 DJoins v,w,G & e9 in b1 holds
e9 = e ) )
proof end;
end;

:: deftheorem Def5 defines RepEdgeSelection GLIB_009:def 5 :
for G being _Graph
for b2 being Subset of (the_Edges_of G) holds
( b2 is RepEdgeSelection of G iff for v, w, e0 being object st e0 Joins v,w,G holds
ex e being object st
( e Joins v,w,G & e in b2 & ( for e9 being object st e9 Joins v,w,G & e9 in b2 holds
e9 = e ) ) );

:: deftheorem Def6 defines RepDEdgeSelection GLIB_009:def 6 :
for G being _Graph
for b2 being Subset of (the_Edges_of G) holds
( b2 is RepDEdgeSelection of G iff for v, w, e0 being object st e0 DJoins v,w,G holds
ex e being object st
( e DJoins v,w,G & e in b2 & ( for e9 being object st e9 DJoins v,w,G & e9 in b2 holds
e9 = e ) ) );

registration
let G be edgeless _Graph;
cluster -> empty for RepEdgeSelection of G;
coherence
for b1 being RepEdgeSelection of G holds b1 is empty
proof end;
cluster -> empty for RepDEdgeSelection of G;
coherence
for b1 being RepDEdgeSelection of G holds b1 is empty
proof end;
end;

registration
let G be non edgeless _Graph;
cluster -> non empty for RepEdgeSelection of G;
coherence
for b1 being RepEdgeSelection of G holds not b1 is empty
proof end;
cluster -> non empty for RepDEdgeSelection of G;
coherence
for b1 being RepDEdgeSelection of G holds not b1 is empty
proof end;
end;

theorem Th72: :: GLIB_009:72
for G being _Graph
for E1 being RepDEdgeSelection of G ex E2 being RepEdgeSelection of G st E2 c= E1
proof end;

theorem Th73: :: GLIB_009:73
for G being _Graph
for E2 being RepEdgeSelection of G ex E1 being RepDEdgeSelection of G st E2 c= E1
proof end;

theorem Th74: :: GLIB_009:74
for G being non-multi _Graph
for E being RepEdgeSelection of G holds E = the_Edges_of G
proof end;

theorem Th75: :: GLIB_009:75
for G being _Graph st ex E being RepEdgeSelection of G st E = the_Edges_of G holds
G is non-multi
proof end;

theorem Th76: :: GLIB_009:76
for G being non-Dmulti _Graph
for E being RepDEdgeSelection of G holds E = the_Edges_of G
proof end;

theorem Th77: :: GLIB_009:77
for G being _Graph st ex E being RepDEdgeSelection of G st E = the_Edges_of G holds
G is non-Dmulti
proof end;

theorem Th78: :: GLIB_009:78
for G1 being _Graph
for G2 being Subgraph of G1
for E being RepEdgeSelection of G1 st E c= the_Edges_of G2 holds
E is RepEdgeSelection of G2
proof end;

theorem Th79: :: GLIB_009:79
for G1 being _Graph
for G2 being Subgraph of G1
for E being RepDEdgeSelection of G1 st E c= the_Edges_of G2 holds
E is RepDEdgeSelection of G2
proof end;

theorem Th80: :: GLIB_009:80
for G1 being _Graph
for G2 being Subgraph of G1
for E2 being RepEdgeSelection of G2 ex E1 being RepEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)
proof end;

theorem Th81: :: GLIB_009:81
for G1 being _Graph
for G2 being Subgraph of G1
for E2 being RepDEdgeSelection of G2 ex E1 being RepDEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)
proof end;

theorem Th82: :: GLIB_009:82
for G1 being _Graph
for E1 being RepEdgeSelection of G1
for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1
for E2 being RepEdgeSelection of G2 holds E1 = E2
proof end;

theorem Th83: :: GLIB_009:83
for G1 being _Graph
for E1 being RepDEdgeSelection of G1
for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1
for E2 being RepDEdgeSelection of G2 holds E1 = E2
proof end;

theorem Th84: :: GLIB_009:84
for G1 being _Graph
for E1 being RepDEdgeSelection of G1
for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1
for E2 being RepEdgeSelection of G2 holds
( E2 c= E1 & E2 is RepEdgeSelection of G1 )
proof end;

theorem Th85: :: GLIB_009:85
for G being _Graph
for E1, E2 being RepEdgeSelection of G ex f being one-to-one Function st
( dom f = E1 & rng f = E2 & ( for e, v, w being object st e in E1 holds
( e Joins v,w,G iff f . e Joins v,w,G ) ) )
proof end;

theorem :: GLIB_009:86
for G being _Graph
for E1, E2 being RepEdgeSelection of G holds card E1 = card E2
proof end;

theorem Th87: :: GLIB_009:87
for G being _Graph
for E1, E2 being RepDEdgeSelection of G ex f being one-to-one Function st
( dom f = E1 & rng f = E2 & ( for e, v, w being object st e in E1 holds
( e DJoins v,w,G iff f . e DJoins v,w,G ) ) )
proof end;

theorem :: GLIB_009:88
for G being _Graph
for E1, E2 being RepDEdgeSelection of G holds card E1 = card E2
proof end;

definition
let G be _Graph;
mode removeParallelEdges of G -> Subgraph of G means :Def7: :: GLIB_009:def 7
 ex E being RepEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E;
existence
ex b1 being Subgraph of G ex E being RepEdgeSelection of G st b1 is inducedSubgraph of G, the_Vertices_of G,E
proof end;
mode removeDParallelEdges of G -> Subgraph of G means :Def8: :: GLIB_009:def 8
 ex E being RepDEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E;
existence
ex b1 being Subgraph of G ex E being RepDEdgeSelection of G st b1 is inducedSubgraph of G, the_Vertices_of G,E
proof end;
end;

:: deftheorem Def7 defines removeParallelEdges GLIB_009:def 7 :
for G being _Graph
for b2 being Subgraph of G holds
( b2 is removeParallelEdges of G iff ex E being RepEdgeSelection of G st b2 is inducedSubgraph of G, the_Vertices_of G,E );

:: deftheorem Def8 defines removeDParallelEdges GLIB_009:def 8 :
for G being _Graph
for b2 being Subgraph of G holds
( b2 is removeDParallelEdges of G iff ex E being RepDEdgeSelection of G st b2 is inducedSubgraph of G, the_Vertices_of G,E );

registration
let G be _Graph;
cluster -> non-multi spanning for removeParallelEdges of G;
coherence
for b1 being removeParallelEdges of G holds
( b1 is spanning & b1 is non-multi )
proof end;
cluster -> non-Dmulti spanning for removeDParallelEdges of G;
coherence
for b1 being removeDParallelEdges of G holds
( b1 is spanning & b1 is non-Dmulti )
proof end;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for removeParallelEdges of G;
existence
ex b1 being removeParallelEdges of G st b1 is plain
proof end;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for removeDParallelEdges of G;
existence
ex b1 being removeDParallelEdges of G st b1 is plain
proof end;
end;

registration
let G be loopless _Graph;
cluster -> simple for removeParallelEdges of G;
coherence
for b1 being removeParallelEdges of G holds b1 is simple ;
cluster -> Dsimple for removeDParallelEdges of G;
coherence
for b1 being removeDParallelEdges of G holds b1 is Dsimple ;
end;

theorem :: GLIB_009:89
for G1 being non-multi _Graph
for G2 being _Graph holds
( G1 == G2 iff G2 is removeParallelEdges of G1 )
proof end;

theorem :: GLIB_009:90
for G1 being non-Dmulti _Graph
for G2 being _Graph holds
( G1 == G2 iff G2 is removeDParallelEdges of G1 )
proof end;

theorem Th91: :: GLIB_009:91
for G1, G2 being _Graph
for G3 being removeParallelEdges of G1 st G1 == G2 holds
G3 is removeParallelEdges of G2
proof end;

theorem :: GLIB_009:92
for G1, G2 being _Graph
for G3 being removeDParallelEdges of G1 st G1 == G2 holds
G3 is removeDParallelEdges of G2
proof end;

theorem Th93: :: GLIB_009:93
for G1, G2 being _Graph
for G3 being removeParallelEdges of G1 st G2 == G3 holds
G2 is removeParallelEdges of G1
proof end;

theorem :: GLIB_009:94
for G1, G2 being _Graph
for G3 being removeDParallelEdges of G1 st G2 == G3 holds
G2 is removeDParallelEdges of G1
proof end;

theorem Th95: :: GLIB_009:95
for G1 being _Graph
for G2 being removeDParallelEdges of G1
for G3 being removeParallelEdges of G2 holds G3 is removeParallelEdges of G1
proof end;

theorem Th96: :: GLIB_009:96
for G1 being _Graph
for G2 being removeDParallelEdges of G1 ex G3 being removeParallelEdges of G1 st G3 is removeParallelEdges of G2
proof end;

theorem Th97: :: GLIB_009:97
for G1 being _Graph
for G3 being removeParallelEdges of G1 ex G2 being removeDParallelEdges of G1 st G3 is removeParallelEdges of G2
proof end;

registration
let G be complete _Graph;
cluster -> complete for removeParallelEdges of G;
coherence
for b1 being removeParallelEdges of G holds b1 is complete
proof end;
cluster -> complete for removeDParallelEdges of G;
coherence
for b1 being removeDParallelEdges of G holds b1 is complete
proof end;
end;

theorem Th98: :: GLIB_009:98
for G1 being _Graph
for G2 being removeParallelEdges of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq()
proof end;

Lm4: for G1 being _Graph
for G2 being removeParallelEdges of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()
proof end;

theorem Th99: :: GLIB_009:99
for G1 being _Graph
for G2 being removeDParallelEdges of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq()
proof end;

Lm5: for G1 being _Graph
for G2 being removeDParallelEdges of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()
proof end;

theorem Th100: :: GLIB_009:100
for G1 being _Graph
for G2 being removeParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
proof end;

theorem Th101: :: GLIB_009:101
for G1 being _Graph
for G2 being removeDParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
proof end;

registration
let G be connected _Graph;
cluster -> connected for removeParallelEdges of G;
coherence
for b1 being removeParallelEdges of G holds b1 is connected
proof end;
cluster -> connected for removeDParallelEdges of G;
coherence
for b1 being removeDParallelEdges of G holds b1 is connected
proof end;
end;

registration
let G be non connected _Graph;
cluster -> non connected for removeParallelEdges of G;
coherence
for b1 being removeParallelEdges of G holds not b1 is connected
proof end;
cluster -> non connected for removeDParallelEdges of G;
coherence
for b1 being removeDParallelEdges of G holds not b1 is connected
proof end;
end;

theorem :: GLIB_009:102
for G1 being _Graph
for G2 being removeParallelEdges of G1 holds G1 .componentSet() = G2 .componentSet()
proof end;

theorem :: GLIB_009:103
for G1 being _Graph
for G2 being removeDParallelEdges of G1 holds G1 .componentSet() = G2 .componentSet()
proof end;

theorem Th104: :: GLIB_009:104
for G1 being _Graph
for G2 being removeParallelEdges of G1 holds G1 .numComponents() = G2 .numComponents()
proof end;

theorem :: GLIB_009:105
for G1 being _Graph
for G2 being removeDParallelEdges of G1 holds G1 .numComponents() = G2 .numComponents()
proof end;

theorem Th106: :: GLIB_009:106
for G1 being _Graph
for G2 being removeParallelEdges of G1 holds
( G1 is chordal iff G2 is chordal )
proof end;

theorem Th107: :: GLIB_009:107
for G1 being _Graph
for G2 being removeDParallelEdges of G1 holds
( G1 is chordal iff G2 is chordal )
proof end;

:: non chordal cluster after non chordal has been clustered with cycles
registration
let G be chordal _Graph;
cluster -> chordal for removeParallelEdges of G;
coherence
for b1 being removeParallelEdges of G holds b1 is chordal by Th106;
cluster -> chordal for removeDParallelEdges of G;
coherence
for b1 being removeDParallelEdges of G holds b1 is chordal by Th107;
end;

:: for cut-vertex property, same as with removeLoops above
theorem Th108: :: GLIB_009:108
for G1 being _Graph
for v being set
for G2 being removeParallelEdges of G1
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is removeParallelEdges of G3
proof end;

theorem Th109: :: GLIB_009:109
for G1 being _Graph
for G2 being removeParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is cut-vertex iff v2 is cut-vertex )
proof end;

theorem Th110: :: GLIB_009:110
for G1 being _Graph
for G2 being removeDParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is cut-vertex iff v2 is cut-vertex )
proof end;

theorem Th111: :: GLIB_009:111
for G1 being _Graph
for G2 being removeParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )
proof end;

theorem Th112: :: GLIB_009:112
for G1 being _Graph
for G2 being removeDParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )
proof end;

theorem Th113: :: GLIB_009:113
for G1 being _Graph
for G2 being removeParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds
v2 is endvertex
proof end;

theorem Th114: :: GLIB_009:114
for G1 being _Graph
for G2 being removeDParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds
v2 is endvertex
proof end;

:: Graphs with Loops and parallel Edges removed
definition
let G be _Graph;
mode SimpleGraph of G -> Subgraph of G means :Def9: :: GLIB_009:def 9
 ex E being RepEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops());
existence
ex b1 being Subgraph of G ex E being RepEdgeSelection of G st b1 is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops())
proof end;
mode DSimpleGraph of G -> Subgraph of G means :Def10: :: GLIB_009:def 10
 ex E being RepDEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops());
existence
ex b1 being Subgraph of G ex E being RepDEdgeSelection of G st b1 is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops())
proof end;
end;

:: deftheorem Def9 defines SimpleGraph GLIB_009:def 9 :
for G being _Graph
for b2 being Subgraph of G holds
( b2 is SimpleGraph of G iff ex E being RepEdgeSelection of G st b2 is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops()) );

:: deftheorem Def10 defines DSimpleGraph GLIB_009:def 10 :
for G being _Graph
for b2 being Subgraph of G holds
( b2 is DSimpleGraph of G iff ex E being RepDEdgeSelection of G st b2 is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops()) );

theorem :: GLIB_009:115
for G1 being _Graph
for G2 being removeParallelEdges of G1
for G3 being removeLoops of G2 holds G3 is SimpleGraph of G1
proof end;

theorem :: GLIB_009:116
for G1 being _Graph
for G2 being removeDParallelEdges of G1
for G3 being removeLoops of G2 holds G3 is DSimpleGraph of G1
proof end;

theorem Th117: :: GLIB_009:117
for G1 being _Graph
for G2 being removeLoops of G1
for G3 being removeParallelEdges of G2 holds G3 is SimpleGraph of G1
proof end;

theorem Th118: :: GLIB_009:118
for G1 being _Graph
for G2 being removeLoops of G1
for G3 being removeDParallelEdges of G2 holds G3 is DSimpleGraph of G1
proof end;

theorem Th119: :: GLIB_009:119
for G1 being _Graph
for G3 being SimpleGraph of G1 ex G2 being removeParallelEdges of G1 st G3 is removeLoops of G2
proof end;

theorem Th120: :: GLIB_009:120
for G1 being _Graph
for G3 being DSimpleGraph of G1 ex G2 being removeDParallelEdges of G1 st G3 is removeLoops of G2
proof end;

theorem Th121: :: GLIB_009:121
for G1 being _Graph
for G2 being removeLoops of G1
for G3 being SimpleGraph of G1 holds G3 is removeParallelEdges of G2
proof end;

theorem Th122: :: GLIB_009:122
for G1 being _Graph
for G2 being removeLoops of G1
for G3 being DSimpleGraph of G1 holds G3 is removeDParallelEdges of G2
proof end;

theorem Th123: :: GLIB_009:123
for G1 being loopless _Graph
for G2 being _Graph holds
( G2 is SimpleGraph of G1 iff G2 is removeParallelEdges of G1 )
proof end;

theorem :: GLIB_009:124
for G1 being loopless _Graph
for G2 being _Graph holds
( G2 is DSimpleGraph of G1 iff G2 is removeDParallelEdges of G1 )
proof end;

theorem :: GLIB_009:125
for G1 being non-multi _Graph
for G2 being _Graph holds
( G2 is SimpleGraph of G1 iff G2 is removeLoops of G1 )
proof end;

theorem :: GLIB_009:126
for G1 being non-Dmulti _Graph
for G2 being _Graph holds
( G2 is DSimpleGraph of G1 iff G2 is removeLoops of G1 )
proof end;

registration
let G be _Graph;
cluster -> loopless non-multi simple spanning for SimpleGraph of G;
coherence
for b1 being SimpleGraph of G holds
( b1 is spanning & b1 is loopless & b1 is non-multi & b1 is simple )
proof end;
cluster -> loopless non-Dmulti Dsimple spanning for DSimpleGraph of G;
coherence
for b1 being DSimpleGraph of G holds
( b1 is spanning & b1 is loopless & b1 is non-Dmulti & b1 is Dsimple )
proof end;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for SimpleGraph of G;
existence
ex b1 being SimpleGraph of G st b1 is plain
proof end;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for DSimpleGraph of G;
existence
ex b1 being DSimpleGraph of G st b1 is plain
proof end;
end;

theorem :: GLIB_009:127
for G1 being simple _Graph
for G2 being _Graph holds
( G1 == G2 iff G2 is SimpleGraph of G1 )
proof end;

theorem :: GLIB_009:128
for G1 being Dsimple _Graph
for G2 being _Graph holds
( G1 == G2 iff G2 is DSimpleGraph of G1 )
proof end;

theorem :: GLIB_009:129
for G1, G2 being _Graph
for G3 being SimpleGraph of G1 st G1 == G2 holds
G3 is SimpleGraph of G2
proof end;

theorem :: GLIB_009:130
for G1, G2 being _Graph
for G3 being DSimpleGraph of G1 st G1 == G2 holds
G3 is DSimpleGraph of G2
proof end;

theorem :: GLIB_009:131
for G1, G2 being _Graph
for G3 being SimpleGraph of G1 st G2 == G3 holds
G2 is SimpleGraph of G1
proof end;

theorem :: GLIB_009:132
for G1, G2 being _Graph
for G3 being DSimpleGraph of G1 st G2 == G3 holds
G2 is DSimpleGraph of G1
proof end;

theorem Th133: :: GLIB_009:133
for G1 being _Graph
for G2 being DSimpleGraph of G1
for G3 being SimpleGraph of G2 holds G3 is SimpleGraph of G1
proof end;

theorem :: GLIB_009:134
for G1 being _Graph
for G2 being DSimpleGraph of G1 ex G3 being SimpleGraph of G1 st G3 is SimpleGraph of G2
proof end;

theorem :: GLIB_009:135
for G1 being _Graph
for G3 being SimpleGraph of G1 ex G2 being DSimpleGraph of G1 st G3 is SimpleGraph of G2
proof end;

registration
let G be complete _Graph;
cluster -> complete for SimpleGraph of G;
coherence
for b1 being SimpleGraph of G holds b1 is complete
proof end;
cluster -> complete for DSimpleGraph of G;
coherence
for b1 being DSimpleGraph of G holds b1 is complete
proof end;
end;

theorem Th136: :: GLIB_009:136
for G1 being _Graph
for G2 being SimpleGraph of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()
proof end;

theorem Th137: :: GLIB_009:137
for G1 being _Graph
for G2 being DSimpleGraph of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()
proof end;

theorem Th138: :: GLIB_009:138
for G1 being _Graph
for G2 being SimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
proof end;

theorem Th139: :: GLIB_009:139
for G1 being _Graph
for G2 being DSimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
proof end;

registration
let G be connected _Graph;
cluster -> connected for SimpleGraph of G;
coherence
for b1 being SimpleGraph of G holds b1 is connected
proof end;
cluster -> connected for DSimpleGraph of G;
coherence
for b1 being DSimpleGraph of G holds b1 is connected
proof end;
end;

registration
let G be non connected _Graph;
cluster -> non connected for SimpleGraph of G;
coherence
for b1 being SimpleGraph of G holds not b1 is connected
proof end;
cluster -> non connected for DSimpleGraph of G;
coherence
for b1 being DSimpleGraph of G holds not b1 is connected
proof end;
end;

theorem :: GLIB_009:140
for G1 being _Graph
for G2 being SimpleGraph of G1 holds G1 .componentSet() = G2 .componentSet()
proof end;

theorem :: GLIB_009:141
for G1 being _Graph
for G2 being DSimpleGraph of G1 holds G1 .componentSet() = G2 .componentSet()
proof end;

theorem :: GLIB_009:142
for G1 being _Graph
for G2 being SimpleGraph of G1 holds G1 .numComponents() = G2 .numComponents()
proof end;

theorem :: GLIB_009:143
for G1 being _Graph
for G2 being DSimpleGraph of G1 holds G1 .numComponents() = G2 .numComponents()
proof end;

theorem Th144: :: GLIB_009:144
for G1 being _Graph
for G2 being SimpleGraph of G1 holds
( G1 is chordal iff G2 is chordal )
proof end;

theorem Th145: :: GLIB_009:145
for G1 being _Graph
for G2 being DSimpleGraph of G1 holds
( G1 is chordal iff G2 is chordal )
proof end;

:: non chordal cluster after non chordal has been clustered with cycles
registration
let G be chordal _Graph;
cluster -> chordal for SimpleGraph of G;
coherence
for b1 being SimpleGraph of G holds b1 is chordal by Th144;
cluster -> chordal for DSimpleGraph of G;
coherence
for b1 being DSimpleGraph of G holds b1 is chordal by Th145;
end;

theorem :: GLIB_009:146
for G1 being _Graph
for G2 being SimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is cut-vertex iff v2 is cut-vertex )
proof end;

theorem :: GLIB_009:147
for G1 being _Graph
for G2 being DSimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is cut-vertex iff v2 is cut-vertex )
proof end;

theorem :: GLIB_009:148
for G1 being loopless _Graph
for G2 being SimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )
proof end;

theorem :: GLIB_009:149
for G1 being loopless _Graph
for G2 being DSimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )
proof end;

theorem :: GLIB_009:150
for G1 being _Graph
for G2 being SimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds
v2 is endvertex
proof end;

theorem :: GLIB_009:151
for G1 being _Graph
for G2 being DSimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds
v2 is endvertex
proof end;