:: Simple Graphs as Simplicial Complexes: the {M}ycielskian of a Graph
:: by Piotr Rudnicki and Lorna Stewart
::
:: Received February 8, 2012
:: Copyright (c) 2012 Association of Mizar Users


begin

:: Could not find in MML
theorem Aux1: :: SCMYCIEL:1
for x, X being set holds not [x,X] in X
proofend;

theorem Aux2: :: SCMYCIEL:2
for x, X being set holds [x,X] <> X
proofend;

theorem Aux3: :: SCMYCIEL:3
for x, X being set holds [x,X] <> x
proofend;

theorem Aux4: :: SCMYCIEL:4
for x1, y1, x2, y2, X being set st x1 in X &amp; x2 in X &amp; {x1,[y1,X]} = {x2,[y2,X]} holds
( x1 = x2 &amp; y1 = y2 )
proofend;

theorem card3: :: SCMYCIEL:5
for X, v being set st 3 c= card X holds
ex v1, v2 being set st
( v1 in X &amp; v2 in X &amp; v1 <> v &amp; v2 <> v &amp; v1 <> v2 )
proofend;

theorem Singletons0: :: SCMYCIEL:6
for x being set holds singletons {x} = {{x}}
proofend;

registration
cluster Relation-like NAT -defined Function-like finite V37() FinSequence-like FinSubsequence-like for set ;
existence
 not for b1 being FinSequence holds b1 is V37()
proofend;
end;

theorem Part0: :: SCMYCIEL:7
for X being non empty finite set
for P being a_partition of X st card P < card X holds
ex p, x, y being set st
( p in P &amp; x in p &amp; y in p &amp; x <> y )
proofend;

registration
cluster Vertices {{}} ->  empty ;
correctness
coherence
union {{}} is empty ;
by ZFMISC_1:25;
end;

theorem SingleVertices: :: SCMYCIEL:8
for x being set holds union {{},{x}} = {x}
proofend;

theorem BSPACEdef9: :: SCMYCIEL:9
for X being set
for s being Subset of X st s is 1 -element holds
ex x being set st
( x in X &amp; s = {x} )
proofend;

theorem McopyV: :: SCMYCIEL:10
for X being set holds card  {  {X,[x,X]} where x is Element of X : x in X  }  = card X
proofend;

definition
let G be set ;
func PairsOf G ->  Subset of G means :LEdges: :: SCMYCIEL:def 1
 for e being set holds
( e in it iff ( e in G &amp; card e = 2 ) );
existence
 ex b1 being Subset of G st
for e being set holds
( e in b1 iff ( e in G &amp; card e = 2 ) )
proofend;
uniqueness
 for b1, b2 being Subset of G st ( for e being set holds
( e in b1 iff ( e in G &amp; card e = 2 ) ) ) &amp; ( for e being set holds
( e in b2 iff ( e in G &amp; card e = 2 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem LEdges defines PairsOf SCMYCIEL:def_1_:_
 for G being set
for b2 being Subset of G holds
( b2 = PairsOf G iff for e being set holds
( e in b2 iff ( e in G &amp; card e = 2 ) ) );

theorem SG4: :: SCMYCIEL:11
for X, e being set st e in PairsOf X holds
ex x, y being set st
( x <> y &amp; x in union X &amp; y in union X &amp; e = {x,y} )
proofend;

theorem SG4a: :: SCMYCIEL:12
for X, x, y being set st x <> y &amp; {x,y} in X holds
{x,y} in PairsOf X
proofend;

theorem SG5: :: SCMYCIEL:13
for X, x, y being set st {x,y} in PairsOf X holds
( x <> y &amp; x in union X &amp; y in union X )
proofend;

theorem SG6e: :: SCMYCIEL:14
for G, H being set st G c= H holds
PairsOf G c= PairsOf H
proofend;

theorem MnewE: :: SCMYCIEL:15
for X being finite set holds card  {  {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X  }  = 2 * (card (PairsOf X))
proofend;

theorem :: SCMYCIEL:16
for X being finite set holds card  {  [x,y] where x, y is Element of union X : {x,y} in PairsOf X  }  = 2 * (card (PairsOf X))
proofend;

registration
let X be finite set ;
cluster PairsOf X ->  finite ;
coherence
 PairsOf X is finite ;
end;

definition
let X be set ;
attrX is void  means :Lvoid: :: SCMYCIEL:def 2
X = {{}};
end;

:: deftheorem Lvoid defines void SCMYCIEL:def_2_:_
 for X being set holds
( X is void iff X = {{}} );

registration
cluster void for set ;
existence
 ex b1 being set st b1 is void by Lvoid;
end;

registration
cluster void  ->  finite for set ;
coherence
 for b1 being set st b1 is void holds
b1 is finite by Lvoid;
end;

registration
let G be void set ;
cluster Vertices G ->  empty ;
coherence
 union G is empty
proofend;
end;

theorem VoidGE: :: SCMYCIEL:17
for X being set st X is void holds
PairsOf X = {}
proofend;

theorem uVoid1: :: SCMYCIEL:18
for X being set holds
( not union X = {} or X = {} or X = {{}} )
proofend;

definition
let X be set ;
attrX is pairfree  means :Ledgeless: :: SCMYCIEL:def 3
 PairsOf X is empty ;
end;

:: deftheorem Ledgeless defines pairfree SCMYCIEL:def_3_:_
 for X being set holds
( X is pairfree iff PairsOf X is empty );

theorem GsingleE: :: SCMYCIEL:19
for X, x being set st card (union X) = 1 holds
X is pairfree
proofend;

CSGLem1:  for X being set holds union  {  V where V is finite Subset of X : card V <= 2  }  = X
proofend;

registration
cluster non empty finite-membered for set ;
existence
 ex b1 being set st
( b1 is finite-membered &amp; not b1 is empty )
proofend;
end;

registration
let X be finite-membered set ;
let Y be set ;
clusterX /\ Y ->  finite-membered ;
coherence
 X /\ Y is finite-membered
proofend;
clusterX \ Y ->  finite-membered ;
coherence
 X \ Y is finite-membered ;
end;

begin

definition
let n be Nat;
let X be set ;
attrX is n -at_most_dimensional  means :Lnatmost: :: SCMYCIEL:def 4
 for x being set st x in X holds
card x c= n + 1;
end;

:: deftheorem Lnatmost defines -at_most_dimensional SCMYCIEL:def_4_:_
 for n being Nat
for X being set holds
( X is n -at_most_dimensional iff for x being set st x in X holds
card x c= n + 1 );

registration
let n be Nat;
clustern -at_most_dimensional  ->  finite-membered for set ;
correctness
coherence
for b1 being set st b1 is n -at_most_dimensional holds
b1 is finite-membered ;
proofend;
end;

Void0:  for n being Nat holds {{}} is n -at_most_dimensional
proofend;

registration
let n be Nat;
cluster non empty subset-closed n -at_most_dimensional for set ;
existence
 ex b1 being set st
( b1 is n -at_most_dimensional &amp; b1 is subset-closed &amp; not b1 is empty )
proofend;
end;

theorem SG1: :: SCMYCIEL:20
for G being non empty subset-closed set holds {} in G
proofend;

theorem Lnatmost1: :: SCMYCIEL:21
for n being natural number
for X being b1 -at_most_dimensional set
for x being Element of X st x in X holds
card x <= n + 1 by Lnatmost, NAT_1:39;

registration
let n be Nat;
let X, Y be n -at_most_dimensional set ;
clusterX \/ Y -> n -at_most_dimensional ;
coherence
 X \/ Y is n -at_most_dimensional
proofend;
end;

registration
let n be Nat;
let X be n -at_most_dimensional set ;
let Y be set ;
clusterX /\ Y -> n -at_most_dimensional ;
coherence
 X /\ Y is n -at_most_dimensional
proofend;
clusterX \ Y -> n -at_most_dimensional ;
coherence
 X \ Y is n -at_most_dimensional
proofend;
end;

registration
let n be Nat;
let X be n -at_most_dimensional set ;
cluster  -> n -at_most_dimensional for Element of bool X;
correctness
coherence
for b1 being Subset of X holds b1 is n -at_most_dimensional ;
proofend;
end;

definition
let s be set ;
attrs is SimpleGraph-like  means :LSGlike: :: SCMYCIEL:def 5
( s is 1 -at_most_dimensional &amp; s is subset-closed &amp; not s is empty );
end;

:: deftheorem LSGlike defines SimpleGraph-like SCMYCIEL:def_5_:_
 for s being set holds
( s is SimpleGraph-like iff ( s is 1 -at_most_dimensional &amp; s is subset-closed &amp; not s is empty ) );

registration
cluster SimpleGraph-like  ->  non empty subset-closed 1 -at_most_dimensional for set ;
correctness
coherence
for b1 being set st b1 is SimpleGraph-like holds
( b1 is 1 -at_most_dimensional &amp; b1 is subset-closed &amp; not b1 is empty );
by LSGlike;
cluster non empty subset-closed 1 -at_most_dimensional  ->  SimpleGraph-like for set ;
correctness
coherence
for b1 being set st b1 is 1 -at_most_dimensional &amp; b1 is subset-closed &amp; not b1 is empty holds
b1 is SimpleGraph-like ;
by LSGlike;
end;

theorem eSG1: :: SCMYCIEL:22
{{}} is SimpleGraph-like
proofend;

registration
cluster{{}} ->  SimpleGraph-like ;
correctness
coherence
{{}} is SimpleGraph-like ;
by eSG1;
end;

registration
cluster SimpleGraph-like for set ;
existence
 ex b1 being set st b1 is SimpleGraph-like by eSG1;
end;

definition
mode SimpleGraph is SimpleGraph-like set ;
end;

registration
cluster non empty finite-membered V233() V267() subset-closed void 1 -at_most_dimensional SimpleGraph-like for set ;
existence
 ex b1 being SimpleGraph st b1 is void
proofend;
cluster non empty finite finite-membered V233() V267() subset-closed 1 -at_most_dimensional SimpleGraph-like for set ;
existence
 ex b1 being SimpleGraph st b1 is finite by eSG1;
end;

notation
let G be set ;
synonym  Vertices G for  union G;
synonym  Edges G for  PairsOf G;
end;

notation
let X be set ;
synonym  edgeless X for  pairfree ;
end;

theorem FinSG: :: SCMYCIEL:23
for G being SimpleGraph st Vertices G is finite holds
G is finite
proofend;

theorem Vertices0: :: SCMYCIEL:24
for G being SimpleGraph
for x being set holds
( x in Vertices G iff {x} in G )
proofend;

theorem SingleVertex: :: SCMYCIEL:25
for x being set holds {{},{x}} is SimpleGraph
proofend;

definition
let X be finite finite-membered set ;
func order X ->  Nat equals :: SCMYCIEL:def 6
 card (union X);
coherence
 card (union X) is Nat ;
end;

:: deftheorem  defines order SCMYCIEL:def_6_:_
 for X being finite finite-membered set holds order X = card (union X);

definition
let X be finite set ;
func size X ->  Nat equals :: SCMYCIEL:def 7
 card (PairsOf X);
coherence
 card (PairsOf X) is Nat ;
end;

:: deftheorem  defines size SCMYCIEL:def_7_:_
 for X being finite set holds size X = card (PairsOf X);

theorem Lorder1: :: SCMYCIEL:26
for G being finite SimpleGraph holds order G <= card G
proofend;

definition
let G be SimpleGraph;
mode Vertex of G is Element of Vertices G;
mode Edge of G is Element of Edges G;
end;

theorem SG0: :: SCMYCIEL:27
for G being SimpleGraph holds G = ({{}} \/ (singletons (Vertices G))) \/ (Edges G)
proofend;

theorem VoidGV: :: SCMYCIEL:28
for G being SimpleGraph st Vertices G = {} holds
G is void by uVoid1, Lvoid;

theorem SG2: :: SCMYCIEL:29
for G being SimpleGraph
for x being set st x in G &amp; x <> {} &amp; ( for y being set holds
( not x = {y} or not y in Vertices G ) ) holds
x in Edges G
proofend;

theorem :: SCMYCIEL:30
for G being SimpleGraph
for x being set st Vertices G = {x} holds
G = {{},{x}}
proofend;

theorem size0SG: :: SCMYCIEL:31
for X being set ex G being SimpleGraph st
( G is edgeless &amp; Vertices G = X )
proofend;

definition
let G be SimpleGraph;
let v be Element of Vertices G;
func Adjacent v ->  Subset of (Vertices G) means :Ladj: :: SCMYCIEL:def 8
 for x being Element of Vertices G holds
( x in it iff {v,x} in Edges G );
existence
 ex b1 being Subset of (Vertices G) st
for x being Element of Vertices G holds
( x in b1 iff {v,x} in Edges G )
proofend;
uniqueness
 for b1, b2 being Subset of (Vertices G) st ( for x being Element of Vertices G holds
( x in b1 iff {v,x} in Edges G ) ) &amp; ( for x being Element of Vertices G holds
( x in b2 iff {v,x} in Edges G ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Ladj defines Adjacent SCMYCIEL:def_8_:_
 for G being SimpleGraph
for v being Element of Vertices G
for b3 being Subset of (Vertices G) holds
( b3 = Adjacent v iff for x being Element of Vertices G holds
( x in b3 iff {v,x} in Edges G ) );

definition
let X be set ;
mode SimpleGraph of X ->  SimpleGraph means :LSGofX: :: SCMYCIEL:def 9
 Vertices it = X;
existence
 ex b1 being SimpleGraph st Vertices b1 = X
proofend;
end;

:: deftheorem LSGofX defines SimpleGraph SCMYCIEL:def_9_:_
 for X being set
for b2 being SimpleGraph holds
( b2 is SimpleGraph of X iff Vertices b2 = X );

definition
let X be set ;
func CompleteSGraph X ->  SimpleGraph of X equals :: SCMYCIEL:def 10
 {  V where V is finite Subset of X : card V <= 2  }  ;
coherence
  {  V where V is finite Subset of X : card V <= 2  }  is SimpleGraph of X
proofend;
end;

:: deftheorem  defines CompleteSGraph SCMYCIEL:def_10_:_
 for X being set holds CompleteSGraph X =  {  V where V is finite Subset of X : card V <= 2  }  ;

theorem CSGdef: :: SCMYCIEL:32
for G being SimpleGraph st ( for x, y being set st x in Vertices G &amp; y in Vertices G holds
{x,y} in G ) holds
G = CompleteSGraph (Vertices G)
proofend;

registration
let X be finite set ;
cluster CompleteSGraph X ->  finite ;
correctness
coherence
CompleteSGraph X is finite ;
proofend;
end;

theorem CSG1a: :: SCMYCIEL:33
for X, x being set st x in X holds
{x} in CompleteSGraph X
proofend;

theorem CSG1: :: SCMYCIEL:34
for X, x, y being set st x in X &amp; y in X holds
{x,y} in CompleteSGraph X
proofend;

theorem eCSG0: :: SCMYCIEL:35
CompleteSGraph {} = {{}}
proofend;

theorem P1: :: SCMYCIEL:36
for x being set holds CompleteSGraph {x} = {{},{x}}
proofend;

theorem P2: :: SCMYCIEL:37
for x, y being set holds CompleteSGraph {x,y} = {{},{x},{y},{x,y}}
proofend;

theorem :: SCMYCIEL:38
for X, Y being set st X c= Y holds
CompleteSGraph X c= CompleteSGraph Y
proofend;

theorem CSGsingle: :: SCMYCIEL:39
for G being SimpleGraph
for x being set st x in Vertices G holds
CompleteSGraph {x} c= G
proofend;

registration
let G be SimpleGraph;
cluster finite-membered 1 -at_most_dimensional SimpleGraph-like for Element of bool G;
existence
 ex b1 being Subset of G st b1 is SimpleGraph-like
proofend;
end;

definition
let G be SimpleGraph;
mode Subgraph of G is SimpleGraph-like Subset of G;
end;

CisSG:  for G being SimpleGraph holds (CompleteSGraph (Vertices G)) \ (Edges G) is SimpleGraph
proofend;

Compl1:  for G being SimpleGraph holds Vertices G = Vertices ((CompleteSGraph (Vertices G)) \ (Edges G))
proofend;

Compl1a:  for G being SimpleGraph
for x, y being set st x <> y &amp; x in Vertices G &amp; y in Vertices G holds
( {x,y} in Edges G iff {x,y} nin Edges ((CompleteSGraph (Vertices G)) \ (Edges G)) )
proofend;

Compl2:  for G, CG being SimpleGraph st CG = (CompleteSGraph (Vertices G)) \ (Edges G) holds
(CompleteSGraph (Vertices CG)) \ (Edges CG) = G
proofend;

definition
let G be SimpleGraph;
func Complement G ->  SimpleGraph equals :: SCMYCIEL:def 11
(CompleteSGraph (Vertices G)) \ (Edges G);
correctness
coherence
(CompleteSGraph (Vertices G)) \ (Edges G) is SimpleGraph;
by CisSG;
involutiveness
 for b1, b2 being SimpleGraph st b1 = (CompleteSGraph (Vertices b2)) \ (Edges b2) holds
b2 = (CompleteSGraph (Vertices b1)) \ (Edges b1) by Compl2;
end;

:: deftheorem  defines Complement SCMYCIEL:def_11_:_
 for G being SimpleGraph holds Complement G = (CompleteSGraph (Vertices G)) \ (Edges G);

theorem :: SCMYCIEL:40
for G being SimpleGraph holds Vertices G = Vertices (Complement G) by Compl1;

theorem :: SCMYCIEL:41
for G being SimpleGraph
for x, y being set st x <> y &amp; x in Vertices G &amp; y in Vertices G holds
( {x,y} in Edges G iff {x,y} nin Edges (Complement G) ) by Compl1a;

begin

definition
let G be SimpleGraph;
let L be set ;
funcG SubgraphInducedBy L ->  Subset of G equals :: SCMYCIEL:def 12
G /\ (bool L);
coherence
 G /\ (bool L) is Subset of G by XBOOLE_1:17;
end;

:: deftheorem  defines SubgraphInducedBy SCMYCIEL:def_12_:_
 for G being SimpleGraph
for L being set holds G SubgraphInducedBy L = G /\ (bool L);

registration
let G be SimpleGraph;
let L be set ;
clusterG SubgraphInducedBy L ->  SimpleGraph-like ;
coherence
 G SubgraphInducedBy L is SimpleGraph-like
proofend;
end;

theorem :: SCMYCIEL:42
for G being SimpleGraph holds G = G SubgraphInducedBy (Vertices G)
proofend;

theorem Sub3a: :: SCMYCIEL:43
for G being SimpleGraph
for L being set holds G SubgraphInducedBy L = G SubgraphInducedBy (L /\ (Vertices G))
proofend;

registration
let G be finite SimpleGraph;
let L be set ;
clusterG SubgraphInducedBy L ->  finite ;
coherence
 G SubgraphInducedBy L is finite ;
end;

registration
let G be SimpleGraph;
let L be finite set ;
clusterG SubgraphInducedBy L ->  finite ;
coherence
 G SubgraphInducedBy L is finite ;
end;

theorem Sub0b: :: SCMYCIEL:44
for G, H being SimpleGraph st G c= H holds
G c= H SubgraphInducedBy (Vertices G)
proofend;

Sub1:  for G being SimpleGraph
for L, x being set st x in Vertices (G SubgraphInducedBy L) holds
x in L
proofend;

Sub3:  for G being SimpleGraph
for L, x being set st x in L &amp; x in Vertices G holds
x in Vertices (G SubgraphInducedBy L)
proofend;

theorem Sub5: :: SCMYCIEL:45
for G being SimpleGraph
for L being set holds Vertices (G SubgraphInducedBy L) = (Vertices G) /\ L
proofend;

Sub0c:  for G being SimpleGraph
for L being set st L c= Vertices G holds
Vertices (G SubgraphInducedBy L) = L
proofend;

Sub6:  for G being SimpleGraph
for L, x, y being set st x in L &amp; y in L &amp; {x,y} in G holds
{x,y} in G SubgraphInducedBy L
proofend;

theorem SingleSub: :: SCMYCIEL:46
for G being SimpleGraph
for x being set st x in Vertices G holds
G SubgraphInducedBy {x} = {{},{x}}
proofend;

begin

definition
let G be SimpleGraph;
attrG is clique  means :Lclique: :: SCMYCIEL:def 13
G = CompleteSGraph (Vertices G);
end;

:: deftheorem Lclique defines clique SCMYCIEL:def_13_:_
 for G being SimpleGraph holds
( G is clique iff G = CompleteSGraph (Vertices G) );

theorem Lclique1: :: SCMYCIEL:47
for G being SimpleGraph st ( for x, y being set st x <> y &amp; x in Vertices G &amp; y in Vertices G holds
{x,y} in Edges G ) holds
G is clique
proofend;

theorem eclique: :: SCMYCIEL:48
{{}} is clique
proofend;

registration
cluster non empty finite-membered V233() V267() subset-closed 1 -at_most_dimensional SimpleGraph-like clique for set ;
existence
 ex b1 being SimpleGraph st b1 is clique by eclique;
let G be SimpleGraph;
cluster non empty finite-membered V233() V267() subset-closed 1 -at_most_dimensional SimpleGraph-like clique for Element of bool G;
existence
 ex b1 being Subgraph of G st b1 is clique
proofend;
end;

definition
let G be SimpleGraph;
mode Clique of G is clique Subgraph of G;
end;

theorem cliqueCSG0: :: SCMYCIEL:49
for X being set holds CompleteSGraph X is clique
proofend;

registration
let X be set ;
cluster CompleteSGraph X ->  clique ;
correctness
coherence
CompleteSGraph X is clique ;
by cliqueCSG0;
end;

theorem SingleClique: :: SCMYCIEL:50
for G being SimpleGraph
for x being set st x in Vertices G holds
{{},{x}} is Clique of G
proofend;

theorem Cliqueon2: :: SCMYCIEL:51
for G being SimpleGraph
for x, y being set st x in Vertices G &amp; y in Vertices G &amp; {x,y} in G holds
{{},{x},{y},{x,y}} is Clique of G
proofend;

registration
let G be SimpleGraph;
cluster non empty finite finite-membered V233() V267() subset-closed 1 -at_most_dimensional SimpleGraph-like clique for Element of bool G;
existence
 ex b1 being Clique of G st b1 is finite
proofend;
end;

theorem CliqueS: :: SCMYCIEL:52
for G being SimpleGraph
for x being set st x in union G holds
ex C being finite Clique of G st Vertices C = {x}
proofend;

theorem Clique2a: :: SCMYCIEL:53
for C being clique SimpleGraph
for u, v being set st u in Vertices C &amp; v in Vertices C holds
{u,v} in C
proofend;

definition
let G be SimpleGraph;
attrG is with_finite_clique#  means :Lwfcno: :: SCMYCIEL:def 14
 ex C being finite Clique of G st
for D being finite Clique of G holds order D <= order C;
end;

:: deftheorem Lwfcno defines with_finite_clique# SCMYCIEL:def_14_:_
 for G being SimpleGraph holds
( G is with_finite_clique# iff ex C being finite Clique of G st
for D being finite Clique of G holds order D <= order C );

registration
cluster non empty finite-membered V233() V267() subset-closed 1 -at_most_dimensional SimpleGraph-like with_finite_clique# for set ;
existence
 ex b1 being SimpleGraph st b1 is with_finite_clique#
proofend;
end;

registration
cluster finite SimpleGraph-like  ->  with_finite_clique# for set ;
coherence
 for b1 being SimpleGraph st b1 is finite holds
b1 is with_finite_clique#
proofend;
end;

definition
let G be with_finite_clique# SimpleGraph;
func clique# G ->  Nat means :Lcliqueno: :: SCMYCIEL:def 15
( ex C being finite Clique of G st order C = it &amp; ( for T being finite Clique of G holds order T <= it ) );
existence
 ex b1 being Nat st
( ex C being finite Clique of G st order C = b1 &amp; ( for T being finite Clique of G holds order T <= b1 ) )
proofend;
uniqueness
 for b1, b2 being Nat st ex C being finite Clique of G st order C = b1 &amp; ( for T being finite Clique of G holds order T <= b1 ) &amp; ex C being finite Clique of G st order C = b2 &amp; ( for T being finite Clique of G holds order T <= b2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Lcliqueno defines clique# SCMYCIEL:def_15_:_
 for G being with_finite_clique# SimpleGraph
for b2 being Nat holds
( b2 = clique# G iff ( ex C being finite Clique of G st order C = b2 &amp; ( for T being finite Clique of G holds order T <= b2 ) ) );

theorem Cno0: :: SCMYCIEL:54
for G being with_finite_clique# SimpleGraph st clique# G = 0 holds
Vertices G = {}
proofend;

theorem :: SCMYCIEL:55
for G being void SimpleGraph holds clique# G = 0
proofend;

theorem Th8: :: SCMYCIEL:56
for G being SimpleGraph
for x, y being set st {x,y} in G holds
G SubgraphInducedBy {x,y} is Clique of G
proofend;

theorem Cno2: :: SCMYCIEL:57
for G being with_finite_clique# SimpleGraph st Edges G <> {} holds
clique# G >= 2
proofend;

theorem CliqueSubno0: :: SCMYCIEL:58
for G, H being with_finite_clique# SimpleGraph st G c= H holds
clique# G <= clique# H
proofend;

theorem cliqueCSG: :: SCMYCIEL:59
for X being finite set holds clique# (CompleteSGraph X) = card X
proofend;

definition
let G be SimpleGraph;
let P be a_partition of Vertices G;
attrP is Clique-wise  means :LCliquewise: :: SCMYCIEL:def 16
 for x being set st x in P holds
G SubgraphInducedBy x is Clique of G;
end;

:: deftheorem LCliquewise defines Clique-wise SCMYCIEL:def_16_:_
 for G being SimpleGraph
for P being a_partition of Vertices G holds
( P is Clique-wise iff for x being set st x in P holds
G SubgraphInducedBy x is Clique of G );

registration
let G be SimpleGraph;
clusterV267() Clique-wise for a_partition of Vertices G;
correctness
existence
ex b1 being a_partition of Vertices G st b1 is Clique-wise ;
proofend;
end;

definition
let G be SimpleGraph;
mode Clique-partition of G is Clique-wise a_partition of Vertices G;
end;

registration
let G be void SimpleGraph;
cluster empty  ->  Clique-wise for a_partition of Vertices G;
correctness
coherence
for b1 being a_partition of Vertices G st b1 is empty holds
b1 is Clique-wise ;
proofend;
end;

definition
let G be SimpleGraph;
attrG is with_finite_cliquecover#  means :Lwfclicov: :: SCMYCIEL:def 17
 ex C being Clique-partition of G st C is finite ;
end;

:: deftheorem Lwfclicov defines with_finite_cliquecover# SCMYCIEL:def_17_:_
 for G being SimpleGraph holds
( G is with_finite_cliquecover# iff ex C being Clique-partition of G st C is finite );

registration
cluster finite SimpleGraph-like  ->  with_finite_cliquecover# for set ;
correctness
coherence
for b1 being SimpleGraph st b1 is finite holds
b1 is with_finite_cliquecover# ;
proofend;
end;

registration
let G be with_finite_cliquecover# SimpleGraph;
cluster finite V267() Clique-wise for a_partition of Vertices G;
correctness
existence
ex b1 being Clique-partition of G st b1 is finite ;
by Lwfclicov;
end;

registration
let G be with_finite_cliquecover# SimpleGraph;
let S be Subset of (Vertices G);
clusterG SubgraphInducedBy S ->  with_finite_cliquecover# ;
correctness
coherence
G SubgraphInducedBy S is with_finite_cliquecover# ;
proofend;
end;

definition
let G be with_finite_cliquecover# SimpleGraph;
func cliquecover# G ->  Nat means :Lclicovno: :: SCMYCIEL:def 18
( ex C being finite Clique-partition of G st card C = it &amp; ( for C being finite Clique-partition of G holds it <= card C ) );
existence
 ex b1 being Nat st
( ex C being finite Clique-partition of G st card C = b1 &amp; ( for C being finite Clique-partition of G holds b1 <= card C ) )
proofend;
uniqueness
 for b1, b2 being Nat st ex C being finite Clique-partition of G st card C = b1 &amp; ( for C being finite Clique-partition of G holds b1 <= card C ) &amp; ex C being finite Clique-partition of G st card C = b2 &amp; ( for C being finite Clique-partition of G holds b2 <= card C ) holds
b1 = b2
proofend;
end;

:: deftheorem Lclicovno defines cliquecover# SCMYCIEL:def_18_:_
 for G being with_finite_cliquecover# SimpleGraph
for b2 being Nat holds
( b2 = cliquecover# G iff ( ex C being finite Clique-partition of G st card C = b2 &amp; ( for C being finite Clique-partition of G holds b2 <= card C ) ) );

begin

definition
let G be SimpleGraph;
let S be Subset of (Vertices G);
attrS is stable  means :Lstable: :: SCMYCIEL:def 19
 for x, y being set st x <> y &amp; x in S &amp; y in S holds
{x,y} nin G;
end;

:: deftheorem Lstable defines stable SCMYCIEL:def_19_:_
 for G being SimpleGraph
for S being Subset of (Vertices G) holds
( S is stable iff for x, y being set st x <> y &amp; x in S &amp; y in S holds
{x,y} nin G );

theorem stable0: :: SCMYCIEL:60
for G being SimpleGraph holds {} (Vertices G) is stable
proofend;

theorem stable1: :: SCMYCIEL:61
for G being SimpleGraph
for S being Subset of (Vertices G)
for v being set st S = {v} holds
S is stable
proofend;

registration
let G be SimpleGraph;
cluster trivial  ->  stable for Element of bool (Vertices G);
coherence
 for b1 being Subset of (Vertices G) st b1 is trivial holds
b1 is stable
proofend;
end;

registration
let G be SimpleGraph;
cluster stable for Element of bool (Vertices G);
existence
 ex b1 being Subset of (Vertices G) st b1 is stable
proofend;
end;

definition
let G be SimpleGraph;
mode StableSet of G is stable Subset of (Vertices G);
end;

theorem Th14: :: SCMYCIEL:62
for G being SimpleGraph
for x, y being set st x in Vertices G &amp; y in Vertices G &amp; {x,y} nin G holds
{x,y} is StableSet of G
proofend;

theorem Th19: :: SCMYCIEL:63
for G being with_finite_clique# SimpleGraph st clique# G = 1 holds
Vertices G is StableSet of G
proofend;

registration
let G be SimpleGraph;
cluster finite stable for Element of bool (Vertices G);
existence
 ex b1 being StableSet of G st b1 is finite
proofend;
end;

theorem Th16: :: SCMYCIEL:64
for G being SimpleGraph
for A being StableSet of G
for B being Subset of A holds B is StableSet of G
proofend;

definition
let G be SimpleGraph;
let P be a_partition of Vertices G;
attrP is StableSet-wise  means :LStableSetwise: :: SCMYCIEL:def 20
 for x being set st x in P holds
x is StableSet of G;
end;

:: deftheorem LStableSetwise defines StableSet-wise SCMYCIEL:def_20_:_
 for G being SimpleGraph
for P being a_partition of Vertices G holds
( P is StableSet-wise iff for x being set st x in P holds
x is StableSet of G );

theorem Coloring1: :: SCMYCIEL:65
for G being SimpleGraph holds SmallestPartition (Vertices G) is StableSet-wise
proofend;

registration
let G be SimpleGraph;
clusterV267() StableSet-wise for a_partition of Vertices G;
existence
 ex b1 being a_partition of Vertices G st b1 is StableSet-wise
proofend;
end;

definition
let G be SimpleGraph;
mode Coloring of G is StableSet-wise a_partition of Vertices G;
end;

definition
let G be SimpleGraph;
attrG is finitely_colorable  means :Lfc: :: SCMYCIEL:def 21
 ex C being Coloring of G st C is finite ;
end;

:: deftheorem Lfc defines finitely_colorable SCMYCIEL:def_21_:_
 for G being SimpleGraph holds
( G is finitely_colorable iff ex C being Coloring of G st C is finite );

registration
cluster non empty finite-membered V233() V267() subset-closed 1 -at_most_dimensional SimpleGraph-like finitely_colorable for set ;
existence
 ex b1 being SimpleGraph st b1 is finitely_colorable
proofend;
end;

registration
cluster finite SimpleGraph-like  ->  finitely_colorable for set ;
correctness
coherence
for b1 being SimpleGraph st b1 is finite holds
b1 is finitely_colorable ;
proofend;
end;

registration
let G be finitely_colorable SimpleGraph;
cluster finite V267() StableSet-wise for a_partition of Vertices G;
existence
 ex b1 being Coloring of G st b1 is finite by Lfc;
end;

theorem SGClique0: :: SCMYCIEL:66
for G being SimpleGraph
for S being Clique of G
for L being set st L c= Vertices S holds
G SubgraphInducedBy L is Clique of G
proofend;

theorem Tsr0: :: SCMYCIEL:67
for G being SimpleGraph
for C being Coloring of G
for S being Subset of (Vertices G) holds C | S is Coloring of (G SubgraphInducedBy S)
proofend;

registration
let G be finitely_colorable SimpleGraph;
let S be set ;
clusterG SubgraphInducedBy S ->  finitely_colorable ;
coherence
 G SubgraphInducedBy S is finitely_colorable
proofend;
end;

definition
let G be finitely_colorable SimpleGraph;
func chromatic# G ->  Nat means :Lchro: :: SCMYCIEL:def 22
( ex C being finite Coloring of G st card C = it &amp; ( for C being finite Coloring of G holds it <= card C ) );
existence
 ex b1 being Nat st
( ex C being finite Coloring of G st card C = b1 &amp; ( for C being finite Coloring of G holds b1 <= card C ) )
proofend;
uniqueness
 for b1, b2 being Nat st ex C being finite Coloring of G st card C = b1 &amp; ( for C being finite Coloring of G holds b1 <= card C ) &amp; ex C being finite Coloring of G st card C = b2 &amp; ( for C being finite Coloring of G holds b2 <= card C ) holds
b1 = b2
proofend;
end;

:: deftheorem Lchro defines chromatic# SCMYCIEL:def_22_:_
 for G being finitely_colorable SimpleGraph
for b2 being Nat holds
( b2 = chromatic# G iff ( ex C being finite Coloring of G st card C = b2 &amp; ( for C being finite Coloring of G holds b2 <= card C ) ) );

theorem Subchro: :: SCMYCIEL:68
for G, H being finitely_colorable SimpleGraph st G c= H holds
chromatic# G <= chromatic# H
proofend;

theorem chromaticCSG: :: SCMYCIEL:69
for X being finite set holds chromatic# (CompleteSGraph X) = card X
proofend;

theorem AdjCol: :: SCMYCIEL:70
for G being finitely_colorable SimpleGraph
for C being finite Coloring of G
for c being set st c in C &amp; card C = chromatic# G holds
ex v being Element of Vertices G st
( v in c &amp; ( for d being Element of C st d <> c holds
ex w being Element of Vertices G st
( w in Adjacent v &amp; w in d ) ) )
proofend;

definition
let G be SimpleGraph;
attrG is with_finite_stability#  means :Lwfstab: :: SCMYCIEL:def 23
 ex A being finite StableSet of G st
for B being finite StableSet of G holds card B <= card A;
end;

:: deftheorem Lwfstab defines with_finite_stability# SCMYCIEL:def_23_:_
 for G being SimpleGraph holds
( G is with_finite_stability# iff ex A being finite StableSet of G st
for B being finite StableSet of G holds card B <= card A );

registration
cluster finite SimpleGraph-like  ->  with_finite_stability# for set ;
correctness
coherence
for b1 being SimpleGraph st b1 is finite holds
b1 is with_finite_stability# ;
proofend;
end;

registration
let G be with_finite_stability# SimpleGraph;
cluster stable  ->  finite for Element of bool (Vertices G);
correctness
coherence
for b1 being StableSet of G holds b1 is finite ;
proofend;
end;

registration
cluster non empty finite-membered V233() V267() subset-closed non void 1 -at_most_dimensional SimpleGraph-like with_finite_stability# for set ;
existence
 ex b1 being SimpleGraph st
( b1 is with_finite_stability# &amp; not b1 is void )
proofend;
end;

definition
let G be with_finite_stability# SimpleGraph;
func stability# G ->  Nat means :Lstabno: :: SCMYCIEL:def 24
( ex A being finite StableSet of G st card A = it &amp; ( for T being finite StableSet of G holds card T <= it ) );
existence
 ex b1 being Nat st
( ex A being finite StableSet of G st card A = b1 &amp; ( for T being finite StableSet of G holds card T <= b1 ) )
proofend;
uniqueness
 for b1, b2 being Nat st ex A being finite StableSet of G st card A = b1 &amp; ( for T being finite StableSet of G holds card T <= b1 ) &amp; ex A being finite StableSet of G st card A = b2 &amp; ( for T being finite StableSet of G holds card T <= b2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Lstabno defines stability# SCMYCIEL:def_24_:_
 for G being with_finite_stability# SimpleGraph
for b2 being Nat holds
( b2 = stability# G iff ( ex A being finite StableSet of G st card A = b2 &amp; ( for T being finite StableSet of G holds card T <= b2 ) ) );

registration
let G be non void with_finite_stability# SimpleGraph;
cluster stability# G ->  positive ;
correctness
coherence
stability# G is positive ;
proofend;
end;

theorem Th21: :: SCMYCIEL:71
for G being with_finite_stability# SimpleGraph st stability# G = 1 holds
G is clique
proofend;

registration
cluster SimpleGraph-like with_finite_clique# with_finite_stability#  ->  finite for set ;
correctness
coherence
for b1 being SimpleGraph st b1 is with_finite_clique# &amp; b1 is with_finite_stability# holds
b1 is finite ;
proofend;
end;

theorem CliStaCompl: :: SCMYCIEL:72
for G being SimpleGraph
for C being Clique of G holds Vertices C is StableSet of (Complement G)
proofend;

theorem CliComplSta: :: SCMYCIEL:73
for G being SimpleGraph
for C being Clique of (Complement G) holds Vertices C is StableSet of G
proofend;

theorem StaCliCompl: :: SCMYCIEL:74
for G being SimpleGraph
for C being StableSet of G holds (Complement G) SubgraphInducedBy C is Clique of (Complement G)
proofend;

theorem StaComplCli: :: SCMYCIEL:75
for G being SimpleGraph
for C being StableSet of (Complement G) holds G SubgraphInducedBy C is Clique of G
proofend;

registration
let G be with_finite_clique# SimpleGraph;
cluster Complement G ->  with_finite_stability# ;
correctness
coherence
Complement G is with_finite_stability# ;
proofend;
end;

registration
let G be with_finite_stability# SimpleGraph;
cluster Complement G ->  with_finite_clique# ;
correctness
coherence
Complement G is with_finite_clique# ;
proofend;
end;

theorem cliRstaCR: :: SCMYCIEL:76
for G being with_finite_clique# SimpleGraph holds clique# G = stability# (Complement G)
proofend;

theorem :: SCMYCIEL:77
for G being with_finite_stability# SimpleGraph holds stability# G = clique# (Complement G)
proofend;

theorem ClicoComplChr: :: SCMYCIEL:78
for G being SimpleGraph
for C being Clique-partition of (Complement G) holds C is Coloring of G
proofend;

theorem ClicoChrCompl: :: SCMYCIEL:79
for G being SimpleGraph
for C being Clique-partition of G holds C is Coloring of (Complement G)
proofend;

theorem ChrClicoCompl: :: SCMYCIEL:80
for G being SimpleGraph
for C being Coloring of G holds C is Clique-partition of (Complement G)
proofend;

theorem :: SCMYCIEL:81
for G being SimpleGraph
for C being Coloring of (Complement G) holds C is Clique-partition of G
proofend;

registration
let G be finitely_colorable SimpleGraph;
cluster Complement G ->  with_finite_cliquecover# ;
correctness
coherence
Complement G is with_finite_cliquecover# ;
proofend;
end;

registration
let G be with_finite_cliquecover# SimpleGraph;
cluster Complement G ->  finitely_colorable ;
correctness
coherence
Complement G is finitely_colorable ;
proofend;
end;

theorem chrRcovCR: :: SCMYCIEL:82
for G being finitely_colorable SimpleGraph holds chromatic# G = cliquecover# (Complement G)
proofend;

theorem :: SCMYCIEL:83
for G being with_finite_cliquecover# SimpleGraph holds cliquecover# G = chromatic# (Complement G)
proofend;

begin

definition
let G be SimpleGraph;
func Mycielskian G ->  SimpleGraph equals :: SCMYCIEL:def 25
((({{}} \/  {  {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum  }  ) \/ (Edges G)) \/  {  {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G  }  ) \/  {  {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G  }  ;
correctness
coherence
((({{}} \/  {  {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum  }  ) \/ (Edges G)) \/  {  {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G  }  ) \/  {  {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G  }  is SimpleGraph;
proofend;
end;

:: deftheorem  defines Mycielskian SCMYCIEL:def_25_:_
 for G being SimpleGraph holds Mycielskian G = ((({{}} \/  {  {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum  }  ) \/ (Edges G)) \/  {  {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G  }  ) \/  {  {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G  }  ;

theorem M0: :: SCMYCIEL:84
for G being SimpleGraph holds G c= Mycielskian G
proofend;

theorem M0v1: :: SCMYCIEL:85
for G being SimpleGraph
for v being set holds
( v in Vertices (Mycielskian G) iff ( v in union G or ex x being set st
( x in union G &amp; v = [x,(union G)] ) or v = union G ) )
proofend;

theorem M0v2: :: SCMYCIEL:86
for G being SimpleGraph holds Vertices (Mycielskian G) = ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)}
proofend;

theorem M00: :: SCMYCIEL:87
for G being SimpleGraph holds union G in union (Mycielskian G)
proofend;

theorem MGvoid: :: SCMYCIEL:88
for G being void SimpleGraph holds Mycielskian G = {{},{(union G)}}
proofend;

registration
let G be finite SimpleGraph;
cluster Mycielskian G ->  finite ;
correctness
coherence
Mycielskian G is finite ;
proofend;
end;

theorem M0order: :: SCMYCIEL:89
for G being finite SimpleGraph holds order (Mycielskian G) = (2 * (order G)) + 1
proofend;

theorem M0e0: :: SCMYCIEL:90
for G being SimpleGraph
for e being set holds
( e in Edges (Mycielskian G) iff ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} &amp; {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} &amp; y in union G ) ) )
proofend;

theorem M0e: :: SCMYCIEL:91
for G being SimpleGraph holds Edges (Mycielskian G) = ((Edges G) \/  {  {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G  }  ) \/  {  {(union G),[y,(union G)]} where y is Element of union G : y in union G  }
proofend;

theorem M0size: :: SCMYCIEL:92
for G being finite SimpleGraph holds size (Mycielskian G) = (3 * (size G)) + (order G)
proofend;

theorem M0e1: :: SCMYCIEL:93
for G being SimpleGraph
for s, t being set holds
( not {s,t} in Edges (Mycielskian G) or {s,t} in Edges G or ( ( s in union G or s = union G ) &amp; ex y being set st
( y in union G &amp; t = [y,(union G)] ) ) or ( ( t in union G or t = union G ) &amp; ex y being set st
( y in union G &amp; s = [y,(union G)] ) ) )
proofend;

theorem M0e2: :: SCMYCIEL:94
for G being SimpleGraph
for u being set st {(union G),u} in Edges (Mycielskian G) holds
ex x being set st
( x in union G &amp; u = [x,(union G)] )
proofend;

theorem M0e2aa: :: SCMYCIEL:95
for G being SimpleGraph
for u being set st u in Vertices G holds
{[u,(union G)]} in Mycielskian G
proofend;

theorem M0e2a: :: SCMYCIEL:96
for G being SimpleGraph
for u being set st u in Vertices G holds
{[u,(union G)],(union G)} in Mycielskian G
proofend;

theorem M0e3: :: SCMYCIEL:97
for G being SimpleGraph
for x, y being set holds not {[x,(union G)],[y,(union G)]} in Edges (Mycielskian G)
proofend;

theorem M0e3a: :: SCMYCIEL:98
for G being SimpleGraph
for x, y being set st x <> y holds
not {[x,(union G)],[y,(union G)]} in Mycielskian G
proofend;

theorem M0e4: :: SCMYCIEL:99
for G being SimpleGraph
for x, y being set st {[x,(union G)],y} in Edges (Mycielskian G) holds
( x <> y &amp; x in union G &amp; ( y in union G or y = union G ) )
proofend;

theorem M0e4a: :: SCMYCIEL:100
for G being SimpleGraph
for x, y being set st {[x,(union G)],y} in Mycielskian G holds
x <> y
proofend;

theorem M0e4b: :: SCMYCIEL:101
for G being SimpleGraph
for x, y being set st y in union G &amp; {[x,(union G)],y} in Mycielskian G holds
{x,y} in G
proofend;

theorem M0e4c: :: SCMYCIEL:102
for G being SimpleGraph
for x, y being set st {x,y} in Edges G holds
{[x,(union G)],y} in Mycielskian G
proofend;

theorem M1: :: SCMYCIEL:103
for G being SimpleGraph
for x, y being set st x in Vertices G &amp; y in Vertices G &amp; {x,y} in Mycielskian G holds
{x,y} in G
proofend;

theorem GsubMG: :: SCMYCIEL:104
for G being SimpleGraph holds G = (Mycielskian G) SubgraphInducedBy (Vertices G)
proofend;

theorem MClique3: :: SCMYCIEL:105
for G being SimpleGraph
for C being finite Clique of (Mycielskian G) st 3 <= order C holds
for v being Vertex of C holds v <> union G
proofend;

theorem MClique0: :: SCMYCIEL:106
for G being with_finite_clique# SimpleGraph st clique# G = 0 holds
for D being finite Clique of (Mycielskian G) holds order D <= 1
proofend;

theorem :: SCMYCIEL:107
for G being SimpleGraph
for x being set st Vertices G = {x} holds
Mycielskian G = {{},{x},{[x,(union G)]},{(union G)},{[x,(union G)],(union G)}}
proofend;

theorem MClique1: :: SCMYCIEL:108
for G being with_finite_clique# SimpleGraph st clique# G = 1 holds
for D being finite Clique of (Mycielskian G) holds order D <= 2
proofend;

theorem MClique2: :: SCMYCIEL:109
for G being with_finite_clique# SimpleGraph st 2 <= clique# G holds
for D being finite Clique of (Mycielskian G) holds order D <= clique# G
proofend;

registration
let G be with_finite_clique# SimpleGraph;
cluster Mycielskian G ->  with_finite_clique# ;
coherence
 Mycielskian G is with_finite_clique#
proofend;
end;

theorem MClique: :: SCMYCIEL:110
for G being with_finite_clique# SimpleGraph st 2 <= clique# G holds
clique# (Mycielskian G) = clique# G
proofend;

theorem Mfc1: :: SCMYCIEL:111
for G being finitely_colorable SimpleGraph ex E being Coloring of (Mycielskian G) st card E = 1 + (chromatic# G)
proofend;

registration
let G be finitely_colorable SimpleGraph;
cluster Mycielskian G ->  finitely_colorable ;
coherence
 Mycielskian G is finitely_colorable
proofend;
end;

theorem Mcn1: :: SCMYCIEL:112
for G being finitely_colorable SimpleGraph holds chromatic# (Mycielskian G) = 1 + (chromatic# G)
proofend;

definition
let G be SimpleGraph;
func MycielskianSeq G ->  ManySortedSet of NAT  means :LMycielskianSeq: :: SCMYCIEL:def 26
 ex myc being Function st
( it = myc &amp; myc . 0 = G &amp; ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) );
existence
 ex b1 being ManySortedSet of NAT ex myc being Function st
( b1 = myc &amp; myc . 0 = G &amp; ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) )
proofend;
uniqueness
 for b1, b2 being ManySortedSet of NAT st ex myc being Function st
( b1 = myc &amp; myc . 0 = G &amp; ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) ) &amp; ex myc being Function st
( b2 = myc &amp; myc . 0 = G &amp; ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) ) holds
b1 = b2
proofend;
end;

:: deftheorem LMycielskianSeq defines MycielskianSeq SCMYCIEL:def_26_:_
 for G being SimpleGraph
for b2 being ManySortedSet of NAT holds
( b2 = MycielskianSeq G iff ex myc being Function st
( b2 = myc &amp; myc . 0 = G &amp; ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) ) );

theorem MSeq0: :: SCMYCIEL:113
for G being SimpleGraph holds (MycielskianSeq G) . 0 = G
proofend;

theorem MGS0: :: SCMYCIEL:114
for G being SimpleGraph
for n being Nat holds (MycielskianSeq G) . n is SimpleGraph
proofend;

registration
let G be SimpleGraph;
let n be Nat;
cluster(MycielskianSeq G) . n ->  SimpleGraph-like ;
coherence
 (MycielskianSeq G) . n is SimpleGraph-like by MGS0;
end;

theorem MSeq1: :: SCMYCIEL:115
for G, H being SimpleGraph
for n being Nat holds (MycielskianSeq G) . (n + 1) = Mycielskian ((MycielskianSeq G) . n)
proofend;

registration
let G be with_finite_clique# SimpleGraph;
let n be Nat;
cluster(MycielskianSeq G) . n ->  with_finite_clique# ;
coherence
 (MycielskianSeq G) . n is with_finite_clique#
proofend;
end;

registration
let G be finitely_colorable SimpleGraph;
let n be Nat;
cluster(MycielskianSeq G) . n ->  finitely_colorable ;
coherence
 (MycielskianSeq G) . n is finitely_colorable
proofend;
end;

registration
let G be finite SimpleGraph;
let n be Nat;
cluster(MycielskianSeq G) . n ->  finite ;
coherence
 (MycielskianSeq G) . n is finite
proofend;
end;

theorem MSnorder: :: SCMYCIEL:116
for G being finite SimpleGraph
for n being Nat holds order ((MycielskianSeq G) . n) = (((2 |^ n) * (order G)) + (2 |^ n)) - 1
proofend;

theorem :: SCMYCIEL:117
for G being finite SimpleGraph
for n being Nat holds size ((MycielskianSeq G) . n) = (((3 |^ n) * (size G)) + (((3 |^ n) - (2 |^ n)) * (order G))) + ((n + 1) block 3)
proofend;

theorem MycTh: :: SCMYCIEL:118
for n being Nat holds
( clique# ((MycielskianSeq (CompleteSGraph 2)) . n) = 2 &amp; chromatic# ((MycielskianSeq (CompleteSGraph 2)) . n) = n + 2 )
proofend;

theorem :: SCMYCIEL:119
for n being Nat ex G being finite SimpleGraph st
( clique# G = 2 &amp; chromatic# G > n )
proofend;

theorem :: SCMYCIEL:120
for n being Nat ex G being finite SimpleGraph st
( stability# G = 2 &amp; cliquecover# G > n )
proofend;