begin
theorem Aux1:
for
x,
X being
set holds not
[x,X] in X
theorem Aux2:
for
x,
X being
set holds
[x,X] <> X
theorem Aux3:
for
x,
X being
set holds
[x,X] <> x
theorem Aux4:
for
x1,
y1,
x2,
y2,
X being
set st
x1 in X &
x2 in X &
{x1,[y1,X]} = {x2,[y2,X]} holds
(
x1 = x2 &
y1 = y2 )
theorem card3:
for
X,
v being
set st 3
c= card X holds
ex
v1,
v2 being
set st
(
v1 in X &
v2 in X &
v1 <> v &
v2 <> v &
v1 <> v2 )
CSGLem1:
for X being set holds union { V where V is finite Subset of X : card V <= 2 } = X
begin
Void0:
for n being Nat holds {{}} is n -at_most_dimensional
CisSG:
for G being SimpleGraph holds (CompleteSGraph (Vertices G)) \ (Edges G) is SimpleGraph
Compl1:
for G being SimpleGraph holds Vertices G = Vertices ((CompleteSGraph (Vertices G)) \ (Edges G))
Compl1a:
for G being SimpleGraph
for x, y being set st x <> y & x in Vertices G & y in Vertices G holds
( {x,y} in Edges G iff {x,y} nin Edges ((CompleteSGraph (Vertices G)) \ (Edges G)) )
Compl2:
for G, CG being SimpleGraph st CG = (CompleteSGraph (Vertices G)) \ (Edges G) holds
(CompleteSGraph (Vertices CG)) \ (Edges CG) = G
begin
Sub1:
for G being SimpleGraph
for L, x being set st x in Vertices (G SubgraphInducedBy L) holds
x in L
Sub3:
for G being SimpleGraph
for L, x being set st x in L & x in Vertices G holds
x in Vertices (G SubgraphInducedBy L)
Sub0c:
for G being SimpleGraph
for L being set st L c= Vertices G holds
Vertices (G SubgraphInducedBy L) = L
Sub6:
for G being SimpleGraph
for L, x, y being set st x in L & y in L & {x,y} in G holds
{x,y} in G SubgraphInducedBy L
begin
begin
begin