let R be finite transitive antisymmetric RelStr ; :: thesis: 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; :: thesis: ( 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
A: card R = (r * s) + 1 and
B: for C being Clique of R holds card C < r + 1 and
C: for A being StableSet of R holds card A < s + 1 ; :: thesis: contradiction
consider p being Clique-partition of R such that
D: card p = stability# R by DWf;
consider A being finite StableSet of R such that
E: card A = stability# R by Lwidth;
stability# R < s + 1 by C, E;
then Fa: stability# R <= s by NAT_1:13;
set wR = stability# R;
set cR = the carrier of R;
set f = canFS p;
Fb: len (canFS p) = card p by UPROOTS:5;
Fd: dom (canFS p) = Seg (len (canFS p)) by FINSEQ_1:def 3;
set f = canFS p;
G: rng (canFS p) = p by FUNCT_2:def 3;
reconsider f = canFS p as FinSequence of bool the carrier of R by G, FINSEQ_1:def 4;

now

let d, e be Nat; :: thesis: ( d in dom f & e in dom f & d <> e implies f . d misses f . e )
assume that
A2: d in dom f and
B2: e in dom f and
C2: d <> e ; :: thesis: f . d misses f . e
D2: f . d in rng f by A2, FUNCT_1:12;
E2: f . e in rng f by B2, FUNCT_1:12;
reconsider fd = f . d, fe = f . e as Subset of the carrier of R by D2, E2, G;
fd <> fe by C2, A2, B2, FUNCT_1:def 8;
hence f . d misses f . e by D2, E2, G, EQREL_1:def 6; :: thesis: verum

end;

then I: card (union (rng f)) = Sum (Card f) by Fb, INT_5:48;
reconsider n9 = r as Element of NAT by ORDINAL1:def 13;
reconsider h = (stability# R) |-> n9 as Element of (stability# R) -tuples_on NAT by FINSEQ_2:132;
Ia: Sum h = (stability# R) * r by RVSUM_1:110;
dom f = dom (Card f) by CARD_3:def 2;
then Ib: len (Card f) = stability# R by Fb, D, FINSEQ_3:31;
reconsider Cf = Card f as Element of (stability# R) -tuples_on NAT by Ib, FINSEQ_2:110;
Ic: h is Element of (stability# R) -tuples_on REAL by FINSEQ_2:129;
Ie: Cf is Element of (stability# R) -tuples_on REAL by FINSEQ_2:129;

now

let j be Nat; :: thesis: ( j in Seg (stability# R) implies Cf . j <= h . j )
assume A2: j in Seg (stability# R) ; :: thesis: Cf . j <= h . j
B2: h . j = r by A2, FINSEQ_2:71;
C2: Cf . j = card (f . j) by A2, Fb, Fd, D, CARD_3:def 2;
f . j in p by G, A2, D, Fb, Fd, FUNCT_1:12;
then reconsider fj = f . j as Clique of R by LCpart;
card fj < r + 1 by B;
hence Cf . j <= h . j by B2, C2, NAT_1:13; :: thesis: verum

end;

then bI: Sum Cf <= Sum h by Ic, Ie, RVSUM_1:112;
(stability# R) * r <= s * r by Fa, XREAL_1:66;
then Sum Cf <= s * r by Ia, bI, XXREAL_0:2;
then (r * s) + 1 <= (r * s) + 0 by I, G, A, EQREL_1:def 6;
hence contradiction by XREAL_1:8; :: thesis: verum