let G1 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be Subset of (the_Vertices_of G1); :: thesis:
let G2 be addAdjVertexAll of G1,v,V; :: thesis:
let G3 be GraphComplement of G1; :: thesis:
assume A1: ( not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3 ) ; :: thesis:
consider E0 being set such that
( card V = card E0 & E0 misses the_Edges_of G1 ) and
the_Edges_of G2 = (the_Edges_of G1) \/ E0 and
A2: for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E0 & e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) ) by A1, GLIB_007:def 4;

per cases ) \ V <> {} or (the_Vertices_of G1) \ V = {} ) ;

suppose A3: (the_Vertices_of G1) \ V <> {} ; :: thesis:

set E = { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } ;
deffunc H₁( object ) -> object = $1 `2 ;
consider h being Function such that
A4: ( dom h = { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } & ( for x being object st x in { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } holds
h . x = H₁(x) ) ) from FUNCT_1:sch 3();
set s = (the_Source_of G3) +* h;
A5: dom ((the_Source_of G3) +* h) = (dom (the_Source_of G3)) \/ (dom h) by FUNCT_4:def 1
.= (the_Edges_of G3) \/ { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } by A4, FUNCT_2:def 1 ;

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

set x = [{(the_Edges_of G2),(the_Edges_of G3)},y];
assume y in (the_Vertices_of G1) \ V ; :: thesis:
then A6: [{(the_Edges_of G2),(the_Edges_of G3)},y] in { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } ;
then h . [{(the_Edges_of G2),(the_Edges_of G3)},y] = [{(the_Edges_of G2),(the_Edges_of G3)},y] `2 by A4
.= y ;
hence y in rng h by A4, A6, FUNCT_1:def 3; :: thesis:

end;

assume y in rng h ; :: thesis:
then consider x being object such that
A7: ( x in dom h & h . x = y ) by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
consider w being Element of (the_Vertices_of G1) \ V such that
A8: x = [{(the_Edges_of G2),(the_Edges_of G3)},w] by A4, A7;
h . x = x `2 by A4, A7
.= w by A8 ;
hence y in (the_Vertices_of G1) \ V by A3, A7; :: thesis:

end;

proof

end;

A21: { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } misses the_Edges_of G2

proof

end;

set G4 = createGraph (((the_Vertices_of G3) \/ {v}),((the_Edges_of G3) \/ { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } ),s,t);

now :: thesis:

thus the_Vertices_of G3 c= the_Vertices_of (createGraph (((the_Vertices_of G3) \/ {v}),((the_Edges_of G3) \/ { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } ),s,t)) by XBOOLE_1:7; :: thesis:
thus the_Edges_of G3 c= the_Edges_of (createGraph (((the_Vertices_of G3) \/ {v}),((the_Edges_of G3) \/ { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } ),s,t)) by XBOOLE_1:7; :: thesis:
let e be set ; :: thesis:
assume A26: e in the_Edges_of G3 ; :: thesis:
then e in (the_Edges_of G3) \/ { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } by XBOOLE_0:def 3;
then A27: not e in { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } by A16, A26, XBOOLE_0:5;
then A28: not e in dom ( { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } --> v) ;
thus (the_Source_of G3) . e = s . e by A4, A27, FUNCT_4:11
.= (the_Source_of (createGraph (((the_Vertices_of G3) \/ {v}),((the_Edges_of G3) \/ { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } ),s,t))) . e ; :: thesis:
thus (the_Target_of G3) . e = t . e by A28, FUNCT_4:11
.= (the_Target_of (createGraph (((the_Vertices_of G3) \/ {v}),((the_Edges_of G3) \/ { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } ),s,t))) . e ; :: thesis:

end;

then reconsider G4 = createGraph (((the_Vertices_of G3) \/ {v}),((the_Edges_of G3) \/ { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } ),s,t) as Supergraph of G3 by GLIB_006:def 9;
(the_Vertices_of G1) \ V c= the_Vertices_of G1 ;
then A29: ( (the_Vertices_of G1) \ V c= the_Vertices_of G3 & not v in the_Vertices_of G3 ) by A1, Th98;

now :: thesis:

thus the_Vertices_of G4 = (the_Vertices_of G3) \/ {v} ; :: thesis:

hereby :: thesis:

let e be object ; :: thesis:
thus not e Joins v,v,G4 :: thesis:

proof

assume A30: e Joins v,v,G4 ; :: thesis:

per cases by GLIB_006:72;

suppose e Joins v,v,G3 ; :: thesis:

then v in the_Vertices_of G3 by GLIB_000:13;
hence contradiction by A1, Th98; :: thesis:

end;

suppose A31: not e in the_Edges_of G3 ; :: thesis:

e in the_Edges_of G4 by A30, GLIB_000:def 13;
then e in (the_Edges_of G3) \/ { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } ;
then A32: e in { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } by A16, A31, XBOOLE_0:5;
then consider w being Element of (the_Vertices_of G1) \ V such that
A33: e = [{(the_Edges_of G2),(the_Edges_of G3)},w] ;
(the_Source_of G4) . e = s . e
.= h . e by A4, A32, FUNCT_4:13
.= [{(the_Edges_of G2),(the_Edges_of G3)},w] `2 by A4, A32, A33
.= w ;
then v = w by A30, GLIB_000:def 13;
then v in (the_Vertices_of G1) \ V by A3;
hence contradiction by A1; :: thesis:

end;

let v1 be object ; :: thesis:

hereby :: thesis:

assume A34: not v1 in (the_Vertices_of G1) \ V ; :: thesis:
assume A35: e Joins v1,v,G4 ; :: thesis:

per cases by GLIB_006:72;

suppose e Joins v1,v,G3 ; :: thesis:

then v in the_Vertices_of G3 by GLIB_000:13;
hence contradiction by A1, Th98; :: thesis:

end;

suppose A36: not e in the_Edges_of G3 ; :: thesis:

e in the_Edges_of G4 by A35, GLIB_000:def 13;
then e in (the_Edges_of G3) \/ { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } ;
then A37: e in { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } by A36, XBOOLE_0:def 3;
then consider w being Element of (the_Vertices_of G1) \ V such that
A38: e = [{(the_Edges_of G2),(the_Edges_of G3)},w] ;
(the_Source_of G4) . e = s . e
.= h . e by A4, A37, FUNCT_4:13
.= [{(the_Edges_of G2),(the_Edges_of G3)},w] `2 by A4, A37, A38
.= w ;

per cases by A35, GLIB_000:def 13;

suppose w = v ; :: thesis:

then v in (the_Vertices_of G1) \ V by A3;
hence contradiction by A1; :: thesis:

end;

suppose w = v1 ; :: thesis:

hence contradiction by A3, A34; :: thesis:

end;

let v2 be object ; :: thesis:
assume A39: ( v1 <> v & v2 <> v & e DJoins v1,v2,G4 ) ; :: thesis:
e in the_Edges_of G3

proof

assume A40: not e in the_Edges_of G3 ; :: thesis:
e in the_Edges_of G4 by A39, GLIB_000:def 14;
then e in (the_Edges_of G3) \/ { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } ;
then A41: e in { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } by A40, XBOOLE_0:def 3;
then A42: e in dom ( { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } --> v) ;
(the_Target_of G4) . e = t . e
.= ( { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } --> v) . e by A42, FUNCT_4:13
.= v by A41, FUNCOP_1:7 ;
hence contradiction by A39, GLIB_000:def 14; :: thesis:

end;

hence e DJoins v1,v2,G3 by A39, GLIB_006:71; :: thesis:

end;

take E = { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } ; :: thesis:

now :: thesis:

let x1, x2 be object ; :: thesis:
assume A43: ( x1 in dom h & x2 in dom h & h . x1 = h . x2 ) ; :: thesis:
then consider w1 being Element of (the_Vertices_of G1) \ V such that
A44: x1 = [{(the_Edges_of G2),(the_Edges_of G3)},w1] by A4;
consider w2 being Element of (the_Vertices_of G1) \ V such that
A45: x2 = [{(the_Edges_of G2),(the_Edges_of G3)},w2] by A4, A43;
w1 = [{(the_Edges_of G2),(the_Edges_of G3)},w1] `2
.= h . x1 by A4, A43, A44
.= [{(the_Edges_of G2),(the_Edges_of G3)},w2] `2 by A4, A43, A45
.= w2 ;
hence x1 = x2 by A44, A45; :: thesis:

end;

then A46: h is one-to-one by FUNCT_1:def 4;
thus card ((the_Vertices_of G1) \ V) = card ((the_Vertices_of G3) \ V) by Th98
.= card E by A4, A9, A46, CARD_1:70 ; :: thesis:
thus E misses the_Edges_of G3 by A16; :: thesis:
thus the_Edges_of G4 = (the_Edges_of G3) \/ E ; :: thesis:
let v1 be object ; :: thesis:
assume A47: v1 in (the_Vertices_of G1) \ V ; :: thesis:
set e1 = [{(the_Edges_of G2),(the_Edges_of G3)},v1];
take e1 = [{(the_Edges_of G2),(the_Edges_of G3)},v1]; :: thesis:
thus A48: e1 in E by A47; :: thesis:
then e1 in (the_Edges_of G3) \/ E by XBOOLE_0:def 3;
then A49: e1 in the_Edges_of G4 ;
A50: e1 in dom (E --> v) by A48;
A51: (the_Source_of G4) . e1 = s . e1
.= h . e1 by A4, A48, FUNCT_4:13
.= e1 `2 by A4, A48
.= v1 ;
(the_Target_of G4) . e1 = t . e1
.= (E --> v) . e1 by A50, FUNCT_4:13
.= v by A48, FUNCOP_1:7 ;
hence e1 Joins v1,v,G4 by A49, A51, GLIB_000:def 13; :: thesis:
let e2 be object ; :: thesis:
assume A52: e2 Joins v1,v,G4 ; :: thesis:
not e2 Joins v1,v,G3

proof

assume e2 Joins v1,v,G3 ; :: thesis:
then v in the_Vertices_of G3 by GLIB_000:13;
hence contradiction by A1, Th98; :: thesis:

end;

then A53: not e2 in the_Edges_of G3 by A52, GLIB_006:72;
e2 in the_Edges_of G4 by A52, GLIB_000:def 13;
then e2 in (the_Edges_of G3) \/ E ;
then A54: e2 in E by A53, XBOOLE_0:def 3;
then consider w being Element of (the_Vertices_of G1) \ V such that
A55: e2 = [{(the_Edges_of G2),(the_Edges_of G3)},w] ;
(the_Source_of G4) . e2 = s . e2
.= h . e2 by A4, A54, FUNCT_4:13
.= [{(the_Edges_of G2),(the_Edges_of G3)},w] `2 by A4, A54, A55
.= w ;
then A56: ( v = w or v1 = w ) by A52, GLIB_000:def 13;
v1 = w

proof

assume v1 <> w ; :: thesis:
then v in (the_Vertices_of G1) \ V by A3, A56;
hence contradiction by A1; :: thesis:

end;

hence e1 = e2 by A55; :: thesis:

end;

then reconsider G4 = G4 as addAdjVertexAll of G3,v,(the_Vertices_of G1) \ V by A29, GLIB_007:def 4;
take G4 ; :: thesis:

now :: thesis:

thus the_Vertices_of G4 = (the_Vertices_of G3) \/ {v}
.= (the_Vertices_of G1) \/ {v} by Th98
.= the_Vertices_of G2 by A1, GLIB_007:def 4 ; :: thesis:
(the_Edges_of G3) \/ { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } misses the_Edges_of G2 by A1, A21, XBOOLE_1:70;
hence the_Edges_of G4 misses the_Edges_of G2 ; :: thesis:
let u, w be Vertex of G2; :: thesis:
assume A57: u <> w ; :: thesis:

hereby :: thesis:

given e1 being object such that A58: e1 Joins u,w,G2 ; :: thesis:

per cases by A58, GLIB_006:72;

suppose A59: e1 Joins u,w,G1 ; :: thesis:

then ( u is Vertex of G1 & w is Vertex of G1 ) by GLIB_000:13;
then A60: for e2 being object holds not e2 Joins u,w,G3 by A57, A59, Th98;
( u <> v & w <> v ) by A1, A59, GLIB_000:13;
hence for e2 being object holds not e2 Joins u,w,G4 by A29, A60, GLIB_007:49; :: thesis:

end;

suppose A61: not e1 in the_Edges_of G1 ; :: thesis:

A62: the_Edges_of G2 = (the_Edges_of G1) \/ (G2 .edgesBetween (V,{v})) by A1, GLIB_007:59;
e1 in the_Edges_of G2 by A58, GLIB_000:def 13;
then e1 in G2 .edgesBetween (V,{v}) by A61, A62, XBOOLE_0:def 3;
then e1 SJoins V,{v},G2 by GLIB_000:def 30;
then ( ( (the_Source_of G2) . e1 in V & (the_Target_of G2) . e1 in {v} ) or ( (the_Source_of G2) . e1 in {v} & (the_Target_of G2) . e1 in V ) ) by GLIB_000:def 15;
then A63: ( ( u in V & w in {v} ) or ( u in {v} & w in V ) ) by A58, GLIB_000:def 13;
then A64: ( ( u = v & w in V ) or ( u in V & w = v ) ) by TARSKI:def 1;
thus for e2 being object holds not e2 Joins u,w,G4 :: thesis:

proof

given e2 being object such that A65: e2 Joins u,w,G4 ; :: thesis:
A66: not e2 in the_Edges_of G3

proof

assume e2 in the_Edges_of G3 ; :: thesis:
then e2 Joins u,w,G3 by A65, GLIB_006:72;
then v in the_Vertices_of G3 by A64, GLIB_000:13;
hence contradiction by A1, Th98; :: thesis:

end;

e2 in the_Edges_of G4 by A65, GLIB_000:def 13;
then e2 in (the_Edges_of G3) \/ { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } ;
then A67: e2 in { [{(the_Edges_of G2),(the_Edges_of G3)},w] where w is Element of (the_Vertices_of G1) \ V : verum } by A66, XBOOLE_0:def 3;
then consider x being Element of (the_Vertices_of G1) \ V such that
A68: e2 = [{(the_Edges_of G2),(the_Edges_of G3)},x] ;
(the_Source_of G4) . e2 = s . e2
.= h . e2 by A4, A67, FUNCT_4:13
.= [{(the_Edges_of G2),(the_Edges_of G3)},x] `2 by A4, A67, A68
.= x ;
then ( (the_Source_of G4) . e2 in the_Vertices_of G1 & not (the_Source_of G4) . e2 in V ) by A3, XBOOLE_0:def 5;

per cases by A65, GLIB_000:def 13;

suppose ( u in the_Vertices_of G1 & not u in V ) ; :: thesis:

hence contradiction by A1, A63, TARSKI:def 1; :: thesis:

end;

suppose ( w in the_Vertices_of G1 & not w in V ) ; :: thesis:

hence contradiction by A1, A63, TARSKI:def 1; :: thesis:

end;

assume A69: for e2 being object holds not e2 Joins u,w,G4 ; :: thesis:
A70: for e2 being object holds not e2 Joins u,w,G3 by A69, GLIB_006:70;

per cases ;

suppose A71: u = v ; :: thesis:

A72: not w in {v} by A57, A71, TARSKI:def 1;
w in V

proof

end;

then consider e1 being object such that
A79: ( e1 in E0 & e1 Joins w,v,G2 ) and
for e2 being object st e2 Joins w,v,G2 holds
e1 = e2 by A2;
take e1 = e1; :: thesis:
thus e1 Joins u,w,G2 by A71, A79, GLIB_000:14; :: thesis:

end;

suppose A80: w = v ; :: thesis:

A81: not u in {v} by A57, A80, TARSKI:def 1;
u in V

proof

end;

then consider e1 being object such that
A88: ( e1 in E0 & e1 Joins u,v,G2 ) and
for e2 being object st e2 Joins u,v,G2 holds
e1 = e2 by A2;
take e1 = e1; :: thesis:
thus e1 Joins u,w,G2 by A80, A88; :: thesis:

end;

suppose ( u <> v & w <> v ) ; :: thesis:

then A89: ( not u in {v} & not w in {v} ) by TARSKI:def 1;
the_Vertices_of G2 = (the_Vertices_of G1) \/ {v} by A1, GLIB_007:def 4;
then ( u is Vertex of G1 & w is Vertex of G1 ) by A89, XBOOLE_0:def 3;
then consider e1 being object such that
A90: e1 Joins u,w,G1 by A57, A70, Th98;
take e1 = e1; :: thesis:
thus e1 Joins u,w,G2 by A90, GLIB_006:70; :: thesis:

end;

hence G4 is GraphComplement of G2 by Th98; :: thesis:

end;

suppose A91: (the_Vertices_of G1) \ V = {} ; :: thesis:

take G4 = the addAdjVertexAll of G3,v,(the_Vertices_of G1) \ V; :: thesis:
A92: G4 is addVertex of G3,v by A91, GLIB_007:55;

now :: thesis:

thus the_Vertices_of G4 = (the_Vertices_of G3) \/ {v} by A92, GLIB_006:def 10
.= (the_Vertices_of G1) \/ {v} by Th98
.= the_Vertices_of G2 by A1, GLIB_007:def 4 ; :: thesis:
the_Edges_of G3 = the_Edges_of G4 by A92, GLIB_006:def 10;
hence the_Edges_of G4 misses the_Edges_of G2 by A1; :: thesis:
let u, w be Vertex of G2; :: thesis:
assume A93: u <> w ; :: thesis:

hereby :: thesis:

given e1 being object such that A94: e1 Joins u,w,G2 ; :: thesis:

per cases by A94, GLIB_006:72;

suppose A95: e1 Joins u,w,G1 ; :: thesis:

then ( u is Vertex of G1 & w is Vertex of G1 ) by GLIB_000:13;
then for e2 being object holds not e2 Joins u,w,G3 by A93, A95, Th98;
hence for e2 being object holds not e2 Joins u,w,G4 by A92, GLIB_006:87; :: thesis:

end;

suppose A96: not e1 in the_Edges_of G1 ; :: thesis:

A97: the_Edges_of G2 = (the_Edges_of G1) \/ (G2 .edgesBetween (V,{v})) by A1, GLIB_007:59;
e1 in the_Edges_of G2 by A94, GLIB_000:def 13;
then e1 in G2 .edgesBetween (V,{v}) by A96, A97, XBOOLE_0:def 3;
then e1 SJoins V,{v},G2 by GLIB_000:def 30;
then ( ( (the_Source_of G2) . e1 in V & (the_Target_of G2) . e1 in {v} ) or ( (the_Source_of G2) . e1 in {v} & (the_Target_of G2) . e1 in V ) ) by GLIB_000:def 15;
then ( ( u in V & w in {v} ) or ( u in {v} & w in V ) ) by A94, GLIB_000:def 13;
then ( ( u in V & w = v ) or ( u = v & w in V ) ) by TARSKI:def 1;
then ( not u in the_Vertices_of G3 or not w in the_Vertices_of G3 ) by A1, Th98;
then for e2 being object holds not e2 Joins u,w,G3 by GLIB_000:13;
hence for e2 being object holds not e2 Joins u,w,G4 by A92, GLIB_006:87; :: thesis:

end;

assume for e2 being object holds not e2 Joins u,w,G4 ; :: thesis:
then A98: for e2 being object holds not e2 Joins u,w,G3 by A92, GLIB_006:87;
A99: the_Vertices_of G2 = (the_Vertices_of G1) \/ {v} by A1, GLIB_007:def 4;
the_Vertices_of G1 c= V by A91, XBOOLE_1:37;
then A100: V = the_Vertices_of G1 by XBOOLE_0:def 10;

per cases ;

suppose A101: u = v ; :: thesis:

then not w in {v} by A93, TARSKI:def 1;
then w in the_Vertices_of G1 by A99, XBOOLE_0:def 3;
then consider e1 being object such that
A102: ( e1 in E0 & e1 Joins w,v,G2 ) and
for e2 being object st e2 Joins w,v,G2 holds
e1 = e2 by A2, A100;
take e1 = e1; :: thesis:
thus e1 Joins u,w,G2 by A101, A102, GLIB_000:14; :: thesis:

end;

suppose A103: w = v ; :: thesis:

then not u in {v} by A93, TARSKI:def 1;
then u in the_Vertices_of G1 by A99, XBOOLE_0:def 3;
then consider e1 being object such that
A104: ( e1 in E0 & e1 Joins u,v,G2 ) and
for e2 being object st e2 Joins u,v,G2 holds
e1 = e2 by A2, A100;
take e1 = e1; :: thesis:
thus e1 Joins u,w,G2 by A103, A104; :: thesis:

end;

suppose ( u <> v & w <> v ) ; :: thesis:

then ( not u in {v} & not w in {v} ) by TARSKI:def 1;
then ( u is Vertex of G1 & w is Vertex of G1 ) by A99, XBOOLE_0:def 3;
then consider e1 being object such that
A105: e1 Joins u,w,G1 by A93, A98, Th98;
take e1 = e1; :: thesis:
thus e1 Joins u,w,G2 by A105, GLIB_006:70; :: thesis:

end;

hence G4 is GraphComplement of G2 by Th98; :: thesis:

end;