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
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 ; :: thesis: 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 :: thesis: for d, e being Nat st d in dom f & e in dom f & d <> e holds
f . d misses f . e

let d, e be Nat; :: thesis: ( 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 ; :: thesis: f . d misses f . e
A13: 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; :: thesis: 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 :: thesis: for j being Nat st j in Seg (stability# R) holds
Cf . j <= h . j

let j be Nat; :: thesis: ( j in Seg (stability# R) implies Cf . j <= h . j )
assume A19: j in Seg (stability# R) ; :: thesis: Cf . j <= h . j
A20: 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; :: thesis: 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; :: thesis: verum