:: About Graph Complements
:: by Sebastian Koch
::
:: Received December 30, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


definition
let G be _Graph;
attr G is loopfull means :Def1: :: GLIB_012:def 1
 for v being Vertex of G ex e being object st e Joins v,v,G;
end;

:: deftheorem Def1 defines loopfull GLIB_012:def 1 :
for G being _Graph holds
( G is loopfull iff for v being Vertex of G ex e being object st e Joins v,v,G );

theorem Th1: :: GLIB_012:1
for G being _Graph holds
( G is loopfull iff for v being Vertex of G ex e being object st e DJoins v,v,G )
proof end;

theorem :: GLIB_012:2
for G being _Graph holds
( G is loopfull iff for v being Vertex of G holds v,v are_adjacent )
proof end;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] loopfull -> non loopless for set ;
coherence
for b1 being _Graph st b1 is loopfull holds
not b1 is loopless
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] non loopless _trivial -> loopfull for set ;
coherence
for b1 being _Graph st b1 is _trivial & not b1 is loopless holds
b1 is loopfull
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] complete loopfull for set ;
existence
ex b1 being _Graph st
( b1 is loopfull & b1 is complete )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] non loopfull for set ;
existence
not for b1 being _Graph holds b1 is loopfull
proof end;
end;

theorem Th3: :: GLIB_012:3
for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds
( G1 is loopfull iff G2 is loopfull )
proof end;

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

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

theorem Th4: :: GLIB_012:4
for G1, G2 being _Graph st G1 == G2 & G1 is loopfull holds
G2 is loopfull
proof end;

theorem Th5: :: GLIB_012:5
for G2 being loopfull _Graph
for G1 being Supergraph of G2 st the_Vertices_of G1 = the_Vertices_of G2 holds
G1 is loopfull
proof end;

theorem Th6: :: GLIB_012:6
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st rng (F _V) = the_Vertices_of G2 & G1 .loops() c= dom (F _E) & G1 is loopfull holds
G2 is loopfull
proof end;

theorem Th7: :: GLIB_012:7
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is total & F is onto & G1 is loopfull holds
G2 is loopfull
proof end;

theorem Th8: :: GLIB_012:8
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is semi-continuous & dom (F _V) = the_Vertices_of G1 & G2 .loops() c= rng (F _E) & G2 is loopfull holds
G1 is loopfull
proof end;

theorem Th9: :: GLIB_012:9
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is total & F is onto & F is semi-continuous & G2 is loopfull holds
G1 is loopfull
proof end;

theorem :: GLIB_012:10
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is loopfull iff G2 is loopfull ) by Th7, Th9;

registration
let G be loopfull _Graph;
let V be set ;
cluster -> loopfull for inducedSubgraph of G,V,G .edgesBetween V;
coherence
for b1 being inducedSubgraph of G,V holds b1 is loopfull
proof end;
cluster -> loopfull for inducedSubgraph of G,(the_Vertices_of G) \ V,G .edgesBetween ((the_Vertices_of G) \ V);
coherence
for b1 being removeVertices of G,V holds b1 is loopfull ;
cluster -> loopfull for inducedSubgraph of G,(the_Vertices_of G) \ {V},G .edgesBetween ((the_Vertices_of G) \ {V});
coherence
for b1 being removeVertex of G,V holds b1 is loopfull ;
end;

registration
let G be non loopfull _Graph;
cluster spanning -> spanning non loopfull for Subgraph of G;
coherence
for b1 being spanning Subgraph of G holds not b1 is loopfull
proof end;
let E be set ;
cluster -> non loopfull for inducedSubgraph of G, the_Vertices_of G,E;
coherence
for b1 being inducedSubgraph of G, the_Vertices_of G,E holds not b1 is loopfull
proof end;
cluster -> non loopfull for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E;
coherence
for b1 being removeEdges of G,E holds not b1 is loopfull ;
cluster -> non loopfull for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {E};
coherence
for b1 being removeEdge of G,E holds not b1 is loopfull ;
end;

theorem Th11: :: GLIB_012:11
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 loopfull
proof end;

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

registration
let G be loopfull _Graph;
let v, e, w be object ;
cluster -> loopfull for addEdge of G,v,e,w;
coherence
for b1 being addEdge of G,v,e,w holds b1 is loopfull
proof end;
end;

theorem Th12: :: GLIB_012:12
for G2 being _Graph
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds
not G1 is loopfull
proof end;

theorem Th13: :: GLIB_012:13
for G2 being _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
not G1 is loopfull
proof end;

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

theorem Th14: :: GLIB_012:14
for G2 being _Graph
for v being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2 holds
not G1 is loopfull
proof end;

registration
let G be non loopfull _Graph;
let v be object ;
let V be set ;
cluster -> non loopfull for addAdjVertexAll of G,v,V;
coherence
for b1 being addAdjVertexAll of G,v,V holds not b1 is loopfull
proof end;
end;

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

:: removeLoops is loopless, hence non loopfull
registration
let G be non loopfull _Graph;
cluster -> non loopfull for removeParallelEdges of G;
coherence
for b1 being removeParallelEdges of G holds not b1 is loopfull ;
cluster -> non loopfull for removeDParallelEdges of G;
coherence
for b1 being removeDParallelEdges of G holds not b1 is loopfull ;
end;

definition
let GF be Graph-yielding Function;
attr GF is loopfull means :Def2: :: GLIB_012:def 2
 for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is loopfull );
end;

:: deftheorem Def2 defines loopfull GLIB_012:def 2 :
for GF being Graph-yielding Function holds
( GF is loopfull iff for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is loopfull ) );

registration
let G be loopfull _Graph;
cluster <*G*> -> loopfull ;
coherence
<*G*> is loopfull
proof end;
cluster NAT --> G -> loopfull ;
coherence
NAT --> G is loopfull by FUNCOP_1:7;
end;

definition
let GF be non empty Graph-yielding Function;
redefine attr GF is loopfull means :Def3: :: GLIB_012:def 3
 for x being Element of dom GF holds GF . x is loopfull ;
compatibility
( GF is loopfull iff for x being Element of dom GF holds GF . x is loopfull )
proof end;
end;

:: deftheorem Def3 defines loopfull GLIB_012:def 3 :
for GF being non empty Graph-yielding Function holds
( GF is loopfull iff for x being Element of dom GF holds GF . x is loopfull );

Lm1: for F being ManySortedSet of NAT
for n being object holds
( n is Nat iff n in dom F )
proof end;

definition
let GSq be GraphSeq;
redefine attr GSq is loopfull means :Def4: :: GLIB_012:def 4
 for n being Nat holds GSq . n is loopfull ;
compatibility
( GSq is loopfull iff for n being Nat holds GSq . n is loopfull )
proof end;
end;

:: deftheorem Def4 defines loopfull GLIB_012:def 4 :
for GSq being GraphSeq holds
( GSq is loopfull iff for n being Nat holds GSq . n is loopfull );

registration
cluster empty Relation-like Function-like Graph-yielding -> Graph-yielding loopfull for set ;
coherence
for b1 being Graph-yielding Function st b1 is empty holds
b1 is loopfull ;
cluster non empty Relation-like Function-like Graph-yielding loopfull -> Graph-yielding non loopless for set ;
coherence
for b1 being Graph-yielding Function st not b1 is empty & b1 is loopfull holds
not b1 is loopless
proof end;
end;

registration
cluster non empty Relation-like NAT -defined Function-like total Graph-yielding loopfull for set ;
existence
ex b1 being GraphSeq st b1 is loopfull
proof end;
cluster non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Graph-yielding loopfull for set ;
existence
ex b1 being Graph-yielding FinSequence st
( not b1 is empty & b1 is loopfull )
proof end;
end;

registration
let GF be non empty Graph-yielding loopfull Function;
let x be Element of dom GF;
cluster GF . x -> loopfull ;
coherence
GF . x is loopfull by Def3;
end;

registration
let GSq be loopfull GraphSeq;
let x be Nat;
cluster GSq . x -> loopfull ;
coherence
GSq . x is loopfull by Def4;
end;

registration
let p be Graph-yielding loopfull FinSequence;
let n be Nat;
cluster p | n -> loopfull ;
coherence
p | n is loopfull
proof end;
cluster p /^ n -> loopfull ;
coherence
p /^ n is loopfull
proof end;
let m be Nat;
cluster smid (p,m,n) -> loopfull ;
coherence
smid (p,m,n) is loopfull
proof end;
cluster (m,n) -cut p -> loopfull ;
coherence
(m,n) -cut p is loopfull
proof end;
end;

registration
let p, q be Graph-yielding loopfull FinSequence;
cluster p ^ q -> loopfull ;
coherence
p ^ q is loopfull
proof end;
cluster p ^' q -> loopfull ;
coherence
p ^' q is loopfull
proof end;
end;

registration
let G1, G2 be loopfull _Graph;
cluster <*G1,G2*> -> loopfull ;
coherence
<*G1,G2*> is loopfull
proof end;
let G3 be loopfull _Graph;
cluster <*G1,G2,G3*> -> loopfull ;
coherence
<*G1,G2,G3*> is loopfull
proof end;
end;

:: a loop is added to each vertex in V, regardless if that
:: vertex has a loop already or not
definition
let G be _Graph;
let V be set ;
mode addLoops of G,V -> Supergraph of G means :Def5: :: GLIB_012:def 5
( the_Vertices_of it = the_Vertices_of G & ex E being set ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of it = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of it = (the_Source_of G) +* f & the_Target_of it = (the_Target_of G) +* f ) ) if V c= the_Vertices_of G
otherwise it == G;
existence
( ( V c= the_Vertices_of G implies ex b1 being Supergraph of G st
( the_Vertices_of b1 = the_Vertices_of G & ex E being set ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of b1 = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of b1 = (the_Source_of G) +* f & the_Target_of b1 = (the_Target_of G) +* f ) ) ) & ( not V c= the_Vertices_of G implies ex b1 being Supergraph of G st b1 == G ) )
proof end;
consistency
for b1 being Supergraph of G holds verum ;
end;

:: deftheorem Def5 defines addLoops GLIB_012:def 5 :
for G being _Graph
for V being set
for b3 being Supergraph of G holds
( ( V c= the_Vertices_of G implies ( b3 is addLoops of G,V iff ( the_Vertices_of b3 = the_Vertices_of G & ex E being set ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of b3 = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of b3 = (the_Source_of G) +* f & the_Target_of b3 = (the_Target_of G) +* f ) ) ) ) & ( not V c= the_Vertices_of G implies ( b3 is addLoops of G,V iff b3 == G ) ) );

definition
let G be _Graph;
mode addLoops of G is addLoops of G, the_Vertices_of G;
end;

theorem Th15: :: GLIB_012:15
for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds the_Vertices_of G1 = the_Vertices_of G2
proof end;

theorem Th16: :: GLIB_012:16
for G2 being _Graph
for V being set
for G1 being addLoops of G2,V
for e, v, w being object st v <> w holds
( e DJoins v,w,G1 iff e DJoins v,w,G2 )
proof end;

theorem Th17: :: GLIB_012:17
for G2 being _Graph
for V being set
for G1 being addLoops of G2,V
for e, v, w being object st v <> w holds
( e Joins v,w,G1 iff e Joins v,w,G2 )
proof end;

theorem :: GLIB_012:18
for G2 being _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V
for v being Vertex of G1 st v in V holds
v,v are_adjacent
proof end;

theorem :: GLIB_012:19
for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds G1 .order() = G2 .order() by Th15;

theorem :: GLIB_012:20
for G2 being _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V holds G1 .size() = (G2 .size()) +` (card V)
proof end;

theorem Th21: :: GLIB_012:21
for G1, G2 being _Graph holds
( G1 is addLoops of G2, {} iff G1 == G2 )
proof end;

theorem :: GLIB_012:22
for G being _Graph holds G is addLoops of G, {}
proof end;

theorem :: GLIB_012:23
for G being _Graph
for V1, V2 being Subset of (the_Vertices_of G)
for G1 being addLoops of G,V1
for G2 being addLoops of G1,V2 st V1 misses V2 holds
G2 is addLoops of G,V1 \/ V2
proof end;

theorem Th24: :: GLIB_012:24
for G3 being _Graph
for V1, V2 being Subset of (the_Vertices_of G3)
for G1 being addLoops of G3,V1 \/ V2 st V1 misses V2 holds
ex G2 being addLoops of G3,V1 st G1 is addLoops of G2,V2
proof end;

theorem Th25: :: GLIB_012:25
for G2 being loopless _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V holds
( the_Edges_of G2 misses G1 .loops() & the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .loops()) )
proof end;

theorem Th26: :: GLIB_012:26
for G1 being loopless _Graph
for V being set
for G2 being addLoops of G1,V
for G3 being removeLoops of G2 holds G1 == G3
proof end;

theorem Th27: :: GLIB_012:27
for G1, G2 being _Graph
for v being Vertex of G2 holds
( G1 is addLoops of G2,{v} iff ex e being object st
( not e in the_Edges_of G2 & G1 is addEdge of G2,v,e,v ) )
proof end;

Lm2: for p being non empty FinSequence
for x being object
for n being Element of dom (p ^ <*x*>) holds
( not n <= (len (p ^ <*x*>)) - 1 or n = (len (p ^ <*x*>)) - 1 or n <= (len p) - 1 )
proof end;

:: finite addition of loops can be finitely constructed with one loop at a time
theorem :: GLIB_012:28
for G2 being _Graph
for V being finite Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card V) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G2 ex e being object st
( p . (n + 1) is addEdge of p . n,v,e,v & v in V & not e in the_Edges_of (p . n) ) ) )
proof end;

theorem Th29: :: GLIB_012:29
for G3, G4 being _Graph
for V1, V2 being set
for G1 being addLoops of G3,V1
for G2 being addLoops of G4,V2
for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds
ex F being PGraphMapping of G1,G2 st
( F _V = F0 _V & (F _E) | (dom (F0 _E)) = F0 _E & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )
proof end;

theorem :: GLIB_012:30
for G3 being _Graph
for G4 being b1 -isomorphic _Graph
for G1 being addLoops of G3
for G2 being addLoops of G4 holds G2 is G1 -isomorphic
proof end;

theorem :: GLIB_012:31
for G3 being _Graph
for G4 being b1 -Disomorphic _Graph
for G1 being addLoops of G3
for G2 being addLoops of G4 holds G2 is G1 -Disomorphic
proof end;

theorem :: GLIB_012:32
for G3, G4 being _Graph
for V being set
for G1 being addLoops of G3,V
for G2 being addLoops of G4,V st G3 == G4 holds
G2 is G1 -Disomorphic
proof end;

theorem :: GLIB_012:33
for G3 being _Graph
for V, E being set
for G4 being reverseEdgeDirections of G3,E
for G1 being addLoops of G3,V
for G2 being addLoops of G4,V holds G2 is G1 -isomorphic
proof end;

theorem :: GLIB_012:34
for G3 being _Graph
for E, V being set
for G4 being reverseEdgeDirections of G3,E
for G1 being addLoops of G3,V
for G2 being reverseEdgeDirections of G1,E st E c= the_Edges_of G3 holds
G2 is addLoops of G4,V
proof end;

theorem :: GLIB_012:35
for G3 being _Graph
for V1 being Subset of (the_Vertices_of G3)
for V2 being non empty Subset of (the_Vertices_of G3)
for G4 being inducedSubgraph of G3,V2
for G1 being addLoops of G3,V1
for G2 being inducedSubgraph of G1,V2 holds G2 is addLoops of G4,V1 /\ V2
proof end;

theorem :: GLIB_012:36
for G2 being _Graph
for V being set
for G1 being addLoops of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st not v1 in V & v1 = v2 holds
( ( v1 is isolated implies v2 is isolated ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) )
proof end;

theorem Th37: :: GLIB_012:37
for G2 being _Graph
for V being set
for G1 being addLoops of G2,V
for P being Path of G1 holds
( P is Path of G2 or ex v, e being object st
( e Joins v,v,G1 & P = G1 .walkOf (v,e,v) ) )
proof end;

theorem :: GLIB_012:38
for G2 being _Graph
for V being set
for G1 being addLoops of G2,V
for W being Walk of G1 st W .edges() misses (G1 .loops()) \ (G2 .loops()) holds
W is Walk of G2
proof end;

registration
let G be _Graph;
cluster -> loopfull for addLoops of G, the_Vertices_of G;
coherence
for b1 being addLoops of G holds b1 is loopfull
proof end;
let V be non empty Subset of (the_Vertices_of G);
cluster -> non loopless for addLoops of G,V;
coherence
for b1 being addLoops of G,V holds not b1 is loopless
proof end;
end;

theorem Th39: :: GLIB_012:39
for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds
( G1 is _finite iff G2 is _finite )
proof end;

registration
let G be _finite _Graph;
let V be set ;
cluster -> _finite for addLoops of G,V;
coherence
for b1 being addLoops of G,V holds b1 is _finite by Th39;
end;

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

theorem Th40: :: GLIB_012:40
for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds
( G1 is connected iff G2 is connected )
proof end;

registration
let G be connected _Graph;
let V be set ;
cluster -> connected for addLoops of G,V;
coherence
for b1 being addLoops of G,V holds b1 is connected by Th40;
end;

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

theorem Th41: :: GLIB_012:41
for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds
( G1 is chordal iff G2 is chordal )
proof end;

registration
let G be chordal _Graph;
let V be set ;
cluster -> chordal for addLoops of G,V;
coherence
for b1 being addLoops of G,V holds b1 is chordal by Th41;
end;

:: non chordal clustering will be done later
registration
let G be non edgeless _Graph;
let V be set ;
cluster -> non edgeless for addLoops of G,V;
coherence
for b1 being addLoops of G,V holds not b1 is edgeless ;
end;

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

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

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

theorem Th42: :: GLIB_012:42
for G2 being _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 in V holds
ex e being object st
( e DJoins v1,v1,G1 & not e in the_Edges_of G2 & v1 .edgesIn() = (v2 .edgesIn()) \/ {e} & v1 .edgesOut() = (v2 .edgesOut()) \/ {e} & v1 .edgesInOut() = (v2 .edgesInOut()) \/ {e} )
proof end;

theorem :: GLIB_012:43
for G2 being _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 in V holds
( v1 .inDegree() = (v2 .inDegree()) +` 1 & v1 .outDegree() = (v2 .outDegree()) +` 1 & v1 .degree() = (v2 .degree()) +` 2 )
proof end;

theorem :: GLIB_012:44
for G2 being _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & not v1 in V holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )
proof end;

definition
let G be _Graph;
mode DLGraphComplement of G -> non-Dmulti _Graph means :Def6: :: GLIB_012:def 6
( the_Vertices_of it = the_Vertices_of G & the_Edges_of it misses the_Edges_of G & ( for v, w being Vertex of G holds
( ex e1 being object st e1 DJoins v,w,G iff for e2 being object holds not e2 DJoins v,w,it ) ) );
existence
ex b1 being non-Dmulti _Graph st
( the_Vertices_of b1 = the_Vertices_of G & the_Edges_of b1 misses the_Edges_of G & ( for v, w being Vertex of G holds
( ex e1 being object st e1 DJoins v,w,G iff for e2 being object holds not e2 DJoins v,w,b1 ) ) )
proof end;
end;

:: deftheorem Def6 defines DLGraphComplement GLIB_012:def 6 :
for G being _Graph
for b2 being non-Dmulti _Graph holds
( b2 is DLGraphComplement of G iff ( the_Vertices_of b2 = the_Vertices_of G & the_Edges_of b2 misses the_Edges_of G & ( for v, w being Vertex of G holds
( ex e1 being object st e1 DJoins v,w,G iff for e2 being object holds not e2 DJoins v,w,b2 ) ) ) );

theorem Th45: :: GLIB_012:45
for G1, G2, G3 being _Graph
for G4 being DLGraphComplement of G1 st G1 == G2 & G3 == G4 holds
G3 is DLGraphComplement of G2
proof end;

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

theorem Th46: :: GLIB_012:46
for G1 being _Graph
for G2 being DLGraphComplement of G1
for e1, e2, v, w being object st e1 DJoins v,w,G1 holds
not e2 DJoins v,w,G2
proof end;

theorem Th47: :: GLIB_012:47
for G1 being _Graph
for G2 being removeDParallelEdges of G1
for G3 being DLGraphComplement of G1 holds G3 is DLGraphComplement of G2
proof end;

theorem Th48: :: GLIB_012:48
for G1, G2 being _Graph
for G3 being removeDParallelEdges of G1
for G4 being removeDParallelEdges of G2
for G5 being DLGraphComplement of G1
for G6 being DLGraphComplement of G2 st G4 is G3 -Disomorphic holds
G6 is G5 -Disomorphic
proof end;

theorem Th49: :: GLIB_012:49
for G1 being _Graph
for G2 being b1 -Disomorphic _Graph
for G3 being DLGraphComplement of G1
for G4 being DLGraphComplement of G2 holds G4 is G3 -Disomorphic
proof end;

theorem Th50: :: GLIB_012:50
for G1 being _Graph
for G2, G3 being DLGraphComplement of G1 holds G3 is G2 -Disomorphic
proof end;

theorem :: GLIB_012:51
for G1 being _Graph
for G2 being reverseEdgeDirections of G1
for G3 being DLGraphComplement of G1
for G4 being reverseEdgeDirections of G3 holds G4 is DLGraphComplement of G2
proof end;

theorem Th52: :: GLIB_012:52
for G1 being _Graph
for V being non empty Subset of (the_Vertices_of G1)
for G2 being inducedSubgraph of G1,V
for G3 being DLGraphComplement of G1
for G4 being inducedSubgraph of G3,V holds G4 is DLGraphComplement of G2
proof end;

theorem :: GLIB_012:53
for G1 being _Graph
for V being proper Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V
for G3 being DLGraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is DLGraphComplement of G2
proof end;

:: involutiveness of graph complement (DLC case)
theorem :: GLIB_012:54
for G1 being non-Dmulti _Graph
for G2 being DLGraphComplement of G1 holds G1 is DLGraphComplement of G2
proof end;

theorem Th55: :: GLIB_012:55
for G1 being _Graph
for G2 being DLGraphComplement of G1 holds G1 .order() = G2 .order() by Def6;

theorem Th56: :: GLIB_012:56
for G1 being _Graph
for G2 being DLGraphComplement of G1 holds
( ( G1 is _trivial implies G2 is _trivial ) & ( G2 is _trivial implies G1 is _trivial ) & ( G1 is loopfull implies G2 is loopless ) & ( G2 is loopless implies G1 is loopfull ) & ( G1 is loopless implies G2 is loopfull ) & ( G2 is loopfull implies G1 is loopless ) )
proof end;

registration
let G be _trivial _Graph;
cluster -> _trivial for DLGraphComplement of G;
coherence
for b1 being DLGraphComplement of G holds b1 is _trivial by Th56;
end;

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

registration
let G be loopfull _Graph;
cluster -> loopless for DLGraphComplement of G;
coherence
for b1 being DLGraphComplement of G holds b1 is loopless by Th56;
end;

registration
let G be non loopfull _Graph;
cluster -> non loopless for DLGraphComplement of G;
coherence
for b1 being DLGraphComplement of G holds not b1 is loopless by Th56;
end;

registration
let G be loopless _Graph;
cluster -> loopfull for DLGraphComplement of G;
coherence
for b1 being DLGraphComplement of G holds b1 is loopfull by Th56;
end;

registration
let G be non loopless _Graph;
cluster -> non loopfull for DLGraphComplement of G;
coherence
for b1 being DLGraphComplement of G holds not b1 is loopfull by Th56;
end;

theorem Th57: :: GLIB_012:57
for G1 being _Graph
for G2 being DLGraphComplement of G1 st the_Edges_of G1 = G1 .loops() holds
G2 is complete
proof end;

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

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

theorem :: GLIB_012:58
for G1 being _Graph
for G2 being DLGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies not v2 is isolated ) & ( v1 is endvertex implies not v2 is endvertex ) )
proof end;

theorem :: GLIB_012:59
for G1 being _Graph
for G2 being DLGraphComplement of G1
for v, w being Vertex of G1 st ( for e being object holds not e Joins v,w,G1 ) holds
ex e being object st e Joins v,w,G2
proof end;

theorem Th60: :: GLIB_012:60
for G1 being _Graph
for G2 being DLGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = (the_Vertices_of G2) \ (v1 .inNeighbors()) & v2 .outNeighbors() = (the_Vertices_of G2) \ (v1 .outNeighbors()) )
proof end;

theorem :: GLIB_012:61
for G1 being _Graph
for G2 being DLGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
( v2 .inNeighbors() = the_Vertices_of G2 & v2 .outNeighbors() = the_Vertices_of G2 & v2 .allNeighbors() = the_Vertices_of G2 )
proof end;

definition
let G be _Graph;
mode LGraphComplement of G -> non-multi _Graph means :Def7: :: GLIB_012:def 7
( the_Vertices_of it = the_Vertices_of G & the_Edges_of it misses the_Edges_of G & ( for v, w being Vertex of G holds
( ex e1 being object st e1 Joins v,w,G iff for e2 being object holds not e2 Joins v,w,it ) ) );
existence
ex b1 being non-multi _Graph st
( the_Vertices_of b1 = the_Vertices_of G & the_Edges_of b1 misses the_Edges_of G & ( for v, w being Vertex of G holds
( ex e1 being object st e1 Joins v,w,G iff for e2 being object holds not e2 Joins v,w,b1 ) ) )
proof end;
end;

:: deftheorem Def7 defines LGraphComplement GLIB_012:def 7 :
for G being _Graph
for b2 being non-multi _Graph holds
( b2 is LGraphComplement of G iff ( the_Vertices_of b2 = the_Vertices_of G & the_Edges_of b2 misses the_Edges_of G & ( for v, w being Vertex of G holds
( ex e1 being object st e1 Joins v,w,G iff for e2 being object holds not e2 Joins v,w,b2 ) ) ) );

theorem Th62: :: GLIB_012:62
for G1, G2, G3 being _Graph
for G4 being LGraphComplement of G1 st G1 == G2 & G3 == G4 holds
G3 is LGraphComplement of G2
proof end;

registration
let G be _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] non-multi non-Dmulti plain for LGraphComplement of G;
existence
ex b1 being LGraphComplement of G st b1 is plain
proof end;
end;

theorem :: GLIB_012:63
for G1 being _Graph
for G2 being non-multi _Graph holds
( G2 is LGraphComplement of G1 iff ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 holds
( v1,w1 are_adjacent iff not v2,w2 are_adjacent ) ) ) )
proof end;

theorem Th64: :: GLIB_012:64
for G1 being _Graph
for G2 being LGraphComplement of G1
for e1, e2, v, w being object st e1 Joins v,w,G1 holds
not e2 Joins v,w,G2
proof end;

theorem Th65: :: GLIB_012:65
for G1 being _Graph
for G2 being removeParallelEdges of G1
for G3 being LGraphComplement of G1 holds G3 is LGraphComplement of G2
proof end;

theorem Th66: :: GLIB_012:66
for G1, G2 being _Graph
for G3 being removeParallelEdges of G1
for G4 being removeParallelEdges of G2
for G5 being LGraphComplement of G1
for G6 being LGraphComplement of G2 st G4 is G3 -isomorphic holds
G6 is G5 -isomorphic
proof end;

theorem Th67: :: GLIB_012:67
for G1 being _Graph
for G2 being b1 -isomorphic _Graph
for G3 being LGraphComplement of G1
for G4 being LGraphComplement of G2 holds G4 is G3 -isomorphic
proof end;

theorem Th68: :: GLIB_012:68
for G1 being _Graph
for G2, G3 being LGraphComplement of G1 holds G3 is G2 -isomorphic
proof end;

theorem Th69: :: GLIB_012:69
for G1 being _Graph
for V being non empty Subset of (the_Vertices_of G1)
for G2 being inducedSubgraph of G1,V
for G3 being LGraphComplement of G1
for G4 being inducedSubgraph of G3,V holds G4 is LGraphComplement of G2
proof end;

theorem :: GLIB_012:70
for G1 being _Graph
for V being proper Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V
for G3 being LGraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is LGraphComplement of G2
proof end;

:: involutiveness of graph complement (LC case)
theorem :: GLIB_012:71
for G1 being non-multi _Graph
for G2 being LGraphComplement of G1 holds G1 is LGraphComplement of G2
proof end;

theorem Th72: :: GLIB_012:72
for G1 being _Graph
for G2 being LGraphComplement of G1 holds G1 .order() = G2 .order() by Def7;

theorem Th73: :: GLIB_012:73
for G1 being _Graph
for G2 being LGraphComplement of G1 holds
( ( G1 is _trivial implies G2 is _trivial ) & ( G2 is _trivial implies G1 is _trivial ) & ( G1 is loopfull implies G2 is loopless ) & ( G2 is loopless implies G1 is loopfull ) & ( G1 is loopless implies G2 is loopfull ) & ( G2 is loopfull implies G1 is loopless ) )
proof end;

registration
let G be _trivial _Graph;
cluster -> _trivial for LGraphComplement of G;
coherence
for b1 being LGraphComplement of G holds b1 is _trivial by Th73;
end;

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

registration
let G be loopfull _Graph;
cluster -> loopless for LGraphComplement of G;
coherence
for b1 being LGraphComplement of G holds b1 is loopless by Th73;
end;

registration
let G be non loopfull _Graph;
cluster -> non loopless for LGraphComplement of G;
coherence
for b1 being LGraphComplement of G holds not b1 is loopless by Th73;
end;

registration
let G be loopless _Graph;
cluster -> loopfull for LGraphComplement of G;
coherence
for b1 being LGraphComplement of G holds b1 is loopfull by Th73;
end;

registration
let G be non loopless _Graph;
cluster -> non loopfull for LGraphComplement of G;
coherence
for b1 being LGraphComplement of G holds not b1 is loopfull by Th73;
end;

theorem Th74: :: GLIB_012:74
for G1 being _Graph
for G2 being LGraphComplement of G1 st the_Edges_of G1 = G1 .loops() holds
G2 is complete
proof end;

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

theorem Th75: :: GLIB_012:75
for G1 being complete _Graph
for G2 being LGraphComplement of G1 holds the_Edges_of G2 = G2 .loops()
proof end;

registration
let G be complete loopfull _Graph;
cluster -> edgeless for LGraphComplement of G;
coherence
for b1 being LGraphComplement of G holds b1 is edgeless
proof end;
end;

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

theorem :: GLIB_012:76
for G1 being _Graph
for G2 being LGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies not v2 is isolated ) & ( v1 is endvertex implies not v2 is endvertex ) )
proof end;

theorem Th77: :: GLIB_012:77
for G1 being _Graph
for G2 being LGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v2 .allNeighbors() = (the_Vertices_of G2) \ (v1 .allNeighbors())
proof end;

theorem :: GLIB_012:78
for G1 being _Graph
for G2 being LGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
v2 .allNeighbors() = the_Vertices_of G2
proof end;

definition
let G be _Graph;
mode DGraphComplement of G -> Dsimple _Graph means :Def8: :: GLIB_012:def 8
 ex G9 being DLGraphComplement of G st it is removeLoops of G9;
existence
ex b1 being Dsimple _Graph ex G9 being DLGraphComplement of G st b1 is removeLoops of G9
proof end;
end;

:: deftheorem Def8 defines DGraphComplement GLIB_012:def 8 :
for G being _Graph
for b2 being Dsimple _Graph holds
( b2 is DGraphComplement of G iff ex G9 being DLGraphComplement of G st b2 is removeLoops of G9 );

theorem Th79: :: GLIB_012:79
for G1, G2, G3 being _Graph
for G4 being DGraphComplement of G1 st G1 == G2 & G3 == G4 holds
G3 is DGraphComplement of G2
proof end;

registration
let G be _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless non-Dmulti Dsimple plain for DGraphComplement of G;
existence
ex b1 being DGraphComplement of G st b1 is plain
proof end;
end;

theorem Th80: :: GLIB_012:80
for G1 being _Graph
for G2 being Dsimple _Graph holds
( G2 is DGraphComplement of G1 iff ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( 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 ) ) ) )
proof end;

theorem Th81: :: GLIB_012:81
for G1 being _Graph
for G2 being DGraphComplement of G1
for e1, e2, v, w being object st e1 DJoins v,w,G1 holds
not e2 DJoins v,w,G2
proof end;

theorem Th82: :: GLIB_012:82
for G1 being _Graph
for G2 being DSimpleGraph of G1
for G3 being DGraphComplement of G1 holds G3 is DGraphComplement of G2
proof end;

theorem Th83: :: GLIB_012:83
for G1, G2 being _Graph
for G3 being DSimpleGraph of G1
for G4 being DSimpleGraph of G2
for G5 being DGraphComplement of G1
for G6 being DGraphComplement of G2 st G4 is G3 -Disomorphic holds
G6 is G5 -Disomorphic
proof end;

theorem Th84: :: GLIB_012:84
for G1 being _Graph
for G2 being b1 -Disomorphic _Graph
for G3 being DGraphComplement of G1
for G4 being DGraphComplement of G2 holds G4 is G3 -Disomorphic
proof end;

theorem Th85: :: GLIB_012:85
for G1 being _Graph
for G2, G3 being DGraphComplement of G1 holds G3 is G2 -Disomorphic
proof end;

theorem :: GLIB_012:86
for G1 being _Graph
for G2 being reverseEdgeDirections of G1
for G3 being DGraphComplement of G1
for G4 being reverseEdgeDirections of G3 holds G4 is DGraphComplement of G2
proof end;

theorem Th87: :: GLIB_012:87
for G1 being _Graph
for V being non empty Subset of (the_Vertices_of G1)
for G2 being inducedSubgraph of G1,V
for G3 being DGraphComplement of G1
for G4 being inducedSubgraph of G3,V holds G4 is DGraphComplement of G2
proof end;

theorem :: GLIB_012:88
for G1 being _Graph
for V being proper Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V
for G3 being DGraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is DGraphComplement of G2
proof end;

:: involutiveness of graph complement (DC case)
theorem :: GLIB_012:89
for G1 being Dsimple _Graph
for G2 being DGraphComplement of G1 holds G1 is DGraphComplement of G2
proof end;

theorem Th90: :: GLIB_012:90
for G1 being _Graph
for G2 being DGraphComplement of G1 holds G1 .order() = G2 .order() by Th80;

theorem Th91: :: GLIB_012:91
for G1 being _Graph
for G2 being DGraphComplement of G1 holds
( G1 is _trivial iff G2 is _trivial )
proof end;

registration
let G be _trivial _Graph;
cluster -> _trivial for DGraphComplement of G;
coherence
for b1 being DGraphComplement of G holds b1 is _trivial by Th91;
end;

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

theorem Th92: :: GLIB_012:92
for G1 being _Graph
for G2 being DGraphComplement of G1 st the_Edges_of G1 = G1 .loops() holds
G2 is complete
proof end;

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

registration
let G be _trivial edgeless _Graph;
cluster -> edgeless for DGraphComplement of G;
coherence
for b1 being DGraphComplement of G holds b1 is edgeless ;
end;

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

theorem :: GLIB_012:93
for G1 being non _trivial _Graph
for G2 being DGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
not v2 is isolated
proof end;

theorem :: GLIB_012:94
for G1 being _Graph
for G2 being DGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & 3 c= G1 .order() & v1 is endvertex holds
not v2 is endvertex
proof end;

theorem Th95: :: GLIB_012:95
for G1 being _Graph
for G2 being DGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = (the_Vertices_of G2) \ ((v1 .inNeighbors()) \/ {v2}) & v2 .outNeighbors() = (the_Vertices_of G2) \ ((v1 .outNeighbors()) \/ {v2}) )
proof end;

theorem :: GLIB_012:96
for G1 being _Graph
for G2 being DGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
( v2 .inNeighbors() = (the_Vertices_of G2) \ {v2} & v2 .outNeighbors() = (the_Vertices_of G2) \ {v2} & v2 .allNeighbors() = (the_Vertices_of G2) \ {v2} )
proof end;

definition
let G be _Graph;
mode GraphComplement of G -> simple _Graph means :Def9: :: GLIB_012:def 9
 ex G9 being LGraphComplement of G st it is removeLoops of G9;
existence
ex b1 being simple _Graph ex G9 being LGraphComplement of G st b1 is removeLoops of G9
proof end;
end;

:: deftheorem Def9 defines GraphComplement GLIB_012:def 9 :
for G being _Graph
for b2 being simple _Graph holds
( b2 is GraphComplement of G iff ex G9 being LGraphComplement of G st b2 is removeLoops of G9 );

theorem Th97: :: GLIB_012:97
for G1, G2, G3 being _Graph
for G4 being GraphComplement of G1 st G1 == G2 & G3 == G4 holds
G3 is GraphComplement of G2
proof end;

registration
let G be _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple plain for GraphComplement of G;
existence
ex b1 being GraphComplement of G st b1 is plain
proof end;
end;

theorem Th98: :: GLIB_012:98
for G1 being _Graph
for G2 being simple _Graph holds
( G2 is GraphComplement of G1 iff ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( for v, w being Vertex of G1 st v <> w holds
( ex e1 being object st e1 Joins v,w,G1 iff for e2 being object holds not e2 Joins v,w,G2 ) ) ) )
proof end;

theorem Th99: :: GLIB_012:99
for G1 being _Graph
for G2 being simple _Graph holds
( G2 is GraphComplement of G1 iff ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & ( for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff not v2,w2 are_adjacent ) ) ) )
proof end;

theorem Th100: :: GLIB_012:100
for G1 being _Graph
for G2 being GraphComplement of G1
for e1, e2, v, w being object st e1 Joins v,w,G1 holds
not e2 Joins v,w,G2
proof end;

theorem Th101: :: GLIB_012:101
for G1 being _Graph
for G2 being SimpleGraph of G1
for G3 being GraphComplement of G1 holds G3 is GraphComplement of G2
proof end;

theorem Th102: :: GLIB_012:102
for G1, G2 being _Graph
for G3 being SimpleGraph of G1
for G4 being SimpleGraph of G2
for G5 being GraphComplement of G1
for G6 being GraphComplement of G2 st G4 is G3 -isomorphic holds
G6 is G5 -isomorphic
proof end;

theorem Th103: :: GLIB_012:103
for G1 being _Graph
for G2 being b1 -isomorphic _Graph
for G3 being GraphComplement of G1
for G4 being GraphComplement of G2 holds G4 is G3 -isomorphic
proof end;

theorem Th104: :: GLIB_012:104
for G1 being _Graph
for G2, G3 being GraphComplement of G1 holds G3 is G2 -isomorphic
proof end;

theorem Th105: :: GLIB_012:105
for G1 being _Graph
for v being object
for V being Subset of (the_Vertices_of G1)
for G2 being addAdjVertexAll of G1,v,V
for G3 being GraphComplement of G1 st not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3 holds
ex G4 being addAdjVertexAll of G3,v,(the_Vertices_of G1) \ V st G4 is GraphComplement of G2
proof end;

theorem :: GLIB_012:106
for G1 being _Graph
for v being object
for G2 being addVertex of G1,v
for G3 being GraphComplement of G1 st not v in the_Vertices_of G1 holds
ex G4 being addAdjVertexAll of G3,v st G4 is GraphComplement of G2
proof end;

theorem :: GLIB_012:107
for G1 being _Graph
for v being object
for G2 being addAdjVertexAll of G1,v
for G3 being GraphComplement of G1
for G4 being addVertex of G3,v st not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3 holds
G4 is GraphComplement of G2
proof end;

theorem Th108: :: GLIB_012:108
for G1 being _Graph
for V being non empty Subset of (the_Vertices_of G1)
for G2 being inducedSubgraph of G1,V
for G3 being GraphComplement of G1
for G4 being inducedSubgraph of G3,V holds G4 is GraphComplement of G2
proof end;

theorem :: GLIB_012:109
for G1 being _Graph
for V being proper Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V
for G3 being GraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is GraphComplement of G2
proof end;

:: involutiveness of graph complement (C case)
theorem Th110: :: GLIB_012:110
for G1 being simple _Graph
for G2 being GraphComplement of G1 holds G1 is GraphComplement of G2
proof end;

theorem Th111: :: GLIB_012:111
for G1 being _Graph
for G2 being GraphComplement of G1 holds G1 .order() = G2 .order() by Th98;

theorem Th112: :: GLIB_012:112
for G1 being _Graph
for G2 being GraphComplement of G1 holds
( G1 is _trivial iff G2 is _trivial )
proof end;

registration
let G be _trivial _Graph;
cluster -> _trivial for GraphComplement of G;
coherence
for b1 being GraphComplement of G holds b1 is _trivial by Th112;
end;

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

theorem Th113: :: GLIB_012:113
for G1 being _Graph
for G2 being GraphComplement of G1 holds
( ( G1 is complete implies G2 is edgeless ) & ( G2 is edgeless implies G1 is complete ) & ( the_Edges_of G1 = G1 .loops() implies G2 is complete ) & ( G2 is complete implies the_Edges_of G1 = G1 .loops() ) )
proof end;

registration
let G be complete _Graph;
cluster -> edgeless for GraphComplement of G;
coherence
for b1 being GraphComplement of G holds b1 is edgeless by Th113;
end;

registration
let G be non complete _Graph;
cluster -> non edgeless for GraphComplement of G;
coherence
for b1 being GraphComplement of G holds not b1 is edgeless by Th113;
end;

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

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

theorem :: GLIB_012:114
for G1 being non _trivial _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
not v2 is isolated
proof end;

theorem Th115: :: GLIB_012:115
for G1 being _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & G1 .order() = 2 holds
( ( v1 is endvertex implies v2 is isolated ) & ( v1 is isolated implies v2 is endvertex ) )
proof end;

theorem :: GLIB_012:116
for G1 being simple _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & G1 .order() = 2 holds
( ( v1 is endvertex implies v2 is isolated ) & ( v2 is isolated implies v1 is endvertex ) & ( v1 is isolated implies v2 is endvertex ) & ( v2 is endvertex implies v1 is isolated ) )
proof end;

:: in case G.order() = 3 we have the endvertices of P3 with complement K2+K1
theorem :: GLIB_012:117
for G1 being _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & 4 c= G1 .order() & v1 is endvertex holds
not v2 is endvertex
proof end;

theorem Th118: :: GLIB_012:118
for G1 being _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v2 .allNeighbors() = (the_Vertices_of G2) \ ((v1 .allNeighbors()) \/ {v2})
proof end;

theorem :: GLIB_012:119
for G1 being _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
v2 .allNeighbors() = (the_Vertices_of G2) \ {v2}
proof end;

definition
let G be _Graph;
attr G is self-DLcomplementary means :: GLIB_012:def 10
 for H being DLGraphComplement of G holds H is G -Disomorphic ;
attr G is self-Lcomplementary means :: GLIB_012:def 11
 for H being LGraphComplement of G holds H is G -isomorphic ;
attr G is self-Dcomplementary means :: GLIB_012:def 12
 for H being DGraphComplement of G holds H is G -Disomorphic ;
attr G is self-complementary means :: GLIB_012:def 13
 for H being GraphComplement of G holds H is G -isomorphic ;
end;

:: deftheorem defines self-DLcomplementary GLIB_012:def 10 :
for G being _Graph holds
( G is self-DLcomplementary iff for H being DLGraphComplement of G holds H is G -Disomorphic );

:: deftheorem defines self-Lcomplementary GLIB_012:def 11 :
for G being _Graph holds
( G is self-Lcomplementary iff for H being LGraphComplement of G holds H is G -isomorphic );

:: deftheorem defines self-Dcomplementary GLIB_012:def 12 :
for G being _Graph holds
( G is self-Dcomplementary iff for H being DGraphComplement of G holds H is G -Disomorphic );

:: deftheorem defines self-complementary GLIB_012:def 13 :
for G being _Graph holds
( G is self-complementary iff for H being GraphComplement of G holds H is G -isomorphic );

theorem :: GLIB_012:120
for G being _Graph holds
( G is self-DLcomplementary iff ex H being DLGraphComplement of G st H is G -Disomorphic )
proof end;

theorem :: GLIB_012:121
for G being _Graph holds
( G is self-Lcomplementary iff ex H being LGraphComplement of G st H is G -isomorphic )
proof end;

theorem :: GLIB_012:122
for G being _Graph holds
( G is self-Dcomplementary iff ex H being DGraphComplement of G st H is G -Disomorphic )
proof end;

theorem :: GLIB_012:123
for G being _Graph holds
( G is self-complementary iff ex H being GraphComplement of G st H is G -isomorphic )
proof end;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] self-DLcomplementary -> non loopless non-Dmulti connected non loopfull for set ;
coherence
for b1 being _Graph st b1 is self-DLcomplementary holds
( not b1 is loopless & not b1 is loopfull & b1 is non-Dmulti & b1 is connected )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] self-Lcomplementary -> non loopless non-multi connected non loopfull for set ;
coherence
for b1 being _Graph st b1 is self-Lcomplementary holds
( not b1 is loopless & not b1 is loopfull & b1 is non-multi & b1 is connected )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] self-Dcomplementary -> Dsimple connected for set ;
coherence
for b1 being _Graph st b1 is self-Dcomplementary holds
( b1 is Dsimple & b1 is connected )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] self-complementary -> simple connected for set ;
coherence
for b1 being _Graph st b1 is self-complementary holds
( b1 is simple & b1 is connected )
proof end;
end;

:: K2 with an added loop is self-DLcomplementary and
:: P4 with loops at the endvertices or the other two vertices
:: is self-Lcomplementary, but both won't be clustered here
:: hence no existence cluster for the attributes here
registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] _trivial edgeless -> self-Dcomplementary self-complementary for set ;
coherence
for b1 being _Graph st b1 is _trivial & b1 is edgeless holds
( b1 is self-Dcomplementary & b1 is self-complementary ) by GLIB_010:178;
cluster Relation-like NAT -defined Function-like finite [Graph-like] self-Dcomplementary self-complementary -> _trivial edgeless for set ;
coherence
for b1 being _Graph st b1 is self-Dcomplementary & b1 is self-complementary holds
( b1 is _trivial & b1 is edgeless )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] self-DLcomplementary -> non _trivial non self-Lcomplementary non self-Dcomplementary non self-complementary for set ;
coherence
for b1 being _Graph st b1 is self-DLcomplementary holds
( not b1 is _trivial & not b1 is self-Lcomplementary & not b1 is self-Dcomplementary & not b1 is self-complementary )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] self-Lcomplementary -> non _trivial non self-DLcomplementary non self-Dcomplementary non self-complementary for set ;
coherence
for b1 being _Graph st b1 is self-Lcomplementary holds
( not b1 is _trivial & not b1 is self-DLcomplementary & not b1 is self-Dcomplementary & not b1 is self-complementary ) ;
end;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] self-Dcomplementary self-complementary for set ;
existence
ex b1 being _Graph st
( b1 is self-Dcomplementary & b1 is self-complementary )
proof end;
end;