let n be Nat; for R being irreflexive NatRelStr of n st 2 <= clique# R holds
clique# R = clique# (Mycielskian R)
let R be irreflexive NatRelStr of n; ( 2 <= clique# R implies clique# R = clique# (Mycielskian R) )
assume that
A1:
2 <= clique# R
and
A2:
clique# R <> clique# (Mycielskian R)
; contradiction
set cR = the carrier of R;
set iR = the InternalRel of R;
set MR = Mycielskian R;
set cMR = the carrier of (Mycielskian R);
set iMR = the InternalRel of (Mycielskian R);
set cnMR = clique# (Mycielskian R);
A3:
the carrier of R = n
by Def7;
A4:
the carrier of R c= the carrier of (Mycielskian R)
by Th37;
consider C being finite Clique of R such that
A5:
card C = clique# R
by DILWORTH:def 4;
n <= n + n
by NAT_1:11;
then
n < (2 * n) + 1
by NAT_1:13;
then
Segm n c= Segm ((2 * n) + 1)
by NAT_1:39;
then reconsider S = n as Subset of (Mycielskian R) by Def7;
A6:
R = subrelstr S
by Th45;
then
C is Clique of (Mycielskian R)
by DILWORTH:28;
then
card C <= clique# (Mycielskian R)
by DILWORTH:def 4;
then A7:
clique# R < clique# (Mycielskian R)
by A2, A5, XXREAL_0:1;
then
2 < clique# (Mycielskian R)
by A1, XXREAL_0:2;
then A8:
2 + 1 <= clique# (Mycielskian R)
by NAT_1:13;
consider D being finite Clique of (Mycielskian R) such that
A9:
card D = clique# (Mycielskian R)
by DILWORTH:def 4;
per cases
( D c= n or not D c= n )
;
suppose
not
D c= n
;
contradictionthen consider x being
object such that A11:
x in D
and A12:
not
x in Segm n
;
x in the
carrier of
(Mycielskian R)
by A11;
then A13:
x in Segm ((2 * n) + 1)
by Def7;
reconsider x =
x as
Nat by A13;
reconsider xp1 =
x as
Element of
(Mycielskian R) by A11;
A14:
x >= n
by A12, NAT_1:44;
x < (2 * n) + 1
by A13, NAT_1:44;
then A15:
x <= 2
* n
by NAT_1:13;
A16:
for
y being
set st
y in D &
x <> y holds
y in Segm n
proof
let y be
set ;
( y in D & x <> y implies y in Segm n )
assume that A17:
y in D
and A18:
x <> y
and A19:
not
y in Segm n
;
contradiction
y in the
carrier of
(Mycielskian R)
by A17;
then A20:
y in Segm ((2 * n) + 1)
by Def7;
reconsider y =
y as
Nat by A20;
reconsider yp1 =
y as
Element of
(Mycielskian R) by A17;
A21:
y >= n
by A19, NAT_1:44;
y < (2 * n) + 1
by A20, NAT_1:44;
then A22:
y <= 2
* n
by NAT_1:13;
set DD =
D \ {x,y};
{x,y} c= D
by A17, A11, ZFMISC_1:32;
then A23:
card (D \ {x,y}) = (card D) - (card {x,y})
by CARD_2:44;
(1 + 2) - 2
<= (card D) - 2
by A8, A9, XREAL_1:9;
then
1
<= card (D \ {x,y})
by A23, A18, CARD_2:57;
then consider z being
object such that A24:
z in D \ {x,y}
by CARD_1:27, XBOOLE_0:def 1;
A25:
z in D
by A24, XBOOLE_0:def 5;
A26:
z in the
carrier of
(Mycielskian R)
by A24;
reconsider zp1 =
z as
Element of
(Mycielskian R) by A24;
A27:
z in Segm ((2 * n) + 1)
by A26, Def7;
reconsider z =
z as
Nat by A27;
x in {x,y}
by TARSKI:def 2;
then A28:
z <> x
by A24, XBOOLE_0:def 5;
y in {x,y}
by TARSKI:def 2;
then A29:
z <> y
by A24, XBOOLE_0:def 5;
per cases
( ( x < 2 * n & y < 2 * n ) or ( x < 2 * n & y = 2 * n ) or ( x = 2 * n & y < 2 * n ) or ( x = 2 * n & y = 2 * n ) )
by A15, A22, XXREAL_0:1;
suppose A30:
(
x < 2
* n &
y < 2
* n )
;
contradictionend; suppose A31:
(
x < 2
* n &
y = 2
* n )
;
contradiction
(
xp1 <= zp1 or
zp1 <= xp1 )
by A28, A25, A11, DILWORTH:6;
then A32:
(
[x,z] in the
InternalRel of
(Mycielskian R) or
[z,x] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 5;
(
yp1 <= zp1 or
zp1 <= yp1 )
by A29, A25, A17, DILWORTH:6;
then
(
[y,z] in the
InternalRel of
(Mycielskian R) or
[z,y] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 5;
then
(
n <= z &
z < 2
* n )
by A31, A21, Th38;
hence
contradiction
by A32, A31, A14, Th38;
verum suppose A33:
(
x = 2
* n &
y < 2
* n )
;
contradiction
(
yp1 <= zp1 or
zp1 <= yp1 )
by A29, A25, A17, DILWORTH:6;
then A34:
(
[y,z] in the
InternalRel of
(Mycielskian R) or
[z,y] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 5;
(
xp1 <= zp1 or
zp1 <= xp1 )
by A28, A25, A11, DILWORTH:6;
then
(
[x,z] in the
InternalRel of
(Mycielskian R) or
[z,x] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 5;
then
(
n <= z &
z < 2
* n )
by A33, A14, Th38;
hence
contradiction
by A34, A33, A21, Th38;
verum suppose
(
x = 2
* n &
y = 2
* n )
;
contradictionhence
contradiction
by A18;
verum end;
end; A35:
card (D \ {x}) =
(card D) - (card {x})
by A11, EULER_1:4
.=
(card D) - 1
by CARD_1:30
;
per cases
( x < 2 * n or x = 2 * n )
by A15, XXREAL_0:1;
suppose A36:
x < 2
* n
;
contradictionconsider xx being
Nat such that A37:
x = n + xx
by A14, NAT_1:10;
n + xx < n + n
by A36, A37;
then A38:
xx < n
by XREAL_1:6;
then A39:
xx in Segm n
by NAT_1:44;
reconsider xxp1 =
xx as
Element of
(Mycielskian R) by A39, A4, A3;
A40:
now not xx in Dassume
xx in D
;
contradictionthen
(
xp1 <= xxp1 or
xxp1 <= xp1 )
by A11, A38, A14, DILWORTH:6;
then
(
[x,xx] in the
InternalRel of
(Mycielskian R) or
[xx,x] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 5;
then
(
[xx,xx] in the
InternalRel of
R or
[xx,xx] in the
InternalRel of
R )
by A39, A37, Th42, Th43;
hence
contradiction
by A39, A3, NECKLACE:def 5;
verum end; set DD =
(D \ {x}) \/ {xx};
(D \ {x}) \/ {xx} c= the
carrier of
R
then reconsider DD =
(D \ {x}) \/ {xx} as
Subset of
R ;
now for a, b being Element of R st a in DD & b in DD & a <> b & not a <= b holds
b <= alet a,
b be
Element of
R;
( a in DD & b in DD & a <> b & not b1 <= b2 implies b2 <= b1 )assume that A41:
a in DD
and A42:
b in DD
and A43:
a <> b
;
( b1 <= b2 or b2 <= b1 )
(
a in D \ {x} or
a in {xx} )
by A41, XBOOLE_0:def 3;
then A44:
( (
a in D & not
a in {x} ) or
a = xx )
by TARSKI:def 1, XBOOLE_0:def 5;
(
b in D \ {x} or
b in {xx} )
by A42, XBOOLE_0:def 3;
then A45:
( (
b in D & not
b in {x} ) or
b = xx )
by TARSKI:def 1, XBOOLE_0:def 5;
A46:
(
a in the
carrier of
R &
b in the
carrier of
R )
by A41;
then
(
a in Segm n &
b in Segm n )
by A3;
then reconsider an =
a,
bn =
b as
Nat ;
reconsider ap1 =
a,
bp1 =
b as
Element of
(Mycielskian R) by A46, A4;
per cases
( ( a in D & a <> x & b in D & b <> x ) or ( a in D & a <> x & b = xx ) or ( a = xx & b in D & b <> x ) )
by A43, A44, A45, TARSKI:def 1;
suppose A48:
(
a in D &
a <> x &
b = xx )
;
( b1 <= b2 or b2 <= b1 )
(
ap1 <= xp1 or
xp1 <= ap1 )
by A48, A11, DILWORTH:6;
then
(
[ap1,x] in the
InternalRel of
(Mycielskian R) or
[x,ap1] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 5;
then
(
[an,xx] in the
InternalRel of
R or
[xx,an] in the
InternalRel of
R )
by A3, A37, Th42, Th43, A39;
hence
(
a <= b or
b <= a )
by A48, ORDERS_2:def 5;
verum suppose A49:
(
a = xx &
b in D &
b <> x )
;
( b1 <= b2 or b2 <= b1 )
(
bp1 <= xp1 or
xp1 <= bp1 )
by A49, A11, DILWORTH:6;
then
(
[bp1,x] in the
InternalRel of
(Mycielskian R) or
[x,bp1] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 5;
then
(
[bn,xx] in the
InternalRel of
R or
[xx,bn] in the
InternalRel of
R )
by A3, A37, Th42, Th43, A39;
hence
(
a <= b or
b <= a )
by A49, ORDERS_2:def 5;
verum end; then reconsider DD =
DD as
Clique of
R by DILWORTH:6;
A50:
not
xx in D \ {x}
by A40, XBOOLE_0:def 5;
card DD =
((card D) - 1) + 1
by A50, A35, CARD_2:41
.=
card D
;
hence
contradiction
by A9, A7, DILWORTH:def 4;
verum end; suppose A51:
x = 2
* n
;
contradiction
(2 + 1) - 1
<= (card D) - 1
by A9, A8, XREAL_1:9;
then
Segm 2
c= Segm (card (D \ {x}))
by A35, NAT_1:39;
then consider y,
z being
object such that A52:
y in D \ {x}
and
z in D \ {x}
and
y <> z
by PENCIL_1:2;
A53:
y in D
by A52, ZFMISC_1:56;
A54:
x <> y
by A52, ZFMISC_1:56;
y in the
carrier of
(Mycielskian R)
by A52;
then
y in Segm ((2 * n) + 1)
by Def7;
then reconsider y =
y as
Nat ;
reconsider yp1 =
y as
Element of
(Mycielskian R) by A52;
(
yp1 <= xp1 or
xp1 <= yp1 )
by A54, A53, A11, DILWORTH:6;
then A55:
(
[y,x] in the
InternalRel of
(Mycielskian R) or
[x,y] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 5;
y in Segm n
by A16, A53, A54;
then A56:
y < n
by NAT_1:44;
n <= n + n
by NAT_1:11;
hence
contradiction
by A55, A51, A56, Th38;
verum end; end;