let G1 be _Graph; :: thesis:
let G2 be Dsimple _Graph; :: thesis:

hereby :: thesis:

assume G2 is DGraphComplement of G1 ; :: thesis:
then consider G9 being DLGraphComplement of G1 such that
A1: G2 is removeLoops of G9 by Def8;
thus the_Vertices_of G2 = the_Vertices_of G9 by A1, GLIB_000:def 33
.= the_Vertices_of G1 by Def6 ; :: thesis:
A2: the_Edges_of G2 c= the_Edges_of G9 by A1, GLIB_000:def 32;
the_Edges_of G9 misses the_Edges_of G1 by Def6;
hence the_Edges_of G2 misses the_Edges_of G1 by A2, XBOOLE_1:63; :: thesis:
let v, w be Vertex of G1; :: thesis:
assume A3: v <> w ; :: thesis:

hereby :: thesis:

given e1 being object such that A4: e1 DJoins v,w,G1 ; :: thesis:
given e2 being object such that A5: e2 DJoins v,w,G2 ; :: thesis:
e2 DJoins v,w,G9 by A1, A5, GLIB_000:72;
hence contradiction by A4, Th46; :: thesis:

end;

assume A6: for e2 being object holds not e2 DJoins v,w,G2 ; :: thesis:
for e9 being object holds not e9 DJoins v,w,G9

proof

given e9 being object such that A7: e9 DJoins v,w,G9 ; :: thesis:
A8: e9 in the_Edges_of G9 by A7, GLIB_000:def 14;
e9 Joins v,w,G9 by A7, GLIB_000:16;
then not e9 in G9 .loops() by A3, GLIB_009:46;
then e9 in (the_Edges_of G9) \ (G9 .loops()) by A8, XBOOLE_0:def 5;
then A9: e9 in the_Edges_of G2 by A1, GLIB_000:53;
e9 DJoins v,w,G2 by A1, A7, A9, GLIB_000:73;
hence contradiction by A6; :: thesis:

end;

hence ex e1 being object st e1 DJoins v,w,G1 by Def6; :: thesis:

end;

assume that
A10: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 ) and
A11: for v, w being Vertex of G1 st v <> w holds
( ex e1 being object st e1 DJoins v,w,G1 iff for e2 being object holds not e2 DJoins v,w,G2 ) ; :: thesis:

per cases ;

suppose A12: not G1 is loopfull ; :: thesis:

defpred S₁[ object ] means for e being object holds not e Joins $1,$1,G1;
consider V being Subset of (the_Vertices_of G2) such that
A13: for x being set holds
( x in V iff ( x in the_Vertices_of G2 & S₁[x] ) ) from SUBSET_1:sch 1();
A14: not V is empty by A10, A12, A13;
set E = { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ;
deffunc H₁( object ) -> object = $1 `2 ;
consider f being Function such that
A15: ( dom f = { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } & ( for x being object st x in { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();

now :: thesis:

let x1, x2 be object ; :: thesis:
assume A16: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis:
then consider v1 being Element of V such that
A17: x1 = [{(the_Edges_of G1),(the_Edges_of G2)},v1] by A15;
consider v2 being Element of V such that
A18: x2 = [{(the_Edges_of G1),(the_Edges_of G2)},v2] by A15, A16;
v1 = [{(the_Edges_of G1),(the_Edges_of G2)},v1] `2
.= f . x1 by A15, A16, A17
.= [{(the_Edges_of G1),(the_Edges_of G2)},v2] `2 by A15, A16, A18
.= v2 ;
hence x1 = x2 by A17, A18; :: thesis:

end;

then reconsider f = f as one-to-one Function by FUNCT_1:def 4;

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in rng f ; :: thesis:
then consider x being object such that
A19: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
consider v being Element of V such that
A20: x = [{(the_Edges_of G1),(the_Edges_of G2)},v] by A15, A19;
y = [{(the_Edges_of G1),(the_Edges_of G2)},v] `2 by A15, A19, A20
.= v ;
hence y in V by A14; :: thesis:

end;

set x = [{(the_Edges_of G1),(the_Edges_of G2)},y];
assume y in V ; :: thesis:
then A21: [{(the_Edges_of G1),(the_Edges_of G2)},y] in { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ;
then f . [{(the_Edges_of G1),(the_Edges_of G2)},y] = [{(the_Edges_of G1),(the_Edges_of G2)},y] `2 by A15
.= y ;
hence y in rng f by A15, A21, FUNCT_1:3; :: thesis:

end;

then A22: rng f = V by TARSKI:2;
A23: { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } misses the_Edges_of G1

proof

end;

A29: { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } misses the_Edges_of G2

proof

end;

set s = (the_Source_of G2) +* f;

now :: thesis:

thus dom ((the_Source_of G2) +* f) = (dom (the_Source_of G2)) \/ (dom f) by FUNCT_4:def 1
.= (the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } by A15, FUNCT_2:def 1 ; :: thesis:
A35: rng ((the_Source_of G2) +* f) c= (rng (the_Source_of G2)) \/ (rng f) by FUNCT_4:17;
(rng (the_Source_of G2)) \/ (rng f) c= the_Vertices_of G2 by A22, XBOOLE_1:8;
hence rng ((the_Source_of G2) +* f) c= the_Vertices_of G2 by A35, XBOOLE_1:1; :: thesis:

end;

then reconsider s = (the_Source_of G2) +* f as Function of ((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),(the_Vertices_of G2) by FUNCT_2:2;
set t = (the_Target_of G2) +* f;

now :: thesis:

thus dom ((the_Target_of G2) +* f) = (dom (the_Target_of G2)) \/ (dom f) by FUNCT_4:def 1
.= (the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } by A15, FUNCT_2:def 1 ; :: thesis:
A36: rng ((the_Target_of G2) +* f) c= (rng (the_Target_of G2)) \/ (rng f) by FUNCT_4:17;
(rng (the_Target_of G2)) \/ (rng f) c= the_Vertices_of G2 by A22, XBOOLE_1:8;
hence rng ((the_Target_of G2) +* f) c= the_Vertices_of G2 by A36, XBOOLE_1:1; :: thesis:

end;

then reconsider t = (the_Target_of G2) +* f as Function of ((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),(the_Vertices_of G2) by FUNCT_2:2;
set G9 = createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t);

now :: thesis:

thus the_Vertices_of G2 c= the_Vertices_of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t)) ; :: thesis:
thus the_Edges_of G2 c= the_Edges_of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t)) by XBOOLE_1:7; :: thesis:
let e be set ; :: thesis:
assume A37: e in the_Edges_of G2 ; :: thesis:
then e in (the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } by XBOOLE_0:def 3;
then A38: not e in dom f by A15, A29, A37, XBOOLE_0:5;
hence (the_Source_of G2) . e = ((the_Source_of G2) +* f) . e by FUNCT_4:11
.= (the_Source_of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t))) . e ;
:: thesis:
thus (the_Target_of G2) . e = ((the_Target_of G2) +* f) . e by A38, FUNCT_4:11
.= (the_Target_of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t))) . e ; :: thesis:

end;

hence createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t) is Supergraph of G2 by GLIB_006:def 9; :: thesis:
thus the_Vertices_of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t)) = the_Vertices_of G2 ; :: thesis:
reconsider E = { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } as set ;
reconsider f = f as one-to-one Function ;
take E = E; :: thesis:
take f = f; :: thesis:
thus E misses the_Edges_of G2 by A29; :: thesis:
thus the_Edges_of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t)) = (the_Edges_of G2) \/ E ; :: thesis:
thus dom f = E by A15; :: thesis:
thus rng f = V by A22; :: thesis:
thus the_Source_of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t)) = (the_Source_of G2) +* f ; :: thesis:
thus the_Target_of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t)) = (the_Target_of G2) +* f ; :: thesis:

end;

then A39: createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t) is addLoops of G2,V by Def5;
then G2 == the removeLoops of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t)) by Th26;
then A40: G2 is removeLoops of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t)) by GLIB_009:59;
A41: createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t) is non-Dmulti by A39;

now :: thesis:

thus the_Vertices_of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t)) = the_Vertices_of G1 by A10; :: thesis:
thus the_Edges_of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t)) misses the_Edges_of G1 by A10, A23, XBOOLE_1:70; :: thesis:
let v, w be Vertex of G1; :: thesis:

hereby :: thesis:

given e1 being object such that A43: e1 DJoins v,w,G1 ; :: thesis:
given e2 being object such that A44: e2 DJoins v,w, createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t) ; :: thesis:

per cases by A39, A44, GLIB_006:71;

suppose A45: e2 DJoins v,w,G2 ; :: thesis:

then v <> w by GLIB_000:136;
hence contradiction by A11, A43, A45; :: thesis:

end;

suppose A46: not e2 in the_Edges_of G2 ; :: thesis:

e2 in the_Edges_of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t)) by A44, GLIB_000:def 14;
then A47: e2 in { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } by A46, XBOOLE_0:def 3;
then consider u being Element of V such that
A48: e2 = [{(the_Edges_of G1),(the_Edges_of G2)},u] ;
A49: for e being object holds not e Joins u,u,G1 by A13, A14;
A50: v = (the_Source_of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t))) . e2 by A44, GLIB_000:def 14
.= s . e2
.= f . e2 by A15, A47, FUNCT_4:13
.= [{(the_Edges_of G1),(the_Edges_of G2)},u] `2 by A15, A47, A48
.= u ;
A51: w = (the_Target_of (createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t))) . e2 by A44, GLIB_000:def 14
.= t . e2
.= f . e2 by A15, A47, FUNCT_4:13
.= [{(the_Edges_of G1),(the_Edges_of G2)},u] `2 by A15, A47, A48
.= u ;
e1 Joins v,w,G1 by A43, GLIB_000:16;
hence contradiction by A49, A50, A51; :: thesis:

end;

assume A52: for e2 being object holds not e2 DJoins v,w, createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t) ; :: thesis:
assume A53: for e1 being object holds not e1 DJoins v,w,G1 ; :: thesis:

per cases ;

suppose A54: v <> w ; :: thesis:

for e2 being object holds not e2 DJoins v,w,G2 by A39, A52, GLIB_006:70;
hence contradiction by A11, A53, A54; :: thesis:

end;

suppose A55: v = w ; :: thesis:

set e = [{(the_Edges_of G1),(the_Edges_of G2)},v];
A56: for e1 being object holds not e1 Joins v,v,G1

proof

given e1 being object such that A57: e1 Joins v,v,G1 ; :: thesis:
e1 DJoins v,v,G1 by A57, GLIB_000:16;
hence contradiction by A53, A55; :: thesis:

end;

end;

then createGraph ((the_Vertices_of G2),((the_Edges_of G2) \/ { [{(the_Edges_of G1),(the_Edges_of G2)},v] where v is Element of V : verum } ),s,t) is DLGraphComplement of G1 by A41, Def6;
hence G2 is DGraphComplement of G1 by A40, Def8; :: thesis:

end;

suppose A61: G1 is loopfull ; :: thesis:

now :: thesis:

let v, w be Vertex of G1; :: thesis:

hereby :: thesis:

given e1 being object such that A62: e1 DJoins v,w,G1 ; :: thesis:

per cases ;

suppose v <> w ; :: thesis:

hence for e2 being object holds not e2 DJoins v,w,G2 by A11, A62; :: thesis:

end;

suppose v = w ; :: thesis:

hence for e2 being object holds not e2 DJoins v,w,G2 by GLIB_000:136; :: thesis:

end;

assume A63: for e2 being object holds not e2 DJoins v,w,G2 ; :: thesis:

per cases ;

suppose v <> w ; :: thesis:

hence ex e1 being object st e1 DJoins v,w,G1 by A11, A63; :: thesis:

end;

suppose v = w ; :: thesis:

hence ex e1 being object st e1 DJoins v,w,G1 by A61, Th1; :: thesis:

end;

then A64: G2 is DLGraphComplement of G1 by A10, Def6;
G2 is removeLoops of G2 by GLIB_009:58;
hence G2 is DGraphComplement of G1 by A64, Def8; :: thesis:

end;