let G be with_finite_clique# SimpleGraph; ( 2 <= clique# G implies for D being finite Clique of (Mycielskian G) holds order D <= clique# G )
assume A1:
2 <= clique# G
; for D being finite Clique of (Mycielskian G) holds order D <= clique# G
let D be finite Clique of (Mycielskian G); order D <= clique# G
assume A2:
order D > clique# G
; contradiction
set MG = Mycielskian G;
set uG = union G;
A3:
Vertices D c= Vertices (Mycielskian G)
by ZFMISC_1:77;
A4:
Edges D c= Edges (Mycielskian G)
by Th14;
2 < order D
by A2, A1, XXREAL_0:2;
then A5:
2 + 1 <= order D
by NAT_1:13;
per cases
( D c= G or not D c= G )
;
suppose
not
D c= G
;
contradictionthen consider e being
object such that A6:
e in D
and A7:
not
e in G
;
then consider v being
object such that A15:
v in Vertices D
and A16:
not
v in Vertices G
;
Segm 3
c= Segm (order D)
by A5, NAT_1:39;
then consider v1,
v2 being
object such that A17:
v1 in Vertices D
and A18:
v2 in Vertices D
and A19:
v1 <> v
and A20:
v2 <> v
and A21:
v1 <> v2
by Th5;
{v,v1} in D
by A15, A17, Th53;
then A22:
{v,v1} in Edges D
by A19, Th12;
{v,v2} in D
by A15, A18, Th53;
then A23:
{v,v2} in Edges D
by A20, Th12;
{v1,v2} in D
by A17, A18, Th53;
then A24:
{v1,v2} in Edges D
by A21, Th12;
per cases
( v = union G or ex x being set st
( x in union G & v = [x,(union G)] ) )
by A15, A3, A16, Th85;
suppose A25:
v = union G
;
contradictionconsider x being
object such that
x in union G
and A26:
v1 = [x,(union G)]
by A25, A22, A4, Th94;
consider y being
object such that
y in union G
and A27:
v2 = [y,(union G)]
by A25, A23, A4, Th94;
thus
contradiction
by A24, A4, A26, A27, Th97;
verum end; suppose
ex
x being
set st
(
x in union G &
v = [x,(union G)] )
;
contradictionthen consider x being
set such that A28:
x in union G
and A29:
v = [x,(union G)]
;
set E =
D SubgraphInducedBy (union G);
reconsider F =
G SubgraphInducedBy ({x} \/ (union (D SubgraphInducedBy (union G)))) as
finite SimpleGraph ;
A30:
Vertices F = {x} \/ (Vertices (D SubgraphInducedBy (union G)))
A34:
union (D SubgraphInducedBy (union G)) c= union D
by ZFMISC_1:77;
reconsider Fs =
F as
SimpleGraph-like Subset of
G ;
now for a, b being set st a <> b & a in union Fs & b in union Fs holds
{a,b} in Edges Fslet a,
b be
set ;
( a <> b & a in union Fs & b in union Fs implies {a,b} in Edges Fs )assume that A36:
a <> b
and A37:
a in union Fs
and A38:
b in union Fs
;
{a,b} in Edges FsA39:
a in (union G) /\ ({x} \/ (union (D SubgraphInducedBy (union G))))
by A37, Th45;
then A40:
(
a in union G &
a in {x} \/ (union (D SubgraphInducedBy (union G))) )
by XBOOLE_0:def 4;
A41:
b in (union G) /\ ({x} \/ (union (D SubgraphInducedBy (union G))))
by A38, Th45;
then A42:
(
b in union G &
b in {x} \/ (union (D SubgraphInducedBy (union G))) )
by XBOOLE_0:def 4;
A43:
a in Vertices G
by A39, XBOOLE_0:def 4;
A44:
b in Vertices G
by A41, XBOOLE_0:def 4;
x in {x}
by TARSKI:def 1;
then A45:
x in {x} \/ (union (D SubgraphInducedBy (union G)))
by XBOOLE_0:def 3;
{a,b} in Fs
proof
per cases
( ( a in {x} & b in {x} ) or ( a in {x} & b in union (D SubgraphInducedBy (union G)) ) or ( b in {x} & a in union (D SubgraphInducedBy (union G)) ) or ( a in union (D SubgraphInducedBy (union G)) & b in union (D SubgraphInducedBy (union G)) ) )
by A40, A42, XBOOLE_0:def 3;
suppose A47:
(
a in {x} &
b in union (D SubgraphInducedBy (union G)) )
;
{a,b} in Fsthen A48:
a = x
by TARSKI:def 1;
b in (union D) /\ (union G)
by A47, Th45;
then A49:
(
b in union D &
b in union G )
by XBOOLE_0:def 4;
then
{[x,(union G)],b} in D
by A15, A29, Th53;
then
{x,b} in G
by A49, Th101;
hence
{a,b} in Fs
by A45, A48, A42, Lm10;
verum end; suppose A50:
(
b in {x} &
a in union (D SubgraphInducedBy (union G)) )
;
{a,b} in Fsthen A51:
b = x
by TARSKI:def 1;
a in (union D) /\ (union G)
by A50, Th45;
then A52:
(
a in union D &
a in union G )
by XBOOLE_0:def 4;
then
{[x,(union G)],a} in D
by A15, A29, Th53;
then
{x,a} in G
by A52, Th101;
hence
{a,b} in Fs
by A45, A51, A40, Lm10;
verum end; end;
end; hence
{a,b} in Edges Fs
by A36, Th12;
verum end; then A53:
Fs is
clique
by Th47;
A54:
Vertices D c= {v} \/ (Vertices (D SubgraphInducedBy (union G)))
proof
let a be
object ;
TARSKI:def 3 ( not a in Vertices D or a in {v} \/ (Vertices (D SubgraphInducedBy (union G))) )
assume A55:
a in Vertices D
;
a in {v} \/ (Vertices (D SubgraphInducedBy (union G)))
per cases
( a = v or a <> v )
;
suppose A56:
a <> v
;
a in {v} \/ (Vertices (D SubgraphInducedBy (union G)))
{a,[x,(union G)]} in D
by A29, A15, A55, Th53;
then
{a,[x,(union G)]} in Edges D
by A56, A29, Th12;
then
(
a in union G or
a = union G )
by A4, Th99;
then
a in Vertices (D SubgraphInducedBy (union G))
by A5, Th105, A55, Lm8;
hence
a in {v} \/ (Vertices (D SubgraphInducedBy (union G)))
by XBOOLE_0:def 3;
verum end; end;
end; A57:
Vertices (D SubgraphInducedBy (union G)) c= Vertices D
by ZFMISC_1:77;
A58:
{v} \/ (Vertices (D SubgraphInducedBy (union G))) c= Vertices D
A59:
not
v in Vertices (D SubgraphInducedBy (union G))
by A29, Lm7, Th1;
order F =
1
+ (card (Vertices (D SubgraphInducedBy (union G))))
by A30, A35, CARD_2:41
.=
card ({v} \/ (Vertices (D SubgraphInducedBy (union G))))
by A59, CARD_2:41
.=
order D
by A58, A54, XBOOLE_0:def 10
;
hence
contradiction
by A2, A53, Def15;
verum end; end; end; end;