:: About Supergraphs, Part {I}
:: by Sebastian Koch
::
:: Received June 29, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users


:: into ABIAN ?
theorem Th1: :: GLIB_006:1
for n being even Integer
for m being odd Integer st n <= m holds
n + 1 <= m
proof end;

:: into ABIAN ?
theorem Th2: :: GLIB_006:2
for n being even Integer
for m being odd Integer st m <= n holds
m + 1 <= n
proof end;

:: into NAT_D ?
theorem Th3: :: GLIB_006:3
for i, j being Nat st i > (i -' 1) + j holds
j = 0
proof end;

:: BEGIN into FINSEQ_6 or JORDAN4 ?
theorem Th6: :: GLIB_006:4
for f, g being FinSequence
for i being Nat st i <= len f & mid (f,i,((i -' 1) + (len g))) = g holds
(i -' 1) + (len g) <= len f
proof end;

Th7: for p being FinSequence
for n being Nat st n in dom p holds
mid (p,n,n) = <*(p . n)*>

by JORDAN4:15;

Th8: for p being FinSequence
for k1, k2 being Nat st k1 < k2 & k1 in dom p holds
mid (p,k1,k2) = <*(p . k1)*> ^ (mid (p,(k1 + 1),k2))

by FINSEQ_6:126;

theorem Th9: :: GLIB_006:5
for p being FinSequence
for n being Nat st n in dom p & n + 1 <= len p holds
mid (p,n,(n + 1)) = <*(p . n),(p . (n + 1))*>
proof end;

theorem Th10: :: GLIB_006:6
for p being FinSequence
for n being Nat st n in dom p & n + 2 <= len p holds
mid (p,n,(n + 2)) = <*(p . n),(p . (n + 1)),(p . (n + 2))*>
proof end;

:: END into FINSEQ_6 or JORDAN 4 ?
:: during research the author noticed the strong similiariy between
:: (m,n)-cut p and smid(p,m,n) (from GRAPH_2 and FINSEQ_8)
:: but no theorems about that will be made here
:: SOLVED: added theorem at the end of FINSEQ_8
:: BEGIN into FINSEQ_8 ?
theorem Th11: :: GLIB_006:7
for D being non empty set
for f, g being FinSequence of D
for n being Nat holds
( not g is_substring_of f,n or len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )
proof end;

definition
let D be non empty set ;
let f, g be FinSequence of D;
let n be Nat;
pred g is_odd_substring_of f,n means :: GLIB_006:def 1
( len g > 0 implies ex i being odd Nat st
( n <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) );
pred g is_even_substring_of f,n means :: GLIB_006:def 2
( len g > 0 implies ex i being even Nat st
( n <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) );
end;

:: deftheorem defines is_odd_substring_of GLIB_006:def 1 :
for D being non empty set
for f, g being FinSequence of D
for n being Nat holds
( g is_odd_substring_of f,n iff ( len g > 0 implies ex i being odd Nat st
( n <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) ) );

:: deftheorem defines is_even_substring_of GLIB_006:def 2 :
for D being non empty set
for f, g being FinSequence of D
for n being Nat holds
( g is_even_substring_of f,n iff ( len g > 0 implies ex i being even Nat st
( n <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) ) );

theorem Th12: :: GLIB_006:8
for D being non empty set
for f, g being FinSequence of D
for n being Nat st g is_odd_substring_of f,n holds
g is_substring_of f,n by FINSEQ_8:def 7;

theorem :: GLIB_006:9
for D being non empty set
for f, g being FinSequence of D
for n being Nat st g is_even_substring_of f,n holds
g is_substring_of f,n by FINSEQ_8:def 7;

theorem :: GLIB_006:10
for D being non empty set
for f, g being FinSequence of D
for n, m being Nat st m >= n holds
( ( g is_odd_substring_of f,m implies g is_odd_substring_of f,n ) & ( g is_even_substring_of f,m implies g is_even_substring_of f,n ) )
proof end;

theorem Th15: :: GLIB_006:11
for D being non empty set
for f being FinSequence of D st 1 <= len f holds
f is_odd_substring_of f, 0
proof end;

theorem Th16: :: GLIB_006:12
for D being non empty set
for f, g being FinSequence of D
for n being even Element of NAT st g is_odd_substring_of f,n holds
g is_odd_substring_of f,n + 1 by Th1;

theorem :: GLIB_006:13
for D being non empty set
for f, g being FinSequence of D
for n being odd Element of NAT st g is_even_substring_of f,n holds
g is_even_substring_of f,n + 1 by Th2;

theorem Th18: :: GLIB_006:14
for D being non empty set
for f, g being FinSequence of D st g is_odd_substring_of f, 0 holds
g is_odd_substring_of f,1
proof end;

:: into GLIB_000 ?
registration
let G be non-Dmulti _Graph;
cluster -> non-Dmulti for Subgraph of G;
coherence
for b1 being Subgraph of G holds b1 is non-Dmulti
proof end;
end;

:: into GLIB_000 ?
theorem Th19: :: GLIB_006:15
for G being _Graph holds G is inducedSubgraph of G,(the_Vertices_of G)
proof end;

:: into GLIB_000 ?
theorem Th20: :: GLIB_006:16
for G1, G3 being _Graph
for V, E being set
for G2 being inducedSubgraph of G1,V,E st G2 == G3 holds
G3 is inducedSubgraph of G1,V,E
proof end;

:: into GLIB_000 ?
theorem Th21: :: GLIB_006:17
for G being _Graph
for X being set
for e, y being object st e SJoins X,{y},G holds
ex x being object st
( x in X & e Joins x,y,G )
proof end;

:: into GLIB_000 ?
theorem :: GLIB_006:18
for G being _Graph
for X being set st X /\ (the_Vertices_of G) = {} holds
( G .edgesInto X = {} & G .edgesOutOf X = {} & G .edgesInOut X = {} & G .edgesBetween X = {} )
proof end;

:: into GLIB_000 ?
theorem :: GLIB_006:19
for G being _Graph
for X1, X2 being set
for y being object st X1 misses X2 holds
G .edgesBetween (X1,{y}) misses G .edgesBetween (X2,{y})
proof end;

:: into GLIB_000 ?
theorem :: GLIB_006:20
for G being _Graph
for X1, X2 being set
for y being object holds G .edgesBetween ((X1 \/ X2),{y}) = (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y}))
proof end;

:: into GLIB_000 ?
:: generalization of GLIB_000:22, uses it for simplification of proof
theorem :: GLIB_006:21
for G being _trivial _Graph ex v being Vertex of G st
( the_Vertices_of G = {v} & the_Source_of G = (the_Edges_of G) --> v & the_Target_of G = (the_Edges_of G) --> v )
proof end;

:: definitely into GLIB_001
registration
let G be _Graph;
cluster V5() closed Trail-like -> Circuit-like for Walk of G;
coherence
for b1 being Walk of G st b1 is closed & b1 is Trail-like & b1 is V5() holds
b1 is Circuit-like
by GLIB_001:def 30;
cluster V5() closed Path-like -> Cycle-like for Walk of G;
coherence
for b1 being Walk of G st b1 is closed & b1 is Path-like & b1 is V5() holds
b1 is Cycle-like
by GLIB_001:def 31;
end;

:: generalizes part of GLIB_001:175 and GLIB_001:176
:: into GLIB_001 ?
theorem Th26: :: GLIB_006:22
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is Trail-like holds
W2 is Trail-like
proof end;

:: generalizes part of GLIB_001:175 and GLIB_001:176
:: into GLIB_001 ?
theorem Th27: :: GLIB_006:23
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is Path-like holds
W2 is Path-like
proof end;

:: generalizes part of GLIB_001:175 and GLIB_001:176
:: more general version of CHORD:24
:: into GLIB_001 ?
theorem :: GLIB_006:24
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is Cycle-like holds
W2 is Cycle-like
proof end;

:: generalizes part of GLIB_001:175 and GLIB_001:176
:: into GLIB_001 ?
theorem :: GLIB_006:25
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is vertex-distinct holds
W2 is vertex-distinct
proof end;

:: BEGIN into GLIB_001 ?
:: Four theorems have been left out, as they need more theorems
:: about is_substring_of (and the even/odd equivalents),
:: and that is not part of this article.
:: The theorems left out here are:
:: theorem for G being _Graph, W being Walk of G, m,n being odd Nat,
:: m2 being Element of NAT
:: st m <= n & n <= len W & m = m2 holds W.cut(m,n) is_odd_substring_of W,m2
:: theorem for G being _Graph, W being Walk of G, m,n being Nat holds
:: W.cut(m,n) is_odd_substring_of W,0
:: theorem for G being _Graph, W1, W2 being Walk of G st W1.last() = W2.first()
:: holds W2 is_odd_substring_of W1.append(W2),len W1
:: theorem for G being _Graph, W1, W2 being Walk of G
:: holds W1 is_odd_substring_of W1.append(W2),0
theorem :: GLIB_006:26
for G being _Graph
for W being Walk of G
for v being Vertex of G st v in W .vertices() holds
G .walkOf v is_substring_of W, 0
proof end;

theorem Th31: :: GLIB_006:27
for G being _Graph
for W being Walk of G
for n being odd Element of NAT st n + 2 <= len W holds
G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) is_odd_substring_of W, 0
proof end;

theorem :: GLIB_006:28
for G being _Graph
for W being Walk of G
for u, e, v being object st e Joins u,v,G & e in W .edges() & not G .walkOf (u,e,v) is_odd_substring_of W, 0 holds
G .walkOf (v,e,u) is_odd_substring_of W, 0
proof end;

theorem :: GLIB_006:29
for G being _Graph
for W being Walk of G
for u, e, v being object st e Joins u,v,G & G .walkOf (u,e,v) is_odd_substring_of W, 0 holds
( e in W .edges() & u in W .vertices() & v in W .vertices() )
proof end;

definition
let G be _Graph;
let W1, W2 be Walk of G;
func W1 .findFirstVertex W2 -> odd Element of NAT means :Def3: :: GLIB_006:def 3
( it <= len W1 & ex k being even Nat st
( it = k + 1 & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k <= l ) ) ) if W2 is_odd_substring_of W1, 0
otherwise it = len W1;
existence
( ( W2 is_odd_substring_of W1, 0 implies ex b1 being odd Element of NAT st
( b1 <= len W1 & ex k being even Nat st
( b1 = k + 1 & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k <= l ) ) ) ) & ( not W2 is_odd_substring_of W1, 0 implies ex b1 being odd Element of NAT st b1 = len W1 ) )
proof end;
uniqueness
for b1, b2 being odd Element of NAT holds
( ( W2 is_odd_substring_of W1, 0 & b1 <= len W1 & ex k being even Nat st
( b1 = k + 1 & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k <= l ) ) & b2 <= len W1 & ex k being even Nat st
( b2 = k + 1 & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k <= l ) ) implies b1 = b2 ) & ( not W2 is_odd_substring_of W1, 0 & b1 = len W1 & b2 = len W1 implies b1 = b2 ) )
proof end;
consistency
for b1 being odd Element of NAT holds verum
;
func W1 .findLastVertex W2 -> odd Element of NAT means :Def4: :: GLIB_006:def 4
( it <= len W1 & ex k being even Nat st
( it = k + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k <= l ) ) ) if W2 is_odd_substring_of W1, 0
otherwise it = len W1;
existence
( ( W2 is_odd_substring_of W1, 0 implies ex b1 being odd Element of NAT st
( b1 <= len W1 & ex k being even Nat st
( b1 = k + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k <= l ) ) ) ) & ( not W2 is_odd_substring_of W1, 0 implies ex b1 being odd Element of NAT st b1 = len W1 ) )
proof end;
uniqueness
for b1, b2 being odd Element of NAT holds
( ( W2 is_odd_substring_of W1, 0 & b1 <= len W1 & ex k being even Nat st
( b1 = k + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k <= l ) ) & b2 <= len W1 & ex k being even Nat st
( b2 = k + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k <= l ) ) implies b1 = b2 ) & ( not W2 is_odd_substring_of W1, 0 & b1 = len W1 & b2 = len W1 implies b1 = b2 ) )
proof end;
consistency
for b1 being odd Element of NAT holds verum
;
end;

:: deftheorem Def3 defines .findFirstVertex GLIB_006:def 3 :
for G being _Graph
for W1, W2 being Walk of G
for b4 being odd Element of NAT holds
( ( W2 is_odd_substring_of W1, 0 implies ( b4 = W1 .findFirstVertex W2 iff ( b4 <= len W1 & ex k being even Nat st
( b4 = k + 1 & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k <= l ) ) ) ) ) & ( not W2 is_odd_substring_of W1, 0 implies ( b4 = W1 .findFirstVertex W2 iff b4 = len W1 ) ) );

:: deftheorem Def4 defines .findLastVertex GLIB_006:def 4 :
for G being _Graph
for W1, W2 being Walk of G
for b4 being odd Element of NAT holds
( ( W2 is_odd_substring_of W1, 0 implies ( b4 = W1 .findLastVertex W2 iff ( b4 <= len W1 & ex k being even Nat st
( b4 = k + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k <= l ) ) ) ) ) & ( not W2 is_odd_substring_of W1, 0 implies ( b4 = W1 .findLastVertex W2 iff b4 = len W1 ) ) );

theorem Th34: :: GLIB_006:30
for G being _Graph
for W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0 holds
( W1 . (W1 .findFirstVertex W2) = W2 .first() & W1 . (W1 .findLastVertex W2) = W2 .last() )
proof end;

theorem Th35: :: GLIB_006:31
for G being _Graph
for W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0 holds
( 1 <= W1 .findFirstVertex W2 & W1 .findFirstVertex W2 <= len W1 & 1 <= W1 .findLastVertex W2 & W1 .findLastVertex W2 <= len W1 ) by Def3, Def4, ABIAN:12;

theorem Th36: :: GLIB_006:32
for G being _Graph
for W being Walk of G holds
( 1 = W .findFirstVertex W & W .findLastVertex W = len W )
proof end;

theorem :: GLIB_006:33
for G being _Graph
for W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0 holds
W1 .findFirstVertex W2 <= W1 .findLastVertex W2
proof end;

definition
let G be _Graph;
let W1, W2, W3 be Walk of G;
func W1 .replaceWith (W2,W3) -> Walk of G equals :Def5: :: GLIB_006:def 5
((W1 .cut (1,(W1 .findFirstVertex W2))) .append W3) .append (W1 .cut ((W1 .findLastVertex W2),(len W1))) if ( W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() )
otherwise W1;
correctness
coherence
( ( W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() implies ((W1 .cut (1,(W1 .findFirstVertex W2))) .append W3) .append (W1 .cut ((W1 .findLastVertex W2),(len W1))) is Walk of G ) & ( ( not W2 is_odd_substring_of W1, 0 or not W2 .first() = W3 .first() or not W2 .last() = W3 .last() ) implies W1 is Walk of G ) )
;
consistency
for b1 being Walk of G holds verum
;
;
end;

:: deftheorem Def5 defines .replaceWith GLIB_006:def 5 :
for G being _Graph
for W1, W2, W3 being Walk of G holds
( ( W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() implies W1 .replaceWith (W2,W3) = ((W1 .cut (1,(W1 .findFirstVertex W2))) .append W3) .append (W1 .cut ((W1 .findLastVertex W2),(len W1))) ) & ( ( not W2 is_odd_substring_of W1, 0 or not W2 .first() = W3 .first() or not W2 .last() = W3 .last() ) implies W1 .replaceWith (W2,W3) = W1 ) );

definition
let G be _Graph;
let W1, W3 be Walk of G;
let e be object ;
func W1 .replaceEdgeWith (e,W3) -> Walk of G equals :Def6: :: GLIB_006:def 6
W1 .replaceWith ((G .walkOf ((W3 .first()),e,(W3 .last()))),W3) if ( e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 )
otherwise W1;
correctness
coherence
( ( e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 implies W1 .replaceWith ((G .walkOf ((W3 .first()),e,(W3 .last()))),W3) is Walk of G ) & ( ( not e Joins W3 .first() ,W3 .last() ,G or not G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 ) implies W1 is Walk of G ) )
;
consistency
for b1 being Walk of G holds verum
;
;
end;

:: deftheorem Def6 defines .replaceEdgeWith GLIB_006:def 6 :
for G being _Graph
for W1, W3 being Walk of G
for e being object holds
( ( e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 implies W1 .replaceEdgeWith (e,W3) = W1 .replaceWith ((G .walkOf ((W3 .first()),e,(W3 .last()))),W3) ) & ( ( not e Joins W3 .first() ,W3 .last() ,G or not G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 ) implies W1 .replaceEdgeWith (e,W3) = W1 ) );

definition
let G be _Graph;
let W1, W2 be Walk of G;
let e be object ;
func W1 .replaceWithEdge (W2,e) -> Walk of G equals :Def7: :: GLIB_006:def 7
W1 .replaceWith (W2,(G .walkOf ((W2 .first()),e,(W2 .last())))) if ( W2 is_odd_substring_of W1, 0 & e Joins W2 .first() ,W2 .last() ,G )
otherwise W1;
correctness
coherence
( ( W2 is_odd_substring_of W1, 0 & e Joins W2 .first() ,W2 .last() ,G implies W1 .replaceWith (W2,(G .walkOf ((W2 .first()),e,(W2 .last())))) is Walk of G ) & ( ( not W2 is_odd_substring_of W1, 0 or not e Joins W2 .first() ,W2 .last() ,G ) implies W1 is Walk of G ) )
;
consistency
for b1 being Walk of G holds verum
;
;
end;

:: deftheorem Def7 defines .replaceWithEdge GLIB_006:def 7 :
for G being _Graph
for W1, W2 being Walk of G
for e being object holds
( ( W2 is_odd_substring_of W1, 0 & e Joins W2 .first() ,W2 .last() ,G implies W1 .replaceWithEdge (W2,e) = W1 .replaceWith (W2,(G .walkOf ((W2 .first()),e,(W2 .last())))) ) & ( ( not W2 is_odd_substring_of W1, 0 or not e Joins W2 .first() ,W2 .last() ,G ) implies W1 .replaceWithEdge (W2,e) = W1 ) );

theorem Th38: :: GLIB_006:34
for G being _Graph
for W1, W2, W3 being Walk of G st W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() holds
( (W1 .cut (1,(W1 .findFirstVertex W2))) .first() = W1 .first() & (W1 .cut (1,(W1 .findFirstVertex W2))) .last() = W3 .first() & ((W1 .cut (1,(W1 .findFirstVertex W2))) .append W3) .first() = W1 .first() & ((W1 .cut (1,(W1 .findFirstVertex W2))) .append W3) .last() = W3 .last() & (W1 .cut ((W1 .findLastVertex W2),(len W1))) .first() = W3 .last() & (W1 .cut ((W1 .findLastVertex W2),(len W1))) .last() = W1 .last() )
proof end;

theorem Th39: :: GLIB_006:35
for G being _Graph
for W1, W2, W3 being Walk of G holds
( W1 .first() = (W1 .replaceWith (W2,W3)) .first() & W1 .last() = (W1 .replaceWith (W2,W3)) .last() )
proof end;

theorem :: GLIB_006:36
for G being _Graph
for W1, W2, W3 being Walk of G st W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() holds
(W1 .replaceWith (W2,W3)) .vertices() = (((W1 .cut (1,(W1 .findFirstVertex W2))) .vertices()) \/ (W3 .vertices())) \/ ((W1 .cut ((W1 .findLastVertex W2),(len W1))) .vertices())
proof end;

theorem Th41: :: GLIB_006:37
for G being _Graph
for W1, W2, W3 being Walk of G st W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() holds
(W1 .replaceWith (W2,W3)) .edges() = (((W1 .cut (1,(W1 .findFirstVertex W2))) .edges()) \/ (W3 .edges())) \/ ((W1 .cut ((W1 .findLastVertex W2),(len W1))) .edges())
proof end;

theorem Th42: :: GLIB_006:38
for G being _Graph
for W1, W3 being Walk of G
for e being object st e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 holds
( e in (W1 .replaceEdgeWith (e,W3)) .edges() iff ( e in (W1 .cut (1,(W1 .findFirstVertex (G .walkOf ((W3 .first()),e,(W3 .last())))))) .edges() or e in W3 .edges() or e in (W1 .cut ((W1 .findLastVertex (G .walkOf ((W3 .first()),e,(W3 .last())))),(len W1))) .edges() ) )
proof end;

:: The Proof got surprisingly long. Maybe there's a shorter way?
theorem Th43: :: GLIB_006:39
for G being _Graph
for W1, W3 being Walk of G
for e being object st e Joins W3 .first() ,W3 .last() ,G & not e in W3 .edges() & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 & ( for n, m being even Nat st n in dom W1 & m in dom W1 & W1 . n = e & W1 . m = e holds
n = m ) holds
not e in (W1 .replaceEdgeWith (e,W3)) .edges()
proof end;

:: this is the important theorem from this whole preliminary theory
:: on replacement of parts of walks that will be used in the main part
theorem Th44: :: GLIB_006:40
for G being _Graph
for T1 being Trail of G
for W3 being Walk of G
for e being object st e Joins W3 .first() ,W3 .last() ,G & not e in W3 .edges() & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of T1, 0 holds
not e in (T1 .replaceEdgeWith (e,W3)) .edges()
proof end;

theorem :: GLIB_006:41
for G being _Graph
for W1, W2 being Walk of G st W1 .first() = W2 .first() & W1 .last() = W2 .last() holds
W1 .replaceWith (W1,W2) = W2
proof end;

:: The following theorem has been left out
:: theorem ThExtra: for G being _Graph, W1, W2 being Walk of G
:: holds W1.replaceWith(W2,W2) = W1
:: as it needs
:: theorem for G being _Graph, W1, W2 being Walk of G
:: st W2 is_odd_substring_of W1,0 holds ex m,n being Element of NAT
:: st 1 <= m & m <= n & n <= len W2 & W1.cut(m,n) = W2
:: which in turn relies on unproven theorems about is_odd_substring_of
:: and -cut/smid.
:: the assumption in the following theorem could be dropped
:: if the theorems above would be available
theorem Th46: :: GLIB_006:42
for G being _Graph
for W1, W3 being Walk of G
for e being object st e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 holds
ex W2 being Walk of G st W1 .replaceEdgeWith (e,W3) = W1 .replaceWith (W2,W3)
proof end;

:: same as theorem above
theorem Th47: :: GLIB_006:43
for G being _Graph
for W1, W2 being Walk of G
for e being object st W2 is_odd_substring_of W1, 0 & e Joins W2 .first() ,W2 .last() ,G holds
ex W3 being Walk of G st W1 .replaceWithEdge (W2,e) = W1 .replaceWith (W2,W3)
proof end;

theorem :: GLIB_006:44
for G being _Graph
for W1, W3 being Walk of G
for e being object holds
( W1 .first() = (W1 .replaceEdgeWith (e,W3)) .first() & W1 .last() = (W1 .replaceEdgeWith (e,W3)) .last() )
proof end;

theorem :: GLIB_006:45
for G being _Graph
for W1, W2 being Walk of G
for e being object holds
( W1 .first() = (W1 .replaceWithEdge (W2,e)) .first() & W1 .last() = (W1 .replaceWithEdge (W2,e)) .last() )
proof end;

theorem Th50: :: GLIB_006:46
for G being _Graph
for W1, W2, W3 being Walk of G
for u, v being object holds
( W1 is_Walk_from u,v iff W1 .replaceWith (W2,W3) is_Walk_from u,v )
proof end;

theorem Th51: :: GLIB_006:47
for G being _Graph
for W1, W3 being Walk of G
for e, u, v being object holds
( W1 is_Walk_from u,v iff W1 .replaceEdgeWith (e,W3) is_Walk_from u,v )
proof end;

theorem :: GLIB_006:48
for G being _Graph
for W1, W2 being Walk of G
for e, u, v being object holds
( W1 is_Walk_from u,v iff W1 .replaceWithEdge (W2,e) is_Walk_from u,v )
proof end;

:: END into GLIB_001 ?
:: into GLIB_002 ?
theorem Th53: :: GLIB_006:49
for G being _Graph
for v1, v2 being Vertex of G st v1 is isolated & v1 <> v2 holds
not v2 in G .reachableFrom v1
proof end;

:: into GLIB_002 ?
theorem Th54: :: GLIB_006:50
for G being _Graph
for v1, v2 being Vertex of G st v1 in G .reachableFrom v2 holds
v2 in G .reachableFrom v1
proof end;

:: into GLIB_002 ?
theorem Th55: :: GLIB_006:51
for G being _Graph
for v being Vertex of G st v is isolated holds
{v} = G .reachableFrom v
proof end;

:: into GLIB_002 ?
theorem :: GLIB_006:52
for G being _Graph
for v being Vertex of G
for C being inducedSubgraph of G,{v} st v is isolated holds
C is Component of G
proof end;

:: into GLIB_002 ?
theorem Th57: :: GLIB_006:53
for G1 being non _trivial _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v st v is isolated holds
( G1 .componentSet() = (G2 .componentSet()) \/ {{v}} & G1 .numComponents() = (G2 .numComponents()) +` 1 )
proof end;

:: into GLIB_002 ?
registration
let G be _Graph;
cluster isolated -> non cut-vertex for Element of the_Vertices_of G;
coherence
for b1 being Vertex of G st b1 is isolated holds
not b1 is cut-vertex
proof end;
end;

:: into GLIB_002 ?
theorem Th58: :: GLIB_006:54
for G1 being _Graph
for G2 being Subgraph of G1
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( W1 is Cycle-like iff W2 is Cycle-like )
proof end;

:: into GLIB_002 ?
theorem :: GLIB_006:55
for G1 being connected _Graph
for G2 being Component of G1 holds G1 == G2
proof end;

:: into CHORD ?
registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] complete -> connected for set ;
coherence
for b1 being _Graph st b1 is complete holds
b1 is connected
proof end;
end;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] non _finite non loopless non non-multi non non-Dmulti non simple non Dsimple non acyclic for set ;
existence
ex b1 being _Graph st
( not b1 is non-Dmulti & not b1 is non-multi & not b1 is loopless & not b1 is Dsimple & not b1 is simple & not b1 is acyclic & not b1 is _finite )
proof end;
end;

definition
let G be _Graph;
func Endvertices G -> Subset of (the_Vertices_of G) means :Def8: :: GLIB_006:def 8
for v being object holds
( v in it iff ex w being Vertex of G st
( v = w & w is endvertex ) );
existence
ex b1 being Subset of (the_Vertices_of G) st
for v being object holds
( v in b1 iff ex w being Vertex of G st
( v = w & w is endvertex ) )
proof end;
uniqueness
for b1, b2 being Subset of (the_Vertices_of G) st ( for v being object holds
( v in b1 iff ex w being Vertex of G st
( v = w & w is endvertex ) ) ) & ( for v being object holds
( v in b2 iff ex w being Vertex of G st
( v = w & w is endvertex ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Endvertices GLIB_006:def 8 :
for G being _Graph
for b2 being Subset of (the_Vertices_of G) holds
( b2 = Endvertices G iff for v being object holds
( v in b2 iff ex w being Vertex of G st
( v = w & w is endvertex ) ) );

theorem :: GLIB_006:56
for G being _Graph
for v being Vertex of G holds
( v in Endvertices G iff v is endvertex )
proof end;

:: analogue to GLIB_000:def 32
definition
let G be _Graph;
mode Supergraph of G -> _Graph means :Def9: :: GLIB_006:def 9
( the_Vertices_of G c= the_Vertices_of it & the_Edges_of G c= the_Edges_of it & ( for e being set st e in the_Edges_of G holds
( (the_Source_of G) . e = (the_Source_of it) . e & (the_Target_of G) . e = (the_Target_of it) . e ) ) );
existence
ex b1 being _Graph st
( the_Vertices_of G c= the_Vertices_of b1 & the_Edges_of G c= the_Edges_of b1 & ( for e being set st e in the_Edges_of G holds
( (the_Source_of G) . e = (the_Source_of b1) . e & (the_Target_of G) . e = (the_Target_of b1) . e ) ) )
proof end;
end;

:: deftheorem Def9 defines Supergraph GLIB_006:def 9 :
for G, b2 being _Graph holds
( b2 is Supergraph of G iff ( the_Vertices_of G c= the_Vertices_of b2 & the_Edges_of G c= the_Edges_of b2 & ( for e being set st e in the_Edges_of G holds
( (the_Source_of G) . e = (the_Source_of b2) . e & (the_Target_of G) . e = (the_Target_of b2) . e ) ) ) );

:: Now we show some handy trivialities. Most of them have a
:: Subgraph equivalent in e.g. GLIB_000 and are shown through it and
:: the following theorem
:: Hence not all Subgraph theorems are reproduced here as they can be easily
:: shown.
theorem Th61: :: GLIB_006:57
for G1, G2 being _Graph holds
( G2 is Subgraph of G1 iff G1 is Supergraph of G2 )
proof end;

theorem Th62: :: GLIB_006:58
for G1, G2 being _Graph holds
( ( G2 is Subgraph of G1 & G2 is Supergraph of G1 ) iff G1 == G2 )
proof end;

theorem Th63: :: GLIB_006:59
for G1, G2 being _Graph holds
( ( G1 is Supergraph of G2 & G2 is Supergraph of G1 ) iff G1 == G2 )
proof end;

theorem Th64: :: GLIB_006:60
for G1, G2 being _Graph holds
( G1 is Supergraph of G2 iff G2 c= G1 )
proof end;

theorem Th65: :: GLIB_006:61
for G being _Graph holds G is Supergraph of G by Th64;

theorem Th66: :: GLIB_006:62
for G3 being _Graph
for G2 being Supergraph of G3
for G1 being Supergraph of G2 holds G1 is Supergraph of G3
proof end;

:: the following 4 Supergraph theorems have no Subgraph analogon in the MML yet
theorem Th67: :: GLIB_006:63
for G1, G2 being _Graph st the_Vertices_of G2 c= the_Vertices_of G1 & the_Source_of G2 c= the_Source_of G1 & the_Target_of G2 c= the_Target_of G1 holds
G1 is Supergraph of G2
proof end;

theorem Th68: :: GLIB_006:64
for G2 being _Graph
for G1 being Supergraph of G2 holds
( the_Source_of G2 c= the_Source_of G1 & the_Target_of G2 c= the_Target_of G1 )
proof end;

theorem Th69: :: GLIB_006:65
for G2 being _Graph
for G1 being Supergraph of G2 st the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of G1 holds
G1 == G2
proof end;

theorem :: GLIB_006:66
for G1, G2 being _Graph st the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of G1 & the_Source_of G2 c= the_Source_of G1 & the_Target_of G2 c= the_Target_of G1 holds
G1 == G2
proof end;

theorem Th71: :: GLIB_006:67
for G2 being _Graph
for G1 being Supergraph of G2
for x being set holds
( ( x in the_Vertices_of G2 implies x in the_Vertices_of G1 ) & ( x in the_Edges_of G2 implies x in the_Edges_of G1 ) )
proof end;

theorem Th72: :: GLIB_006:68
for G2 being _Graph
for G1 being Supergraph of G2
for v being Vertex of G2 holds v is Vertex of G1 by Th71;

theorem :: GLIB_006:69
for G2 being _Graph
for G1 being Supergraph of G2 holds
( the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G2) & the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G2) )
proof end;

theorem Th74: :: GLIB_006:70
for G2 being _Graph
for G1 being Supergraph of G2
for x, y being set
for e being object holds
( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
proof end;

theorem Th75: :: GLIB_006:71
for G2 being _Graph
for G1 being Supergraph of G2
for e, v1, v2 being object holds
( not e DJoins v1,v2,G1 or e DJoins v1,v2,G2 or not e in the_Edges_of G2 )
proof end;

theorem Th76: :: GLIB_006:72
for G2 being _Graph
for G1 being Supergraph of G2
for e, v1, v2 being object holds
( not e Joins v1,v2,G1 or e Joins v1,v2,G2 or not e in the_Edges_of G2 )
proof end;

registration
let G be _finite _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] _finite for Supergraph of G;
existence
ex b1 being Supergraph of G st b1 is _finite
proof end;
end;

:: no equivalent in GLIB_000
theorem :: GLIB_006:73
for G2 being _Graph
for G1 being Supergraph of G2 holds
( G2 .order() c= G1 .order() & G2 .size() c= G1 .size() )
proof end;

theorem :: GLIB_006:74
for G2 being _finite _Graph
for G1 being _finite Supergraph of G2 holds
( G2 .order() <= G1 .order() & G2 .size() <= G1 .size() )
proof end;

theorem Th79: :: GLIB_006:75
for G2 being _Graph
for G1 being Supergraph of G2
for W being Walk of G2 holds W is Walk of G1
proof end;

theorem Th80: :: GLIB_006:76
for G2 being _Graph
for G1 being Supergraph of G2
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 holds
( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is V5() implies W2 is V5() ) & ( W2 is V5() implies W1 is V5() ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) & ( W1 is Cycle-like implies W2 is Cycle-like ) & ( W2 is Cycle-like implies W1 is Cycle-like ) )
proof end;

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

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

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

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

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

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

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

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

definition
let G be _Graph;
let V be set ;
mode addVertices of G,V -> Supergraph of G means :Def10: :: GLIB_006:def 10
( the_Vertices_of it = (the_Vertices_of G) \/ V & the_Edges_of it = the_Edges_of G & the_Source_of it = the_Source_of G & the_Target_of it = the_Target_of G );
existence
ex b1 being Supergraph of G st
( the_Vertices_of b1 = (the_Vertices_of G) \/ V & the_Edges_of b1 = the_Edges_of G & the_Source_of b1 = the_Source_of G & the_Target_of b1 = the_Target_of G )
proof end;
end;

:: deftheorem Def10 defines addVertices GLIB_006:def 10 :
for G being _Graph
for V being set
for b3 being Supergraph of G holds
( b3 is addVertices of G,V iff ( the_Vertices_of b3 = (the_Vertices_of G) \/ V & the_Edges_of b3 = the_Edges_of G & the_Source_of b3 = the_Source_of G & the_Target_of b3 = the_Target_of G ) );

theorem :: GLIB_006:77
for G being _Graph
for V being set
for G1, G2 being addVertices of G,V holds G1 == G2
proof end;

theorem Th82: :: GLIB_006:78
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds
( G1 == G2 iff V c= the_Vertices_of G2 )
proof end;

theorem :: GLIB_006:79
for G1, G2 being _Graph
for V being set st G1 == G2 & V c= the_Vertices_of G2 holds
G1 is addVertices of G2,V
proof end;

theorem :: GLIB_006:80
for G, G2 being _Graph
for V being set
for G1 being addVertices of G,V st G1 == G2 holds
G2 is addVertices of G,V
proof end;

theorem Th85: :: GLIB_006:81
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G1
proof end;

theorem :: GLIB_006:82
for G3 being _Graph
for V1, V2 being set
for G2 being addVertices of G3,V2
for G1 being addVertices of G2,V1 holds G1 is addVertices of G3,V1 \/ V2
proof end;

theorem :: GLIB_006:83
for G3 being _Graph
for V1, V2 being set
for G1 being addVertices of G3,V1 \/ V2 ex G2 being addVertices of G3,V2 st G1 is addVertices of G2,V1
proof end;

theorem Th88: :: GLIB_006:84
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds G2 is inducedSubgraph of G1,(the_Vertices_of G2)
proof end;

theorem Th89: :: GLIB_006:85
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for x, y, e being object holds
( e DJoins x,y,G1 iff e DJoins x,y,G2 )
proof end;

theorem Th90: :: GLIB_006:86
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for v being object st v in V holds
v is Vertex of G1
proof end;

theorem Th91: :: GLIB_006:87
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for x, y, e being object holds
( e Joins x,y,G1 iff e Joins x,y,G2 )
proof end;

theorem Th92: :: GLIB_006:88
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for v being Vertex of G1 st v in V \ (the_Vertices_of G2) holds
( v is isolated & not v is cut-vertex )
proof end;

theorem Th93: :: GLIB_006:89
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V st V \ (the_Vertices_of G2) <> {} holds
( not G1 is _trivial & not G1 is connected & not G1 is Tree-like & not G1 is complete )
proof end;

registration
let G be non-Dmulti _Graph;
let V be set ;
cluster -> non-Dmulti for addVertices of G,V;
coherence
for b1 being addVertices of G,V holds b1 is non-Dmulti
proof end;
end;

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

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

registration
let G be Dsimple _Graph;
let V be set ;
cluster -> Dsimple for addVertices of G,V;
coherence
for b1 being addVertices of G,V holds b1 is Dsimple
;
end;

registration
let G be Dsimple _Graph;
let V be set ;
cluster -> Dsimple for addVertices of G,V;
coherence
for b1 being addVertices of G,V holds b1 is Dsimple
;
end;

theorem Th94: :: GLIB_006:90
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for W being Walk of G1 holds
( W .vertices() misses V \ (the_Vertices_of G2) or not W is V5() )
proof end;

theorem Th95: :: GLIB_006:91
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for W being Walk of G1 st W .vertices() misses V \ (the_Vertices_of G2) holds
W is Walk of G2
proof end;

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

theorem Th96: :: GLIB_006:92
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds
( G2 is chordal iff G1 is chordal )
proof end;

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

definition
let G be _Graph;
let v be object ;
mode addVertex of G,v is addVertices of G,{v};
end;

theorem :: GLIB_006:93
for G2 being _Graph
for v being object
for G1 being addVertex of G2,v holds
( G1 == G2 iff v in the_Vertices_of G2 ) by Th82, ZFMISC_1:31;

theorem Th98: :: GLIB_006:94
for G2 being _Graph
for v being object
for G1 being addVertex of G2,v holds v is Vertex of G1
proof end;

Lm1: for X being set holds {X} \ X <> {}
proof end;

registration
let G be _Graph;
cluster -> non _trivial non connected non complete for addVertices of G,{(the_Vertices_of G)};
coherence
for b1 being addVertex of G,(the_Vertices_of G) holds
( not b1 is _trivial & not b1 is connected & not b1 is complete )
proof end;
end;

:: the prime example of how to use the new modes to show existences
:: of certain graphs
registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] non _trivial non connected non complete for set ;
existence
ex b1 being _Graph st
( not b1 is _trivial & not b1 is connected & not b1 is complete )
proof end;
end;

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

:: In general, non finite versions of cardinalities are missing in the
:: graph construction modes of GLIB_000 (e.g. removeVertex) and should
:: be added.
theorem Th99: :: GLIB_006:95
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds
( G1 .size() = G2 .size() & G1 .order() = (G2 .order()) +` (card (V \ (the_Vertices_of G2))) )
proof end;

theorem Th100: :: GLIB_006:96
for G2 being _finite _Graph
for V being finite set
for G1 being addVertices of G2,V holds G1 .order() = (G2 .order()) + (card (V \ (the_Vertices_of G2)))
proof end;

theorem :: GLIB_006:97
for G2 being _Graph
for v being object
for G1 being addVertex of G2,v st not v in the_Vertices_of G2 holds
G1 .order() = (G2 .order()) +` 1
proof end;

theorem :: GLIB_006:98
for G2 being _finite _Graph
for v being object
for G1 being addVertex of G2,v st not v in the_Vertices_of G2 holds
G1 .order() = (G2 .order()) + 1
proof end;

registration
let G be _finite _Graph;
let V be finite set ;
cluster -> _finite for addVertices of G,V;
coherence
for b1 being addVertices of G,V holds b1 is _finite
proof end;
end;

registration
let G be _finite _Graph;
let v be object ;
cluster -> _finite for addVertices of G,{v};
coherence
for b1 being addVertex of G,v holds b1 is _finite
;
end;

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

:: we explicitly add an edge only if it is not used already
:: to ensure getting a Supergraph
definition
let G be _Graph;
let v1, e, v2 be object ;
mode addEdge of G,v1,e,v2 -> Supergraph of G means :Def11: :: GLIB_006:def 11
( the_Vertices_of it = the_Vertices_of G & the_Edges_of it = (the_Edges_of G) \/ {e} & the_Source_of it = (the_Source_of G) +* (e .--> v1) & the_Target_of it = (the_Target_of G) +* (e .--> v2) ) if ( v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G )
otherwise it == G;
existence
( ( v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ex b1 being Supergraph of G st
( the_Vertices_of b1 = the_Vertices_of G & the_Edges_of b1 = (the_Edges_of G) \/ {e} & the_Source_of b1 = (the_Source_of G) +* (e .--> v1) & the_Target_of b1 = (the_Target_of G) +* (e .--> v2) ) ) & ( ( not v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) implies ex b1 being Supergraph of G st b1 == G ) )
proof end;
consistency
for b1 being Supergraph of G holds verum
;
end;

:: deftheorem Def11 defines addEdge GLIB_006:def 11 :
for G being _Graph
for v1, e, v2 being object
for b5 being Supergraph of G holds
( ( v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b5 is addEdge of G,v1,e,v2 iff ( the_Vertices_of b5 = the_Vertices_of G & the_Edges_of b5 = (the_Edges_of G) \/ {e} & the_Source_of b5 = (the_Source_of G) +* (e .--> v1) & the_Target_of b5 = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( not v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) implies ( b5 is addEdge of G,v1,e,v2 iff b5 == G ) ) );

theorem :: GLIB_006:99
for G being _Graph
for v1, e, v2 being object
for G1, G2 being addEdge of G,v1,e,v2 holds G1 == G2
proof end;

theorem :: GLIB_006:100
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 holds
( G1 == G2 iff e in the_Edges_of G2 )
proof end;

theorem :: GLIB_006:101
for G, G2 being _Graph
for v1, e, v2 being object
for G1 being addEdge of G,v1,e,v2 st G1 == G2 holds
G2 is addEdge of G,v1,e,v2
proof end;

theorem Th106: :: GLIB_006:102
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 holds the_Vertices_of G1 = the_Vertices_of G2
proof end;

theorem :: GLIB_006:103
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 holds G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G1
proof end;

theorem Th108: :: GLIB_006:104
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2
for v being Vertex of G1 holds v is Vertex of G2
proof end;

theorem Th109: :: GLIB_006:105
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
e DJoins v1,v2,G1
proof end;

theorem Th110: :: GLIB_006:106
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 holds
e1 = e
proof end;

theorem :: GLIB_006:107
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 & not ( w1 = v1 & w2 = v2 ) holds
( w1 = v2 & w2 = v1 )
proof end;

theorem Th112: :: GLIB_006:108
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being set
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
G2 is removeEdge of G1,e
proof end;

theorem Th113: :: GLIB_006:109
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2
for W being Walk of G1 st ( e in W .edges() implies e in the_Edges_of G2 ) holds
W is Walk of G2
proof end;

registration
let G be _trivial _Graph;
let v1, e, v2 be object ;
cluster -> _trivial for addEdge of G,v1,e,v2;
coherence
for b1 being addEdge of G,v1,e,v2 holds b1 is _trivial
proof end;
end;

registration
let G be connected _Graph;
let v1, e, v2 be object ;
cluster -> connected for addEdge of G,v1,e,v2;
coherence
for b1 being addEdge of G,v1,e,v2 holds b1 is connected
proof end;
end;

registration
let G be complete _Graph;
let v1, e, v2 be object ;
cluster -> complete for addEdge of G,v1,e,v2;
coherence
for b1 being addEdge of G,v1,e,v2 holds b1 is complete
proof end;
end;

theorem :: GLIB_006:110
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
( G1 .order() = G2 .order() & G1 .size() = (G2 .size()) +` 1 )
proof end;

theorem :: GLIB_006:111
for G2 being _finite _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
G1 .size() = (G2 .size()) + 1
proof end;

registration
let G be _finite _Graph;
let v1, e, v2 be object ;
cluster -> _finite for addEdge of G,v1,e,v2;
coherence
for b1 being addEdge of G,v1,e,v2 holds b1 is _finite
proof end;
end;

theorem Th116: :: GLIB_006:112
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st G2 is loopless & v1 <> v2 holds
G1 is loopless
proof end;

theorem Th117: :: GLIB_006:113
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 G2 is loopless or not e in the_Edges_of G2 ) holds
not G1 is loopless
proof end;

registration
let G be _Graph;
let v be Vertex of G;
cluster -> non loopless for addEdge of G,v, the_Edges_of G,v;
coherence
for b1 being addEdge of G,v, the_Edges_of G,v holds not b1 is loopless
proof end;
end;

theorem Th118: :: GLIB_006:114
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st G2 is non-Dmulti & ( for e3 being object holds not e3 DJoins v1,v2,G2 ) holds
G1 is non-Dmulti
proof end;

theorem :: GLIB_006:115
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & ex e2 being object st e2 DJoins v1,v2,G2 holds
not G1 is non-Dmulti
proof end;

theorem Th120: :: GLIB_006:116
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st G2 is non-multi & not v1,v2 are_adjacent holds
G1 is non-multi
proof end;

theorem :: GLIB_006:117
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & v1,v2 are_adjacent holds
not G1 is non-multi
proof end;

theorem Th122: :: GLIB_006:118
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st G2 is acyclic & not v2 in G2 .reachableFrom v1 holds
G1 is acyclic
proof end;

theorem :: GLIB_006:119
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & v2 in G2 .reachableFrom v1 holds
not G1 is acyclic
proof end;

:: this is the theorem that spawned most of the preliminaries,
:: although it carries a seemingly obvious meaning.
:: it basically states that adding an edge within a component of a graph
:: doesn't connect it to other components
theorem :: GLIB_006:120
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not G2 is connected & v2 in G2 .reachableFrom v1 holds
not G1 is connected
proof end;

:: this theorem means there is at most one edge missing to completion
theorem :: GLIB_006:121
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & ( for v3, v4 being Vertex of G2 holds
( v3,v4 are_adjacent or v3 = v4 or ( v1 = v3 & v2 = v4 ) or ( v1 = v4 & v2 = v3 ) ) ) holds
G1 is complete
proof end;

theorem :: GLIB_006:122
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not G2 is complete & v1,v2 are_adjacent holds
not G1 is complete
proof end;

definition
let G be _Graph;
let v1, e, v2 be object ;
mode addAdjVertex of G,v1,e,v2 -> Supergraph of G means :Def12: :: GLIB_006:def 12
( the_Vertices_of it = (the_Vertices_of G) \/ {v2} & the_Edges_of it = (the_Edges_of G) \/ {e} & the_Source_of it = (the_Source_of G) +* (e .--> v1) & the_Target_of it = (the_Target_of G) +* (e .--> v2) ) if ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G )
( the_Vertices_of it = (the_Vertices_of G) \/ {v1} & the_Edges_of it = (the_Edges_of G) \/ {e} & the_Source_of it = (the_Source_of G) +* (e .--> v1) & the_Target_of it = (the_Target_of G) +* (e .--> v2) ) if ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G )
otherwise it == G;
existence
( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G implies ex b1 being Supergraph of G st
( the_Vertices_of b1 = (the_Vertices_of G) \/ {v2} & the_Edges_of b1 = (the_Edges_of G) \/ {e} & the_Source_of b1 = (the_Source_of G) +* (e .--> v1) & the_Target_of b1 = (the_Target_of G) +* (e .--> v2) ) ) & ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ex b1 being Supergraph of G st
( the_Vertices_of b1 = (the_Vertices_of G) \/ {v1} & the_Edges_of b1 = (the_Edges_of G) \/ {e} & the_Source_of b1 = (the_Source_of G) +* (e .--> v1) & the_Target_of b1 = (the_Target_of G) +* (e .--> v2) ) ) & ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) implies ex b1 being Supergraph of G st b1 == G ) )
proof end;
consistency
for b1 being Supergraph of G st v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G & not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G holds
( the_Vertices_of b1 = (the_Vertices_of G) \/ {v2} & the_Edges_of b1 = (the_Edges_of G) \/ {e} & the_Source_of b1 = (the_Source_of G) +* (e .--> v1) & the_Target_of b1 = (the_Target_of G) +* (e .--> v2) iff ( the_Vertices_of b1 = (the_Vertices_of G) \/ {v1} & the_Edges_of b1 = (the_Edges_of G) \/ {e} & the_Source_of b1 = (the_Source_of G) +* (e .--> v1) & the_Target_of b1 = (the_Target_of G) +* (e .--> v2) ) )
;
end;

:: deftheorem Def12 defines addAdjVertex GLIB_006:def 12 :
for G being _Graph
for v1, e, v2 being object
for b5 being Supergraph of G holds
( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b5 is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b5 = (the_Vertices_of G) \/ {v2} & the_Edges_of b5 = (the_Edges_of G) \/ {e} & the_Source_of b5 = (the_Source_of G) +* (e .--> v1) & the_Target_of b5 = (the_Target_of G) +* (e .--> v2) ) ) ) & ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b5 is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b5 = (the_Vertices_of G) \/ {v1} & the_Edges_of b5 = (the_Edges_of G) \/ {e} & the_Source_of b5 = (the_Source_of G) +* (e .--> v1) & the_Target_of b5 = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) implies ( b5 is addAdjVertex of G,v1,e,v2 iff b5 == G ) ) );

definition
let G be _Graph;
let v1 be Vertex of G;
let e, v2 be object ;
redefine mode addAdjVertex of G,v1,e,v2 means :Def13: :: GLIB_006:def 13
( the_Vertices_of it = (the_Vertices_of G) \/ {v2} & the_Edges_of it = (the_Edges_of G) \/ {e} & the_Source_of it = (the_Source_of G) +* (e .--> v1) & the_Target_of it = (the_Target_of G) +* (e .--> v2) ) if ( not v2 in the_Vertices_of G & not e in the_Edges_of G )
otherwise it == G;
compatibility
for b1 being Supergraph of G holds
( ( not v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b1 is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b1 = (the_Vertices_of G) \/ {v2} & the_Edges_of b1 = (the_Edges_of G) \/ {e} & the_Source_of b1 = (the_Source_of G) +* (e .--> v1) & the_Target_of b1 = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( v2 in the_Vertices_of G or e in the_Edges_of G ) implies ( b1 is addAdjVertex of G,v1,e,v2 iff b1 == G ) ) )
by Def12;
consistency
for b1 being Supergraph of G holds verum
;
end;

:: deftheorem Def13 defines addAdjVertex GLIB_006:def 13 :
for G being _Graph
for v1 being Vertex of G
for e, v2 being object
for b5 being Supergraph of G holds
( ( not v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b5 is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b5 = (the_Vertices_of G) \/ {v2} & the_Edges_of b5 = (the_Edges_of G) \/ {e} & the_Source_of b5 = (the_Source_of G) +* (e .--> v1) & the_Target_of b5 = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( v2 in the_Vertices_of G or e in the_Edges_of G ) implies ( b5 is addAdjVertex of G,v1,e,v2 iff b5 == G ) ) );

definition
let G be _Graph;
let v1, e be object ;
let v2 be Vertex of G;
redefine mode addAdjVertex of G,v1,e,v2 means :Def14: :: GLIB_006:def 14
( the_Vertices_of it = (the_Vertices_of G) \/ {v1} & the_Edges_of it = (the_Edges_of G) \/ {e} & the_Source_of it = (the_Source_of G) +* (e .--> v1) & the_Target_of it = (the_Target_of G) +* (e .--> v2) ) if ( not v1 in the_Vertices_of G & not e in the_Edges_of G )
otherwise it == G;
compatibility
for b1 being Supergraph of G holds
( ( not v1 in the_Vertices_of G & not e in the_Edges_of G implies ( b1 is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b1 = (the_Vertices_of G) \/ {v1} & the_Edges_of b1 = (the_Edges_of G) \/ {e} & the_Source_of b1 = (the_Source_of G) +* (e .--> v1) & the_Target_of b1 = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( v1 in the_Vertices_of G or e in the_Edges_of G ) implies ( b1 is addAdjVertex of G,v1,e,v2 iff b1 == G ) ) )
by Def12;
consistency
for b1 being Supergraph of G holds verum
;
end;

:: deftheorem Def14 defines addAdjVertex GLIB_006:def 14 :
for G being _Graph
for v1, e being object
for v2 being Vertex of G
for b5 being Supergraph of G holds
( ( not v1 in the_Vertices_of G & not e in the_Edges_of G implies ( b5 is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b5 = (the_Vertices_of G) \/ {v1} & the_Edges_of b5 = (the_Edges_of G) \/ {e} & the_Source_of b5 = (the_Source_of G) +* (e .--> v1) & the_Target_of b5 = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( v1 in the_Vertices_of G or e in the_Edges_of G ) implies ( b5 is addAdjVertex of G,v1,e,v2 iff b5 == G ) ) );

theorem :: GLIB_006:123
for G being _Graph
for v1, e, v2 being object
for G1, G2 being addAdjVertex of G,v1,e,v2 holds G1 == G2
proof end;

theorem :: GLIB_006:124
for G, G2 being _Graph
for v1, e, v2 being object
for G1 being addAdjVertex of G,v1,e,v2 st G1 == G2 holds
G2 is addAdjVertex of G,v1,e,v2
proof end;

theorem Th129: :: GLIB_006:125
for G2 being _Graph
for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 holds
ex G3 being addVertex of G2,v2 st G1 is addEdge of G3,v1,e,v2
proof end;

theorem Th130: :: GLIB_006:126
for G2 being _Graph
for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds
ex G3 being addVertex of G2,v1 st G1 is addEdge of G3,v1,e,v2
proof end;

theorem :: GLIB_006:127
for G3 being _Graph
for v1 being Vertex of G3
for e, v2 being object
for G2 being addVertex of G3,v2
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G3 & not v2 in the_Vertices_of G3 holds
G1 is addAdjVertex of G3,v1,e,v2
proof end;

theorem :: GLIB_006:128
for G3 being _Graph
for v1, e being object
for v2 being Vertex of G3
for G2 being addVertex of G3,v1
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G3 & not v1 in the_Vertices_of G3 holds
G1 is addAdjVertex of G3,v1,e,v2
proof end;

theorem Th133: :: GLIB_006:129
for G2 being _Graph
for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
v2 is Vertex of G1
proof end;

theorem Th134: :: GLIB_006:130
for G2 being _Graph
for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
v1 is Vertex of G1
proof end;

theorem Th135: :: GLIB_006:131
for G2 being _Graph
for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
( e DJoins v1,v2,G1 & e Joins v1,v2,G1 )
proof end;

theorem Th136: :: GLIB_006:132
for G2 being _Graph
for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
( e DJoins v1,v2,G1 & e Joins v1,v2,G1 )
proof end;

theorem Th137: :: GLIB_006:133
for G2 being _Graph
for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
for e1, w being object st ( w <> v1 or e1 <> e ) holds
not e1 Joins w,v2,G1
proof end;

theorem Th138: :: GLIB_006:134
for G2 being _Graph
for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
for e1, w being object st ( w <> v2 or e1 <> e ) holds
not e1 Joins v1,w,G1
proof end;

theorem Th139: :: GLIB_006:135
for G2 being _Graph
for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 holds G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G2
proof end;

theorem Th140: :: GLIB_006:136
for G2 being _Graph
for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 holds G2 is inducedSubgraph of G1,(the_Vertices_of G2)
proof end;

theorem Th141: :: GLIB_006:137
for G2 being _Graph
for v1 being Vertex of G2
for e being object
for v2 being set
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 holds
G2 is removeVertex of G1,v2
proof end;

theorem Th142: :: GLIB_006:138
for G2 being _Graph
for v1 being set
for e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds
G2 is removeVertex of G1,v1
proof end;

theorem :: GLIB_006:139
for G being non _trivial _Graph
for v1 being Vertex of G
for e, v2 being object
for G1 being addAdjVertex of G,v1,e,v2
for G2 being removeVertex of G1,v1
for G3 being removeVertex of G,v1 st not e in the_Edges_of G & not v2 in the_Vertices_of G holds
G2 is addVertex of G3,v2
proof end;

theorem :: GLIB_006:140
for G being non _trivial _Graph
for v1, e being object
for v2 being Vertex of G
for G1 being addAdjVertex of G,v1,e,v2
for G2 being removeVertex of G1,v2
for G3 being removeVertex of G,v2 st not e in the_Edges_of G & not v1 in the_Vertices_of G holds
G2 is addVertex of G3,v1
proof end;

:: What has been left out here is the Proof that the vertex to which
:: a new vertex with edge is added becomes a cut-vertex in the
:: resulting supergraph. A sketch of the Proof is commented below.
:: This theorem would be the easy way to show that any vertex in a (non
:: trivial) path graph that isn't an endvertex is a cut-vertex.
::
:: The difficulty of my Proofs lies in the difficulty of the Proofs of
:: the theorems my Proof would need. First there is
:: theorem (1) for G2 being non trivial _Graph, v1, e,v2 being object,
:: G1 being addAdjVertex of G2,v1,e,v2
:: holds G1.numComponents() = G2.numComponents();
:: which is not hard, just cumbersome. Then
:: theorem (2) for G being _Graph, v being Vertex of G,
:: G2 being removeVertex of G, v
:: st G2.numComponents() in G.numComponents()
:: holds v is isolated;
:: which is harder than it looks, especially since the converse has
:: already been proven in the preliminaries. I found it to need
:: theorem (3) for G being _Graph, u,v,w being Vertex of G
:: st v is non cut-vertex & u in G.reachableFrom(w)
:: holds ex W being Walk st W is_Walk_from w,u & not v in W.vertices();
:: for a contradiction Proof (take v to be non isolated, let w be a
:: neighbour of v; v is non cut-vertex by assumption, so use (3)
:: to show G2.reachableFrom(w) = G1.reachableFrom(w) \ {v},
:: deduce a bijection between component sets of G1 and G2 leading
:: to the contradiction).
:: Last theorem is
:: theorem (4) for G1 being non trivial _Graph, v being Vertex of G,
:: G2 being removeVertex of G1, v
:: st v is non isolated non cut-vertex
:: holds G1.numComponents() = G2.numComponents();
:: which is just a corrolary of (2) and the definition of cut-vertex.
:: Of course (2), (3) and (4) would belong into GLIB_002 to ease theorem
:: finding for future articles.
::
:: The dedicated reader is welcome to prove these theorems and the main one
:: below, or even find a shorter Proof (nevertheless theorems (1)-(3)
:: should be added to the MML because they are stating obvious facts).
::
::theorem
:: for G2 being non trivial _Graph, v1 being Vertex of G2, e,v2 being object,
:: G1 being addAdjVertex of G2,v1,e,v2, w being Vertex of G1
:: st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & w = v1
:: & v1 is non isolated
:: holds w is cut-vertex;
::proof
:: let G2 be non trivial _Graph, v1 be Vertex of G2, e,v2 be object;
:: let G1 be addAdjVertex of G2,v1,e,v2, w be Vertex of G1;
:: assume A1: not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & w=v1
:: & v1 is non isolated;
:: for G4 being removeVertex of G1,w holds
:: G1.numComponents() in G4.numComponents()
:: proof
:: let G4 be removeVertex of G1,w;
:: set G3 = the removeVertex of G2,v1;
:: G4 is removeVertex of G1,v1 by A1;
:: G4 is addVertex of G3, v2
:: C(G1) = C(G2) by (1)
:: C(G4) = C(G3)+1
:: if v1 is cut-vertex in G2:
:: ==> C(G2) in C(G3)
:: if C(G4) = C(G1)
:: ==> C(G1) = C(G4) = C(G3)+1
:: but C(G1)+1 = C(G2)+1 in C(G3)+1, hence contradiction
:: so C(G4) <> C(G1)
:: also C(G4) < C(G1) implies w is isolated by (2)
:: so C(G4) > C(G1) qed
:: if not v1 is cut-vertex in G2:
:: v1 is non isolated
:: ==> C(G3) = C(G2) by (4)
:: ==> C(G4) = C(G1)+1
:: ==> C(G1) in C(G4) qed
:: thus thesis;
:: end;
:: hence thesis by GLIB_002:def 10;
::end;
:: also don't forget the symmetric analogon
:: (for v1, e being object, v2 being Vertex of G2)
theorem Th145: :: GLIB_006:141
for G2 being _Graph
for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
for w being Vertex of G1 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & w = v2 holds
w is endvertex
proof end;

theorem Th146: :: GLIB_006:142
for G2 being _Graph
for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
for w being Vertex of G1 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & w = v1 holds
w is endvertex
proof end;

theorem Th147: :: GLIB_006:143
for G2 being _Graph
for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
not G1 is _trivial
proof end;

theorem Th148: :: GLIB_006:144
for G2 being _Graph
for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
not G1 is _trivial
proof end;

registration
let G be _Graph;
let v be Vertex of G;
cluster -> non _trivial for addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G;
coherence
for b1 being addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G holds not b1 is _trivial
proof end;
cluster -> non _trivial for addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v;
coherence
for b1 being addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v holds not b1 is _trivial
proof end;
end;

registration
let G be _trivial _Graph;
let v be Vertex of G;
cluster -> complete for addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G;
coherence
for b1 being addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G holds b1 is complete
proof end;
cluster -> complete for addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v;
coherence
for b1 being addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v holds b1 is complete
proof end;
end;

registration
let G be loopless _Graph;
let v1, e, v2 be object ;
cluster -> loopless for addAdjVertex of G,v1,e,v2;
coherence
for b1 being addAdjVertex of G,v1,e,v2 holds b1 is loopless
proof end;
end;

registration
let G be non-Dmulti _Graph;
let v1, e, v2 be object ;
cluster -> non-Dmulti for addAdjVertex of G,v1,e,v2;
coherence
for b1 being addAdjVertex of G,v1,e,v2 holds b1 is non-Dmulti
proof end;
end;

registration
let G be non-multi _Graph;
let v1, e, v2 be object ;
cluster -> non-multi for addAdjVertex of G,v1,e,v2;
coherence
for b1 being addAdjVertex of G,v1,e,v2 holds b1 is non-multi
proof end;
end;

registration
let G be Dsimple _Graph;
let v1, e, v2 be object ;
cluster -> Dsimple for addAdjVertex of G,v1,e,v2;
coherence
for b1 being addAdjVertex of G,v1,e,v2 holds b1 is Dsimple
;
end;

registration
let G be simple _Graph;
let v1, e, v2 be object ;
cluster -> simple for addAdjVertex of G,v1,e,v2;
coherence
for b1 being addAdjVertex of G,v1,e,v2 holds b1 is simple
;
end;

theorem Th149: :: GLIB_006:145
for G2 being _Graph
for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
for W being Walk of G1 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & ( ( not e in W .edges() & W is V5() ) or not v2 in W .vertices() ) holds
W is Walk of G2
proof end;

theorem Th150: :: GLIB_006:146
for G2 being _Graph
for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
for W being Walk of G1 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & ( ( not e in W .edges() & W is V5() ) or not v1 in W .vertices() ) holds
W is Walk of G2
proof end;

theorem Th151: :: GLIB_006:147
for G2 being _Graph
for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
for T being Trail of G1 st not e in the_Edges_of G2 & T .first() in the_Vertices_of G2 & T .last() in the_Vertices_of G2 holds
not e in T .edges()
proof end;

registration
let G be connected _Graph;
let v1, e, v2 be object ;
cluster -> connected for addAdjVertex of G,v1,e,v2;
coherence
for b1 being addAdjVertex of G,v1,e,v2 holds b1 is connected
proof end;
end;

registration
let G be non connected _Graph;
let v1, e, v2 be object ;
cluster -> non connected for addAdjVertex of G,v1,e,v2;
coherence
for b1 being addAdjVertex of G,v1,e,v2 holds not b1 is connected
proof end;
end;

registration
let G be acyclic _Graph;
let v1, e, v2 be object ;
cluster -> acyclic for addAdjVertex of G,v1,e,v2;
coherence
for b1 being addAdjVertex of G,v1,e,v2 holds b1 is acyclic
proof end;
end;

registration
let G be Tree-like _Graph;
let v1, e, v2 be object ;
cluster -> Tree-like for addAdjVertex of G,v1,e,v2;
coherence
for b1 being addAdjVertex of G,v1,e,v2 holds b1 is Tree-like
;
end;

theorem Th152: :: GLIB_006:148
for G2 being _Graph
for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & not G2 is _trivial holds
not G1 is complete
proof end;

theorem Th153: :: GLIB_006:149
for G2 being _Graph
for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & not G2 is _trivial holds
not G1 is complete
proof end;

registration
let G be non complete _Graph;
let v1, e, v2 be object ;
cluster -> non complete for addAdjVertex of G,v1,e,v2;
coherence
for b1 being addAdjVertex of G,v1,e,v2 holds not b1 is complete
proof end;
end;

registration
let G be non _trivial _Graph;
let v be Vertex of G;
cluster -> non complete for addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G;
coherence
for b1 being addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G holds not b1 is complete
proof end;
cluster -> non complete for addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v;
coherence
for b1 being addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v holds not b1 is complete
proof end;
end;

theorem :: GLIB_006:150
for G2 being _Graph
for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 holds
( G1 .order() = (G2 .order()) +` 1 & G1 .size() = (G2 .size()) +` 1 )
proof end;

theorem :: GLIB_006:151
for G2 being _Graph
for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds
( G1 .order() = (G2 .order()) +` 1 & G1 .size() = (G2 .size()) +` 1 )
proof end;

theorem :: GLIB_006:152
for G2 being _finite _Graph
for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 holds
( G1 .order() = (G2 .order()) + 1 & G1 .size() = (G2 .size()) + 1 )
proof end;

theorem :: GLIB_006:153
for G2 being _finite _Graph
for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds
( G1 .order() = (G2 .order()) + 1 & G1 .size() = (G2 .size()) + 1 )
proof end;

registration
let G be _finite _Graph;
let v1, e, v2 be object ;
cluster -> _finite for addAdjVertex of G,v1,e,v2;
coherence
for b1 being addAdjVertex of G,v1,e,v2 holds b1 is _finite
proof end;
end;