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
A:
2 <= clique# R
and
B:
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);
Carn:
the carrier of R = n
by LNRS;
Car:
the carrier of R c= the carrier of (Mycielskian R)
by cMR0;
consider C being finite Clique of R such that
C:
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
n c= (2 * n) + 1
by NAT_1:40;
then reconsider S = n as Subset of (Mycielskian R) by LNRS;
F:
R = subrelstr S
by Msubrel;
then
C is Clique of (Mycielskian R)
by DILWORTH:28;
then
card C <= clique# (Mycielskian R)
by DILWORTH:def 4;
then D:
clique# R < clique# (Mycielskian R)
by B, C, XXREAL_0:1;
then
2 < clique# (Mycielskian R)
by A, XXREAL_0:2;
then Da:
2 + 1 <= clique# (Mycielskian R)
by NAT_1:13;
consider D being finite Clique of (Mycielskian R) such that
E:
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
set such that A1:
x in D
and B1:
not
x in n
by TARSKI:def 3;
x in the
carrier of
(Mycielskian R)
by A1;
then C1:
x in (2 * n) + 1
by LNRS;
reconsider x =
x as
Nat by C1, NECKLACE:4;
reconsider xp1 =
x as
Element of
(Mycielskian R) by A1;
D1:
x >= n
by B1, NAT_1:45;
x < (2 * n) + 1
by C1, NAT_1:45;
then E1:
x <= 2
* n
by NAT_1:13;
F1:
for
y being
set st
y in D &
x <> y holds
y in n
proof
let y be
set ;
( y in D & x <> y implies y in n )
assume that A2:
y in D
and B2:
x <> y
and C2:
not
y in n
;
contradiction
y in the
carrier of
(Mycielskian R)
by A2;
then D2:
y in (2 * n) + 1
by LNRS;
reconsider y =
y as
Nat by D2, NECKLACE:4;
reconsider yp1 =
y as
Element of
(Mycielskian R) by A2;
D2a:
y >= n
by C2, NAT_1:45;
y < (2 * n) + 1
by D2, NAT_1:45;
then E2:
y <= 2
* n
by NAT_1:13;
set DD =
D \ {x,y};
{x,y} c= D
by A2, A1, ZFMISC_1:38;
then F2a:
card (D \ {x,y}) = (card D) - (card {x,y})
by CARD_2:63;
(1 + 2) - 2
<= (card D) - 2
by Da, E, XREAL_1:11;
then
1
<= card (D \ {x,y})
by F2a, B2, CARD_2:76;
then consider z being
set such that G2:
z in D \ {x,y}
by XBOOLE_0:def 1, CARD_1:47;
A2z:
z in D
by G2, XBOOLE_0:def 5;
A2zz:
z in the
carrier of
(Mycielskian R)
by G2;
reconsider zp1 =
z as
Element of
(Mycielskian R) by G2;
D2z:
z in (2 * n) + 1
by A2zz, LNRS;
reconsider z =
z as
Nat by D2z, NECKLACE:4;
x in {x,y}
by TARSKI:def 2;
then G2z:
z <> x
by G2, XBOOLE_0:def 5;
y in {x,y}
by TARSKI:def 2;
then H2z:
z <> y
by G2, 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 E1, E2, XXREAL_0:1;
suppose S1:
(
x < 2
* n &
y < 2
* n )
;
contradictionend; suppose S1:
(
x < 2
* n &
y = 2
* n )
;
contradiction
(
xp1 <= zp1 or
zp1 <= xp1 )
by G2z, A2z, A1, DILWORTH:6;
then A3:
(
[x,z] in the
InternalRel of
(Mycielskian R) or
[z,x] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 9;
(
yp1 <= zp1 or
zp1 <= yp1 )
by H2z, A2z, A2, DILWORTH:6;
then
(
[y,z] in the
InternalRel of
(Mycielskian R) or
[z,y] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 9;
then
(
n <= z &
z < 2
* n )
by S1, D2a, iMR0;
hence
contradiction
by A3, S1, D1, iMR0;
verum suppose S1:
(
x = 2
* n &
y < 2
* n )
;
contradiction
(
yp1 <= zp1 or
zp1 <= yp1 )
by H2z, A2z, A2, DILWORTH:6;
then B3:
(
[y,z] in the
InternalRel of
(Mycielskian R) or
[z,y] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 9;
(
xp1 <= zp1 or
zp1 <= xp1 )
by G2z, A2z, A1, DILWORTH:6;
then
(
[x,z] in the
InternalRel of
(Mycielskian R) or
[z,x] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 9;
then
(
n <= z &
z < 2
* n )
by S1, D1, iMR0;
hence
contradiction
by B3, S1, D2a, iMR0;
verum suppose
(
x = 2
* n &
y = 2
* n )
;
contradictionhence
contradiction
by B2;
verum end;
end; C2X:
card (D \ {x}) =
(card D) - (card {x})
by A1, EULER_1:5
.=
(card D) - 1
by CARD_1:50
;
per cases
( x < 2 * n or x = 2 * n )
by E1, XXREAL_0:1;
suppose S2:
x < 2
* n
;
contradictionconsider xx being
Nat such that A2:
x = n + xx
by D1, NAT_1:10;
n + xx < n + n
by S2, A2;
then B2a:
xx < n
by XREAL_1:8;
then B2:
xx in n
by NAT_1:45;
reconsider xxp1 =
xx as
Element of
(Mycielskian R) by B2, Car, Carn;
C2:
now assume
xx in D
;
contradictionthen
(
xp1 <= xxp1 or
xxp1 <= xp1 )
by A1, B2a, D1, DILWORTH:6;
then
(
[x,xx] in the
InternalRel of
(Mycielskian R) or
[xx,x] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 9;
then
(
[xx,xx] in the
InternalRel of
R or
[xx,xx] in the
InternalRel of
R )
by B2, A2, iMR1c, iMR1d;
hence
contradiction
by B2, Carn, NECKLACE:def 6;
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 let a,
b be
Element of
R;
( a in DD & b in DD & a <> b & not b1 <= b2 implies b2 <= b1 )assume that A3:
a in DD
and B3:
b in DD
and C3:
a <> b
;
( b1 <= b2 or b2 <= b1 )
(
a in D \ {x} or
a in {xx} )
by A3, XBOOLE_0:def 3;
then D3:
( (
a in D & not
a in {x} ) or
a = xx )
by XBOOLE_0:def 5, TARSKI:def 1;
(
b in D \ {x} or
b in {xx} )
by B3, XBOOLE_0:def 3;
then E3:
( (
b in D & not
b in {x} ) or
b = xx )
by XBOOLE_0:def 5, TARSKI:def 1;
F3:
(
a in the
carrier of
R &
b in the
carrier of
R )
by A3;
reconsider an =
a,
bn =
b as
Nat by A3, Carn, NECKLACE:4;
reconsider ap1 =
a,
bp1 =
b as
Element of
(Mycielskian R) by F3, Car;
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 C3, D3, E3, TARSKI:def 1;
suppose S3:
(
a in D &
a <> x &
b = xx )
;
( b1 <= b2 or b2 <= b1 )
(
ap1 <= xp1 or
xp1 <= ap1 )
by S3, A1, DILWORTH:6;
then
(
[ap1,x] in the
InternalRel of
(Mycielskian R) or
[x,ap1] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 9;
then
(
[an,xx] in the
InternalRel of
R or
[xx,an] in the
InternalRel of
R )
by Carn, B2a, A2, iMR1c, iMR1d;
hence
(
a <= b or
b <= a )
by S3, ORDERS_2:def 9;
verum suppose S3:
(
a = xx &
b in D &
b <> x )
;
( b1 <= b2 or b2 <= b1 )
(
bp1 <= xp1 or
xp1 <= bp1 )
by S3, A1, DILWORTH:6;
then
(
[bp1,x] in the
InternalRel of
(Mycielskian R) or
[x,bp1] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 9;
then
(
[bn,xx] in the
InternalRel of
R or
[xx,bn] in the
InternalRel of
R )
by Carn, B2a, A2, iMR1c, iMR1d;
hence
(
a <= b or
b <= a )
by S3, ORDERS_2:def 9;
verum end; then reconsider DD =
DD as
Clique of
R by DILWORTH:6;
C2a:
not
xx in D \ {x}
by C2, XBOOLE_0:def 5;
card DD =
((card D) - 1) + 1
by C2a, C2X, CARD_2:54
.=
card D
;
hence
contradiction
by E, D, DILWORTH:def 4;
verum end; suppose S2:
x = 2
* n
;
contradiction
(2 + 1) - 1
<= (card D) - 1
by E, Da, XREAL_1:11;
then
2
c= card (D \ {x})
by C2X, NAT_1:40;
then consider y,
z being
set such that G1:
y in D \ {x}
and
z in D \ {x}
and
y <> z
by PENCIL_1:2;
J1:
y in D
by G1, ZFMISC_1:64;
K1:
x <> y
by G1, ZFMISC_1:64;
y in the
carrier of
(Mycielskian R)
by G1;
then
y in (2 * n) + 1
by LNRS;
then reconsider y =
y as
Nat by NECKLACE:4;
reconsider yp1 =
y as
Element of
(Mycielskian R) by G1;
(
yp1 <= xp1 or
xp1 <= yp1 )
by K1, J1, A1, DILWORTH:6;
then L1:
(
[y,x] in the
InternalRel of
(Mycielskian R) or
[x,y] in the
InternalRel of
(Mycielskian R) )
by ORDERS_2:def 9;
y in n
by F1, J1, K1;
then M1:
y < n
by NAT_1:45;
n <= n + n
by NAT_1:11;
hence
contradiction
by L1, S2, M1, iMR0;
verum end; end;