:: by Sebastian Koch
::
:: 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
coherence
for b1 being _Graph st b1 is loopfull holds
not b1 is loopless
proof end;
coherence
for b1 being _Graph st b1 is _trivial & not b1 is loopless holds
b1 is loopfull
proof end;
existence
ex b1 being _Graph st
( b1 is loopfull & b1 is complete )
proof end;
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 ;

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,() \ V,G .edgesBetween (() \ V);
coherence
for b1 being removeVertices of G,V holds b1 is loopfull
;
cluster -> loopfull for inducedSubgraph of G,() \ {V},G .edgesBetween (() \ {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,() \ 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,() \ {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 \ () <> {} 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 ;
coherence
proof end;
end;

theorem Th14: :: GLIB_012:14
for G2 being _Graph
for v being object
for V being Subset of ()
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 ;
coherence
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;
coherence
<*G*> is loopfull
proof end;
coherence 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
coherence
for b1 being Graph-yielding Function st b1 is empty holds
b1 is loopfull
;
coherence
for b1 being Graph-yielding Function st not b1 is empty & b1 is loopfull holds
not b1 is loopless
proof end;
end;

registration
existence
ex b1 being GraphSeq st b1 is loopfull
proof end;
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 = () \/ E & dom f = E & rng f = V & the_Source_of it = () +* f & the_Target_of it = () +* 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 = () \/ E & dom f = E & rng f = V & the_Source_of b1 = () +* f & the_Target_of b1 = () +* 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 = () \/ E & dom f = E & rng f = V & the_Source_of b3 = () +* f & the_Target_of b3 = () +* f ) ) ) ) & ( not V c= the_Vertices_of G implies ( b3 is addLoops of G,V iff b3 == G ) ) );

definition
let G be _Graph;
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 ()
for G1 being addLoops of G2,V
for v being Vertex of G1 st v in V holds
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 ()
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 ()
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 ()
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 ()
for G1 being addLoops of G2,V holds
( the_Edges_of G2 misses G1 .loops() & the_Edges_of G1 = () \/ (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 ()
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
proof end;

theorem :: GLIB_012:35
for G3 being _Graph
for V1 being Subset of ()
for V2 being non empty Subset of ()
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 ();
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 ()
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() = () \/ {e} & v1 .edgesOut() = () \/ {e} & v1 .edgesInOut() = () \/ {e} )
proof end;

theorem :: GLIB_012:43
for G2 being _Graph
for V being Subset of ()
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() = () + 1 & v1 .outDegree() = () + 1 & v1 .degree() = () + 2 )
proof end;

theorem :: GLIB_012:44
for G2 being _Graph
for V being Subset of ()
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;
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 ()
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 ()
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() = () \ () & v2 .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;
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
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 ()
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 ()
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() = () \ ()
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;
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 ()
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 ()
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() = () \ (() \/ {v2}) & v2 .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() = () \ {v2} & v2 .outNeighbors() = () \ {v2} & v2 .allNeighbors() = () \ {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;
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
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 ()
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,() \ 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 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 ()
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 ()
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() = () \ (() \/ {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() = () \ {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
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;
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;
coherence
for b1 being _Graph st b1 is self-Dcomplementary holds
( b1 is Dsimple & b1 is connected )
proof end;
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
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;
coherence
for b1 being _Graph st b1 is self-Dcomplementary & b1 is self-complementary holds
( b1 is _trivial & b1 is edgeless )
proof end;
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;
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
existence
ex b1 being _Graph st
( b1 is self-Dcomplementary & b1 is self-complementary )
proof end;
end;