let R be finite transitive antisymmetric RelStr ; for r, s being Nat holds
( not card R = (r * s) + 1 or ex C being Clique of R st card C >= r + 1 or ex A being StableSet of R st card A >= s + 1 )
let r, s be Nat; ( not card R = (r * s) + 1 or ex C being Clique of R st card C >= r + 1 or ex A being StableSet of R st card A >= s + 1 )
assume that
A1:
card R = (r * s) + 1
and
A2:
for C being Clique of R holds card C < r + 1
and
A3:
for A being StableSet of R holds card A < s + 1
; contradiction
consider p being Clique-partition of R such that
A4:
card p = stability# R
by Th51;
consider A being finite StableSet of R such that
A5:
card A = stability# R
by Def6;
stability# R < s + 1
by A3, A5;
then A6:
stability# R <= s
by NAT_1:13;
set wR = stability# R;
set cR = the carrier of R;
set f = canFS p;
A7:
len (canFS p) = card p
by FINSEQ_1:93;
A8:
dom (canFS p) = Seg (len (canFS p))
by FINSEQ_1:def 3;
set f = canFS p;
A9:
rng (canFS p) = p
by FUNCT_2:def 3;
then reconsider f = canFS p as FinSequence of bool the carrier of R by FINSEQ_1:def 4;
now for d, e being Nat st d in dom f & e in dom f & d <> e holds
f . d misses f . elet d,
e be
Nat;
( d in dom f & e in dom f & d <> e implies f . d misses f . e )assume that A10:
d in dom f
and A11:
e in dom f
and A12:
d <> e
;
f . d misses f . eA13:
f . d in rng f
by A10, FUNCT_1:3;
A14:
f . e in rng f
by A11, FUNCT_1:3;
then reconsider fd =
f . d,
fe =
f . e as
Subset of the
carrier of
R by A13, A9;
fd <> fe
by A12, A10, A11, FUNCT_1:def 4;
hence
f . d misses f . e
by A13, A14, A9, EQREL_1:def 4;
verum end;
then A15:
card (union (rng f)) = Sum (Card f)
by INT_5:48;
reconsider n9 = r as Element of NAT by ORDINAL1:def 12;
reconsider h = (stability# R) |-> n9 as Element of (stability# R) -tuples_on NAT ;
A16:
Sum h = (stability# R) * r
by RVSUM_1:80;
dom f = dom (Card f)
by CARD_3:def 2;
then
len (Card f) = stability# R
by A7, A4, FINSEQ_3:29;
then reconsider Cf = Card f as Element of (stability# R) -tuples_on NAT by FINSEQ_2:92;
now for j being Nat st j in Seg (stability# R) holds
Cf . j <= h . jlet j be
Nat;
( j in Seg (stability# R) implies Cf . j <= h . j )assume A19:
j in Seg (stability# R)
;
Cf . j <= h . jA20:
h . j = r
by A19, FINSEQ_2:57;
A21:
Cf . j = card (f . j)
by A19, A7, A8, A4, CARD_3:def 2;
f . j in p
by A9, A19, A4, A7, A8, FUNCT_1:3;
then reconsider fj =
f . j as
Clique of
R by Def11;
card fj < r + 1
by A2;
hence
Cf . j <= h . j
by A20, A21, NAT_1:13;
verum end;
then A22:
Sum Cf <= Sum h
by RVSUM_1:82;
(stability# R) * r <= s * r
by A6, XREAL_1:64;
then
Sum Cf <= s * r
by A16, A22, XXREAL_0:2;
then
(r * s) + 1 <= (r * s) + 0
by A15, A9, A1, EQREL_1:def 4;
hence
contradiction
by XREAL_1:6; verum