:: by Sebastian Koch
::
:: Copyright (c) 2018-2021 Association of Mizar Users

definition
let G be _Graph;
let E be set ;
mode reverseEdgeDirections of G,E -> _Graph means :Def1: :: GLIB_007:def 1
( the_Vertices_of it = the_Vertices_of G & the_Edges_of it = the_Edges_of G & the_Source_of it = () +* (() | E) & the_Target_of it = () +* (() | E) ) if E c= the_Edges_of G
otherwise it == G;
existence
( ( E c= the_Edges_of G implies ex b1 being _Graph st
( the_Vertices_of b1 = the_Vertices_of G & the_Edges_of b1 = the_Edges_of G & the_Source_of b1 = () +* (() | E) & the_Target_of b1 = () +* (() | E) ) ) & ( not E c= the_Edges_of G implies ex b1 being _Graph st b1 == G ) )
proof end;
consistency
for b1 being _Graph holds verum
;
end;

:: deftheorem Def1 defines reverseEdgeDirections GLIB_007:def 1 :
for G being _Graph
for E being set
for b3 being _Graph holds
( ( E c= the_Edges_of G implies ( b3 is reverseEdgeDirections of G,E iff ( the_Vertices_of b3 = the_Vertices_of G & the_Edges_of b3 = the_Edges_of G & the_Source_of b3 = () +* (() | E) & the_Target_of b3 = () +* (() | E) ) ) ) & ( not E c= the_Edges_of G implies ( b3 is reverseEdgeDirections of G,E iff b3 == G ) ) );

definition end;

theorem :: GLIB_007:1
for G being _Graph
for E being set
for G1, G2 being reverseEdgeDirections of G,E holds G1 == G2
proof end;

theorem Th2: :: GLIB_007:2
for G, G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G,E st G1 == G2 holds
G2 is reverseEdgeDirections of G,E
proof end;

theorem Th3: :: GLIB_007:3
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E holds G2 is reverseEdgeDirections of G1,E
proof end;

theorem Th4: :: GLIB_007:4
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E holds
( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )
proof end;

theorem Th5: :: GLIB_007:5
for G2 being _Graph
for G1 being reverseEdgeDirections of G2 holds G2 is reverseEdgeDirections of G1
proof end;

theorem Th6: :: GLIB_007:6
for G2 being _trivial _Graph
for E being set
for G1 being _Graph holds
( G1 == G2 iff G1 is reverseEdgeDirections of G2,E )
proof end;

Lm1: for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & e in E & e DJoins v1,v2,G2 holds
e DJoins v2,v1,G1

proof end;

theorem Th7: :: GLIB_007:7
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & e in E holds
( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )
proof end;

Lm2: for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & not e in E & e DJoins v1,v2,G2 holds
e DJoins v1,v2,G1

proof end;

theorem Th8: :: GLIB_007:8
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & not e in E holds
( e DJoins v1,v2,G2 iff e DJoins v1,v2,G1 )
proof end;

Lm3: for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E st E c= the_Edges_of G2 holds
for v1, e, v2 being object st e Joins v1,v2,G2 holds
e Joins v1,v2,G1

proof end;

theorem Th9: :: GLIB_007:9
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object holds
( e Joins v1,v2,G2 iff e Joins v1,v2,G1 )
proof end;

theorem Th10: :: GLIB_007:10
for G2 being _Graph
for E being set
for v being object
for G1 being reverseEdgeDirections of G2,E holds
( v is Vertex of G1 iff v is Vertex of G2 ) by Th4;

theorem Th11: :: GLIB_007:11
for G2 being _Graph
for E, V being set
for G1 being reverseEdgeDirections of G2,E holds G1 .edgesBetween V = G2 .edgesBetween V
proof end;

theorem Th12: :: GLIB_007:12
for G2 being _Graph
for E, V being set
for G1 being reverseEdgeDirections of G2,E holds G1 .edgesInOut V = G2 .edgesInOut V
proof end;

theorem Th13: :: GLIB_007:13
for G2 being _Graph
for E, V being set
for G1 being reverseEdgeDirections of G2,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v1 .edgesInOut() = v2 .edgesInOut()
proof end;

theorem Th14: :: GLIB_007:14
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2 holds W2 is Walk of G1
proof end;

theorem Th15: :: GLIB_007:15
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for W1 being Walk of G1 holds W1 is Walk of G2
proof end;

theorem Th16: :: GLIB_007:16
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2
for W1 being Walk of G1 st E c= the_Edges_of G2 & W1 = W2 & W2 .edges() c= E holds
( W1 is directed iff W2 .reverse() is directed )
proof end;

theorem :: GLIB_007:17
for G2 being _Graph
for G1 being reverseEdgeDirections of G2
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 holds
( W1 is directed iff W2 .reverse() is directed )
proof end;

Lm4: for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 & W1 is chordal holds
W2 is chordal

proof end;

theorem Th18: :: GLIB_007:18
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 holds
( W1 is chordal iff W2 is chordal )
proof end;

theorem Th19: :: GLIB_007:19
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, v2 being object holds
( ex W1 being Walk of G1 st W1 is_Walk_from v1,v2 iff ex W2 being Walk of G2 st W2 is_Walk_from v1,v2 )
proof end;

theorem Th20: :: GLIB_007:20
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
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 Th21: :: GLIB_007:21
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E holds
( G1 .componentSet() = G2 .componentSet() & G1 .numComponents() = G2 .numComponents() )
proof end;

registration
let G be _trivial _Graph;
let E be set ;
cluster -> _trivial for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is _trivial
proof end;
end;

registration
let G be non _trivial _Graph;
let E be set ;
cluster -> non _trivial for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds not b1 is _trivial
proof end;
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 (partially) reversed edge directions
theorem Th22: :: GLIB_007:22
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v being set
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is reverseEdgeDirections of G3,E \ ()
proof end;

Lm5: for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) )

proof end;

theorem :: GLIB_007:23
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies v2 is isolated ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) & ( v2 is cut-vertex implies v1 is cut-vertex ) )
proof end;

theorem :: GLIB_007:24
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E holds
( G1 .order() = G2 .order() & G1 .size() = G2 .size() )
proof end;

theorem Th25: :: GLIB_007:25
for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E st E c= the_Edges_of G2 & G2 is non-Dmulti & ( for e1, e2, v1, v2 being object st e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 & not ( e1 in E & e2 in E ) holds
( not e1 in E & not e2 in E ) ) holds
G1 is non-Dmulti
proof end;

registration
let G be non-Dmulti _Graph;
coherence
for b1 being reverseEdgeDirections of G holds b1 is non-Dmulti
proof end;
end;

registration
let G be non non-Dmulti _Graph;
cluster -> non non-Dmulti for reverseEdgeDirections of G, the_Edges_of G;
coherence
for b1 being reverseEdgeDirections of G holds not b1 is non-Dmulti
proof end;
end;

registration
let G be non-multi _Graph;
let E be set ;
cluster -> non-multi for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is non-multi
proof end;
end;

registration
let G be non non-multi _Graph;
let E be set ;
cluster -> non non-multi for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds not b1 is non-multi
proof end;
end;

registration
let G be loopless _Graph;
let E be set ;
cluster -> loopless for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is loopless
proof end;
end;

registration
let G be non loopless _Graph;
let E be set ;
cluster -> non loopless for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds not b1 is loopless
proof end;
end;

registration
let G be connected _Graph;
let E be set ;
cluster -> connected for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is connected
proof end;
end;

registration
let G be non connected _Graph;
let E be set ;
cluster -> non connected for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds not b1 is connected
proof end;
end;

registration
let G be acyclic _Graph;
let E be set ;
cluster -> acyclic for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is acyclic
proof end;
end;

registration
let G be non acyclic _Graph;
let E be set ;
cluster -> non acyclic for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds not b1 is acyclic
proof end;
end;

registration
let G be complete _Graph;
let E be set ;
cluster -> complete for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is complete
proof end;
end;

registration
let G be non complete _Graph;
let E be set ;
cluster -> non complete for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds not b1 is complete
proof end;
end;

registration
let G be chordal _Graph;
let E be set ;
cluster -> chordal for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is chordal
proof end;
end;

:: "non"-version of this cluster has to wait
:: because non chordal existence will be proven with cycle graphs
registration
let G be _finite _Graph;
let E be set ;
cluster -> _finite for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is _finite
proof end;
end;

registration
let G be non _finite _Graph;
let E be set ;
cluster -> non _finite for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds not b1 is _finite
proof end;
end;

theorem Th26: :: GLIB_007:26
for G2 being _Graph
for G1 being reverseEdgeDirections of G2 holds
( the_Source_of G1 = the_Target_of G2 & the_Target_of G1 = the_Source_of G2 )
proof end;

theorem :: GLIB_007:27
for G2 being _Graph
for G1 being reverseEdgeDirections of G2
for v1, e, v2 being object holds
( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )
proof end;

Lm6: for X, Y being set holds X /\ (Y --> X) = {}
proof end;

Lm7: for X, Y being set
for x being object st X /\ Y = {} & x in X holds
not x in Y

by XBOOLE_0:def 4;

:: we need a lot of edges, so we take the freedom
:: to specify them within the definition
definition
let G be _Graph;
let v be object ;
let V be set ;
mode addAdjVertexToAll of G,v,V -> Supergraph of G means :Def2: :: GLIB_007:def 2
( the_Vertices_of it = () \/ {v} & the_Edges_of it = () \/ (V --> ()) & the_Source_of it = () +* ((V --> ()) --> v) & the_Target_of it = () +* (pr1 (V,{()})) ) if ( V c= the_Vertices_of G & not v in the_Vertices_of G )
otherwise it == G;
existence
( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ex b1 being Supergraph of G st
( the_Vertices_of b1 = () \/ {v} & the_Edges_of b1 = () \/ (V --> ()) & the_Source_of b1 = () +* ((V --> ()) --> v) & the_Target_of b1 = () +* (pr1 (V,{()})) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ex b1 being Supergraph of G st b1 == G ) )
proof end;
consistency
for b1 being Supergraph of G holds verum
;
end;

for G being _Graph
for v being object
for V being set
for b4 being Supergraph of G holds
( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( b4 is addAdjVertexToAll of G,v,V iff ( the_Vertices_of b4 = () \/ {v} & the_Edges_of b4 = () \/ (V --> ()) & the_Source_of b4 = () +* ((V --> ()) --> v) & the_Target_of b4 = () +* (pr1 (V,{()})) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ( b4 is addAdjVertexToAll of G,v,V iff b4 == G ) ) );

definition
let G be _Graph;
let v be object ;
let V be set ;
mode addAdjVertexFromAll of G,v,V -> Supergraph of G means :Def3: :: GLIB_007:def 3
( the_Vertices_of it = () \/ {v} & the_Edges_of it = () \/ (V --> ()) & the_Source_of it = () +* (pr1 (V,{()})) & the_Target_of it = () +* ((V --> ()) --> v) ) if ( V c= the_Vertices_of G & not v in the_Vertices_of G )
otherwise it == G;
existence
( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ex b1 being Supergraph of G st
( the_Vertices_of b1 = () \/ {v} & the_Edges_of b1 = () \/ (V --> ()) & the_Source_of b1 = () +* (pr1 (V,{()})) & the_Target_of b1 = () +* ((V --> ()) --> v) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ex b1 being Supergraph of G st b1 == G ) )
proof end;
consistency
for b1 being Supergraph of G holds verum
;
end;

for G being _Graph
for v being object
for V being set
for b4 being Supergraph of G holds
( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( b4 is addAdjVertexFromAll of G,v,V iff ( the_Vertices_of b4 = () \/ {v} & the_Edges_of b4 = () \/ (V --> ()) & the_Source_of b4 = () +* (pr1 (V,{()})) & the_Target_of b4 = () +* ((V --> ()) --> v) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ( b4 is addAdjVertexFromAll of G,v,V iff b4 == G ) ) );

definition end;

theorem :: GLIB_007:28
for G being _Graph
for v being object
for V being set
proof end;

theorem :: GLIB_007:29
for G being _Graph
for v being object
for V being set
proof end;

theorem :: GLIB_007:30
for G, G2 being _Graph
for v being object
for V being set
proof end;

theorem :: GLIB_007:31
for G, G2 being _Graph
for v being object
for V being set
proof end;

theorem Th32: :: GLIB_007:32
for G being _Graph
for v being object
for V being set
( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )
proof end;

theorem Th33: :: GLIB_007:33
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .edgesOutOf {v} = V --> ()
proof end;

theorem Th34: :: GLIB_007:34
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .edgesInto {v} = V --> ()
proof end;

theorem Th35: :: GLIB_007:35
for G being _Graph
for v being object
for V being set
for G2 being addAdjVertexFromAll of G,v,V st V c= the_Vertices_of G & not v in the_Vertices_of G holds
( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )
proof end;

theorem :: GLIB_007:36
for G being _Graph
for v being object
for V being set
for v1, e, v2 being object holds
( e Joins v1,v2,G1 iff e Joins v1,v2,G2 )
proof end;

theorem :: GLIB_007:37
for G being _Graph
for v being object
for V being set
for w being object holds
( w is Vertex of G1 iff w is Vertex of G2 ) by Th32;

theorem Th38: :: GLIB_007:38
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e1, u being object holds
( not e1 DJoins u,v,G1 & ( not u in V implies not e1 DJoins v,u,G1 ) & ( for e2 being object st e1 DJoins v,u,G1 & e2 DJoins v,u,G1 holds
e1 = e2 ) )
proof end;

theorem Th39: :: GLIB_007:39
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e1, u being object holds
( not e1 DJoins v,u,G1 & ( not u in V implies not e1 DJoins u,v,G1 ) & ( for e2 being object st e1 DJoins u,v,G1 & e2 DJoins u,v,G1 holds
e1 = e2 ) )
proof end;

theorem Th40: :: GLIB_007:40
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e, v1, v2 being object st v1 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2
proof end;

theorem Th41: :: GLIB_007:41
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e, v1, v2 being object st v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2
proof end;

theorem Th42: :: GLIB_007:42
for G2 being _Graph
for v being object
for V being set
for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds
[v1,()] DJoins v,v1,G1
proof end;

theorem Th43: :: GLIB_007:43
for G2 being _Graph
for v being object
for V being set
for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds
[v1,()] DJoins v1,v,G1
proof end;

theorem :: GLIB_007:44
for G being _Graph
for v being object
for V being set
for W1 being Walk of G1 holds W1 is Walk of G2
proof end;

theorem :: GLIB_007:45
for G being _Graph
for v being object
for V being set
for W2 being Walk of G2 holds W2 is Walk of G1
proof end;

Lm8: for V, E being set holds card V = card (V --> E)
proof end;

Lm9: for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( for e being object holds
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2 ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = () \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) ) )

proof end;

Lm10: for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( for e being object holds
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2 ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = () \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) ) )

proof end;

:: If someone could come up with an easier redefinition
:: without using isomorphisms, it would be appreciated.
:: Note that each property of the definition is used within
:: the next three theorems.
:: Also note that about half the definition is implied when V is finite
:: because of the card-property. However, this will not be proved here.
:: to give a constructive characterization of star and wheel graphs
:: without having to use isomorphisms.
definition
let G be _Graph;
let v be object ;
let V be set ;
mode addAdjVertexAll of G,v,V -> Supergraph of G means :Def4: :: GLIB_007:def 4
( the_Vertices_of it = () \/ {v} & ( for e being object holds
( not e Joins v,v,it & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,it ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,it holds
e DJoins v1,v2,G ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G & the_Edges_of it = () \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,it & ( for e2 being object st e2 Joins v1,v,it holds
e1 = e2 ) ) ) ) ) if ( V c= the_Vertices_of G & not v in the_Vertices_of G )
otherwise it == G;
existence
( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ex b1 being Supergraph of G st
( the_Vertices_of b1 = () \/ {v} & ( for e being object holds
( not e Joins v,v,b1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,b1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,b1 holds
e DJoins v1,v2,G ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G & the_Edges_of b1 = () \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,b1 & ( for e2 being object st e2 Joins v1,v,b1 holds
e1 = e2 ) ) ) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ex b1 being Supergraph of G st b1 == G ) )
proof end;
consistency
for b1 being Supergraph of G holds verum
;
end;

for G being _Graph
for v being object
for V being set
for b4 being Supergraph of G holds
( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( b4 is addAdjVertexAll of G,v,V iff ( the_Vertices_of b4 = () \/ {v} & ( for e being object holds
( not e Joins v,v,b4 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,b4 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,b4 holds
e DJoins v1,v2,G ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G & the_Edges_of b4 = () \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,b4 & ( for e2 being object st e2 Joins v1,v,b4 holds
e1 = e2 ) ) ) ) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ( b4 is addAdjVertexAll of G,v,V iff b4 == G ) ) );

definition
let G be _Graph;
let v be object ;
correctness
;
let V be set ;
coherence
proof end;
coherence
proof end;
end;

theorem Th46: :: GLIB_007:46
for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v, {} holds the_Edges_of G2 = the_Edges_of G1
proof end;

Lm11: for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v, {} st the_Edges_of G2 = {} holds
the_Edges_of G1 = {}

by Th46;

theorem Th47: :: GLIB_007:47
for G2 being _Graph
for v being object
for V being non empty set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
the_Edges_of G1 <> {}
proof end;

theorem :: GLIB_007:48
for G, G2 being _Graph
for v being object
for V being set
proof end;

theorem Th49: :: GLIB_007:49
for G2 being _Graph
for v being object
for V being set
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 holds
e Joins v1,v2,G2
proof end;

theorem Th50: :: GLIB_007:50
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
v is Vertex of G1
proof end;

theorem Th51: :: GLIB_007:51
for G2 being _Graph
for v being object
for V being set
for E being set
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = () \/ E & E misses the_Edges_of G2 & e Joins v1,v2,G1 & not e in the_Edges_of G2 holds
( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )
proof end;

theorem Th52: :: GLIB_007:52
for G2 being _Graph
for v being object
for V being set
for E being set st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = () \/ E & E misses the_Edges_of G2 holds
ex f, g being Function of E,(V \/ {v}) st
( the_Source_of G1 = () +* f & the_Target_of G1 = () +* g & ( for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) )
proof end;

theorem Th53: :: GLIB_007:53
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
the_Edges_of G2 = G1 .edgesBetween ()
proof end;

theorem :: GLIB_007:54
for G2 being _Graph
for v, V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G2 is removeVertex of G1,v
proof end;

theorem Th55: :: GLIB_007:55
for G2 being _Graph
for v being object
proof end;

:: TODO other direction
theorem :: GLIB_007:56
for G2 being _Graph
for v, v1 being object
for G1 being addAdjVertexAll of G2,v,{v1} st v1 in the_Vertices_of G2 & not v in the_Vertices_of G2 holds
ex e being object st
proof end;

Lm12: for G2 being _Graph
for v being object
for V being set
for W being Subset of V
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G1 .edgesBetween (W,{v}) = {} holds
W = {}

proof end;

theorem Th57: :: GLIB_007:57
for G2 being _Graph
for v being object
for V being set
for W being Subset of V
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
ex f being Function of W,(G1 .edgesBetween (W,{v})) st
( f is one-to-one & f is onto & ( for w being object st w in W holds
f . w Joins w,v,G1 ) )
proof end;

theorem Th58: :: GLIB_007:58
for G2 being _Graph
for v being object
for V, E being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & E misses the_Edges_of G2 & the_Edges_of G1 = () \/ E holds
E = G1 .edgesBetween (V,{v})
proof end;

theorem :: GLIB_007:59
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( G1 .edgesBetween (V,{v}) misses the_Edges_of G2 & the_Edges_of G1 = () \/ (G1 .edgesBetween (V,{v})) )
proof end;

theorem Th60: :: GLIB_007:60
for G3 being _Graph
for v being object
for V1, V2 being set
for G2 being removeEdges of G1,(G1 .edgesBetween (V2,{v})) st V1 \/ V2 c= the_Vertices_of G3 & not v in the_Vertices_of G3 & V1 misses V2 holds
proof end;

theorem :: GLIB_007:61
for G3 being _Graph
for v being object
for V being set
for v1 being Vertex of G3
for G1 being addAdjVertexAll of G3,v,V \/ {v1} st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V holds
( not e in the_Edges_of G2 & ( G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v ) )
proof end;

theorem :: GLIB_007:62
for G3 being _Graph
for v being object
for V being set
for v1 being Vertex of G3
for e being object
for G2 being addAdjVertexAll of G3,v,V st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V & not e in the_Edges_of G2 holds
for G1 being _Graph st ( G1 is addEdge of G2,v1,e,v or G1 is addEdge of G2,v,e,v1 ) holds
proof end;

Lm13: for k being odd Element of NAT st 1 < k holds
k - 2 is odd Element of NAT

proof end;

theorem Th63: :: GLIB_007:63
for G2 being _Graph
for v being object
for V being set
for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( W .edges() c= the_Edges_of G2 & W is V5() implies not v in W .vertices() ) & ( not v in W .vertices() implies W .edges() c= the_Edges_of G2 ) )
proof end;

theorem Th64: :: GLIB_007:64
for G2 being _Graph
for v being object
for V being set
for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( ( W .edges() c= the_Edges_of G2 & W is V5() ) or not v in W .vertices() ) holds
W is Walk of G2
proof end;

theorem Th65: :: GLIB_007:65
for G2 being _Graph
for v being object
for V being set
for W being Walk of G1 st W .vertices() c= the_Vertices_of G2 holds
W .edges() c= the_Edges_of G2
proof end;

theorem :: GLIB_007:66
for G being _Graph
for v being object
for V being set
( the_Vertices_of G1 = the_Vertices_of G2 & ( for v1 being Vertex of G1 holds v1 is Vertex of G2 ) )
proof end;

theorem Th67: :: GLIB_007:67
for G being _Graph
for v being object
for V being set
for v1, e1, v2 being object st e1 Joins v1,v2,G1 holds
ex e2 being object st e2 Joins v1,v2,G2
proof end;

:: The closest analogon we can get for
:: theorem for G, v, V for G1, G2 being addAdjVertexToAll of G,v,V
:: holds G1 == G2
:: but also preparation for
:: registration let G, v, V; let G1 being addAdjVertexAll of G,v,V;
:: coming soon
theorem :: GLIB_007:68
for G being _Graph
for v being object
for V being set
for G1, G2 being addAdjVertexAll of G,v,V ex f being Function of (),() st
( f | () = id () & f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )
proof end;

registration
let G be loopless _Graph;
let v be object ;
let V be set ;
coherence
proof end;
end;

registration
let G be non-Dmulti _Graph;
let v be object ;
let V be set ;
coherence
proof end;
end;

registration
let G be non-multi _Graph;
let v be object ;
let V be set ;
coherence
proof end;
end;

registration
let G be Dsimple _Graph;
let v be object ;
let V be set ;
coherence
;
end;

registration
let G be simple _Graph;
let v be object ;
let V be set ;
coherence
;
end;

theorem Th69: :: GLIB_007:69
for G2 being _Graph
for v being object
for V being set
for W being Walk of G1
for v1, v2 being Vertex of G2 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & W .first() = v1 & W .last() = v2 & not v2 in G2 .reachableFrom v1 holds
v in W .vertices()
proof end;

Lm14: for k being odd Element of NAT holds
( (k -' 1) + 1 = k & ( for n being Element of NAT st k <= n holds
k -' 1 < n ) )

proof end;

Lm15: for k, n being odd Element of NAT holds n + (k -' 1) is odd Element of NAT
proof end;

Lm16: ( 1 is odd Element of NAT & 3 is odd Element of NAT )
by ;

:: this means that in each component there is at most one
:: vertex connecting to the new one
theorem :: GLIB_007:70
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G2 is acyclic & ( for G3 being Component of G2
for w1, w2 being Vertex of G3 st w1 in V & w2 in V holds
w1 = w2 ) holds
G1 is acyclic
proof end;

theorem :: GLIB_007:71
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( not G2 is acyclic or ex G3 being Component of G2 ex w1, w2 being Vertex of G3 st
( w1 in V & w2 in V & w1 <> w2 ) ) holds
not G1 is acyclic
proof end;

:: this means that in each component there is at least one
:: vertex connecting to the new one
theorem Th72: :: GLIB_007:72
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( for G3 being Component of G2 ex w being Vertex of G3 st w in V ) holds
G1 is connected
proof end;

registration
let G be connected _Graph;
let v be object ;
let V be non empty set ;
coherence
proof end;
end;

theorem Th73: :: GLIB_007:73
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st
for w being Vertex of G3 holds not w in V holds
not G1 is connected
proof end;

theorem :: GLIB_007:74
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st the_Vertices_of G3 misses V holds
not G1 is connected
proof end;

registration
let G be non connected _Graph;
let v be object ;
coherence
for b1 being addAdjVertexAll of G,v, {} holds not b1 is connected
proof end;
end;

theorem Th75: :: GLIB_007:75
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( G1 is complete iff ( G2 is complete & V = the_Vertices_of G2 ) )
proof end;

registration
let G be complete _Graph;
coherence
for b1 being addAdjVertexAll of G, the_Vertices_of G holds b1 is complete
proof end;
end;

theorem :: GLIB_007:76
for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( G1 .order() = (G2 .order()) + 1 & G1 .size() = (G2 .size()) + (card V) )
proof end;

theorem :: GLIB_007:77
for G2 being _finite _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .order() = (G2 .order()) + 1
proof end;

theorem :: GLIB_007:78
for G2 being _finite _Graph
for v being object
for V being finite set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .size() = (G2 .size()) + (card V)
proof end;

registration
let G be _finite _Graph;
let v be object ;
let V be set ;