let R be transitive antisymmetric with_finite_stability# RelStr ; :: thesis:

hence ex C being Clique-partition of R st card C = stability# R by Th51; :: thesis:

end;

defpred S₁[ Nat] means for P being non empty transitive antisymmetric with_finite_stability# RelStr st stability# P = $1 holds
ex C being Clique-partition of P st card C = stability# P;
A2: S₁[ 0 ] ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A4: S₁[k] ; :: thesis:
let P be non empty transitive antisymmetric with_finite_stability# RelStr ; :: thesis:
assume A5: stability# P = k + 1 ; :: thesis:
consider C being non empty Subset of P such that
A6: C is strong-chain and
A7: for D being Subset of P holds
( not D is strong-chain or not C c< D ) by Th52;
set cP = the carrier of P;

per cases ;

suppose A8: C = the carrier of P ; :: thesis:

for x being set st x in {C} holds
x is Clique of P by A6, TARSKI:def 1;
then reconsider Cp = {C} as Clique-partition of P by Def11, A8, EQREL_1:39;
take Cp ; :: thesis:
A9: the carrier of P = [#] P ;
thus card Cp = 1 by CARD_1:30
.= stability# P by A9, A6, A8, Th20 ; :: thesis:

end;

suppose C <> the carrier of P ; :: thesis:

then A10: C c< the carrier of P ;
set cP9 = the carrier of P \ C;
A11: the carrier of P \ ( the carrier of P \ C) = the carrier of P /\ C by XBOOLE_1:48
.= C by XBOOLE_1:28 ;
reconsider cP9 = the carrier of P \ C as Subset of P ;
cP9 <> {} by A10, XBOOLE_1:105;
then reconsider P9 = subrelstr cP9 as non empty transitive antisymmetric with_finite_stability# RelStr ;
A12: cP9 = the carrier of P9 by YELLOW_0:def 15;
A13: stability# P9 <= k + 1 by A5, Th44;
A14: stability# P9 <> k + 1

proof

assume A15: stability# P9 = k + 1 ; :: thesis:
consider A being finite StableSet of P9 such that
A16: card A = stability# P9 by Def6;
reconsider A9 = A as non empty finite StableSet of P by A16, Th30;
defpred S₂[ set , set , set ] means for c being set holds
( not c in $2 or not $1 /\ $3 c= c or ex d being set st
( d in $2 & d <> c & $3 /\ d <> {} ) );
defpred S₃[ finite Subset of P, set ] means for p being Clique-partition of (subrelstr $1) st card p <= stability# P holds
S₂[$1,p,$2];
defpred S₄[ object , object ] means ex S being non empty finite Subset of P st
( $2 = S & $1 in S & S₃[S,C \/ {$1}] );
A17: for x being object st x in A holds
ex y being object st S₄[x,y]

proof

let a be object ; :: thesis:
assume A18: a in A ; :: thesis:
A c= the carrier of P by A12, XBOOLE_1:1;
then {a} c= the carrier of P by A18, ZFMISC_1:31;
then reconsider Ca = C \/ {a} as Subset of P by XBOOLE_1:8;

now :: thesis:

assume A19: Ca is strong-chain ; :: thesis:
a in {a} by TARSKI:def 1;
then A20: a in Ca by XBOOLE_0:def 3;
A21: not a in C by A12, A18, XBOOLE_0:def 5;
C c= Ca by XBOOLE_1:7;
then C c< Ca by A20, A21;
hence contradiction by A19, A7; :: thesis:

end;

then consider S being non empty finite Subset of P such that
A22: S₃[S,Ca] ;
take S ; :: thesis:
take S ; :: thesis:
thus S = S ; :: thesis:

now :: thesis:

assume A23: not a in S ; :: thesis:
A24: S /\ C c= S /\ Ca

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in S /\ C ; :: thesis:
then ( x in S & x in C ) by XBOOLE_0:def 4;
then ( x in S & x in Ca ) by XBOOLE_0:def 3;
hence x in S /\ Ca by XBOOLE_0:def 4; :: thesis:

end;

S /\ Ca c= S /\ C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A25: x in S /\ Ca ; :: thesis:
then A26: x in S by XBOOLE_0:def 4;
x in Ca by A25, XBOOLE_0:def 4;
then ( x in C or x in {a} ) by XBOOLE_0:def 3;
hence x in S /\ C by A26, A23, TARSKI:def 1, XBOOLE_0:def 4; :: thesis:

end;

then A27: S /\ C = S /\ Ca by A24;
consider p being Clique-partition of (subrelstr S) such that
A28: card p <= stability# P and
A29: not S₂[S,p,C] by A6;
consider c being set such that
A30: c in p and
A31: S /\ C c= c and
A32: for d being set st d in p & d <> c holds
C /\ d = {} by A29;
for d being set st d in p & d <> c holds
Ca /\ d = {}

proof

let d be set ; :: thesis:
assume that
A33: d in p and
A34: d <> c ; :: thesis:

now :: thesis:

assume Ca /\ d <> {} ; :: thesis:
then consider x being object such that
A35: x in Ca /\ d by XBOOLE_0:def 1;
A36: x in Ca by A35, XBOOLE_0:def 4;
A37: x in d by A35, XBOOLE_0:def 4;

per cases by A36, XBOOLE_0:def 3;

suppose x in C ; :: thesis:

then x in C /\ d by A37, XBOOLE_0:def 4;
hence contradiction by A33, A34, A32; :: thesis:

end;

suppose x in {a} ; :: thesis:

then x = a by TARSKI:def 1;
then a in the carrier of (subrelstr S) by A37, A33;
hence contradiction by A23, YELLOW_0:def 15; :: thesis:

end;

hence Ca /\ d = {} ; :: thesis:

end;

hence contradiction by A30, A31, A28, A27, A22; :: thesis:

end;

hence a in S ; :: thesis:
thus S₃[S,C \/ {a}] by A22; :: thesis:

end;

consider f being Function such that
A38: dom f = A and
A39: for x being object st x in A holds
S₄[x,f . x] from CLASSES1:sch 1(A17);
A40: rng f is finite by A38, FINSET_1:8;
set SS = union (rng f);
A41: for x being set st x in rng f holds
x is finite

proof

let x be set ; :: thesis:
assume x in rng f ; :: thesis:
then consider a being object such that
A42: a in dom f and
A43: x = f . a by FUNCT_1:def 3;
S₄[a,f . a] by A38, A42, A39;
then consider S being non empty finite Subset of P such that
A44: f . a = S and
( a in f . a & S₃[S,C \/ {a}] ) ;
thus x is finite by A44, A43; :: thesis:

end;

A45: union (rng f) c= the carrier of P

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union (rng f) ; :: thesis:
then consider y being set such that
A46: x in y and
A47: y in rng f by TARSKI:def 4;
consider a being object such that
A48: a in dom f and
A49: y = f . a by A47, FUNCT_1:def 3;
S₄[a,f . a] by A38, A48, A39;
then consider S being non empty finite Subset of P such that
A50: f . a = S and
( a in f . a & S₃[S,C \/ {a}] ) ;
thus x in the carrier of P by A46, A49, A50; :: thesis:

end;

A51: A9 c= union (rng f)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A52: x in A9 ; :: thesis:
then S₄[x,f . x] by A39;
then consider S being non empty finite Subset of P such that
f . x = S and
A53: x in f . x and
S₃[S,C \/ {x}] ;
f . x in rng f by A52, A38, FUNCT_1:3;
hence x in union (rng f) by A53, TARSKI:def 4; :: thesis:

end;

then reconsider SS = union (rng f) as non empty finite Subset of P by A41, A40, A45, FINSET_1:7;
set SSp = subrelstr SS;
A54: SS = the carrier of (subrelstr SS) by YELLOW_0:def 15;
consider p being Clique-partition of (subrelstr SS) such that
A55: card p <= stability# P and
A56: not S₂[SS,p,C] by A6;
consider c being set such that
A57: c in p and
A58: SS /\ C c= c and
A59: for d being set st d in p & d <> c holds
C /\ d = {} by A56;
reconsider c = c as Element of p by A57;
A9 = A9 /\ SS by A51, XBOOLE_1:28;
then reconsider A = A9 as non empty finite StableSet of (subrelstr SS) by Th31;
A60: stability# (subrelstr SS) >= card A by Def6;
card p >= stability# (subrelstr SS) by Th46;
then card p >= card A by A60, XXREAL_0:2;
then consider a being Element of A such that
A61: c /\ A = {a} by Th48, A55, A16, A15, A5, XXREAL_0:1;
a in c /\ A by A61, TARSKI:def 1;
then A62: a in c by XBOOLE_0:def 4;
S₄[a,f . a] by A39;
then consider S being non empty finite Subset of P such that
A63: f . a = S and
A64: a in f . a and
A65: S₃[S,C \/ {a}] ;
deffunc H₁( set ) -> Element of bool the carrier of P = $1 /\ S;
defpred S₅[ set ] means $1 meets S;
set Sp = { H₁(e) where e is Element of p : S₅[e] } ;
A66: S c= SS

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A67: x in S ; :: thesis:
S in rng f by A63, A38, FUNCT_1:3;
hence x in SS by A67, TARSKI:def 4; :: thesis:

end;

then reconsider Sp = { H₁(e) where e is Element of p : S₅[e] } as a_partition of S by A54, PUA2MSS1:11;
for x being set st x in Sp holds
x is Clique of (subrelstr S)

proof

let x be set ; :: thesis:
assume x in Sp ; :: thesis:
then consider e being Element of p such that
A68: x = e /\ S and
e meets S ;
e is Clique of (subrelstr SS) by Def11;
then e is Clique of P by Th28;
hence x is Clique of (subrelstr S) by A68, Th29; :: thesis:

end;

then reconsider Sp = Sp as Clique-partition of (subrelstr S) by Def11, YELLOW_0:def 15;
A69: Sp = { H₁(e) where e is Element of p : S₅[e] } ;
A70: card Sp <= card p from DILWORTH:sch 1(A69);
set cc = c /\ S;
c meets S by A62, A63, A64, XBOOLE_0:3;
then A71: c /\ S in Sp ;
S /\ (C \/ {a}) c= c /\ S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A72: x in S /\ (C \/ {a}) ; :: thesis:
then A73: x in S by XBOOLE_0:def 4;
A74: x in C \/ {a} by A72, XBOOLE_0:def 4;

per cases by A74, XBOOLE_0:def 3;

suppose x in C ; :: thesis:

then x in SS /\ C by A73, A66, XBOOLE_0:def 4;
hence x in c /\ S by A73, A58, XBOOLE_0:def 4; :: thesis:

end;

suppose x in {a} ; :: thesis:

then x = a by TARSKI:def 1;
hence x in c /\ S by A62, A63, A64, XBOOLE_0:def 4; :: thesis:

end;

then consider d being set such that
A75: d in Sp and
A76: d <> c /\ S and
A77: (C \/ {a}) /\ d <> {} by A71, A70, A55, A65, XXREAL_0:2;
consider dd being Element of p such that
A78: d = dd /\ S and
dd meets S by A75;
C /\ dd = {} by A78, A76, A59;
then A79: C /\ d = {} /\ S by A78, XBOOLE_1:16
.= {} ;
(C /\ d) \/ ({a} /\ d) <> {} by A77, XBOOLE_1:23;
then consider x being object such that
A80: x in {a} /\ d by A79, XBOOLE_0:def 1;
( x in {a} & x in d ) by A80, XBOOLE_0:def 4;
then a in d by TARSKI:def 1;
then a in dd by A78, XBOOLE_0:def 4;
then c meets dd by A62, XBOOLE_0:3;
hence contradiction by A78, A76, EQREL_1:def 4; :: thesis:

end;

then stability# P9 < k + 1 by A13, XXREAL_0:1;
then A81: stability# P9 <= k by NAT_1:13;
consider A being finite StableSet of P such that
A82: card A = stability# P by Def6;
A83: stability# P9 = k

proof

per cases ;

suppose A84: A /\ C = {} ; :: thesis:

A c= cP9

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A85: x in A ; :: thesis:
then not x in C by A84, XBOOLE_0:def 4;
hence x in cP9 by A85, XBOOLE_0:def 5; :: thesis:

end;

hence stability# P9 = k by A5, A14, A82, Th45; :: thesis:

end;

suppose A /\ C <> {} ; :: thesis:

then consider x being object such that
A86: x in A /\ C by XBOOLE_0:def 1;
A87: x in A by A86, XBOOLE_0:def 4;
A88: x in C by A86, XBOOLE_0:def 4;
set A9 = A \ {x};
{x} c= A by A87, ZFMISC_1:31;
then A89: A = (A \ {x}) \/ {x} by XBOOLE_1:45;
x in {x} by TARSKI:def 1;
then not x in A \ {x} by XBOOLE_0:def 5;
then A90: card A = (card (A \ {x})) + 1 by A89, CARD_2:41;
A91: A \ {x} c= A by XBOOLE_1:36;
A \ {x} c= cP9

proof

let xx be object ; :: according to TARSKI:def 3 :: thesis:
assume A92: xx in A \ {x} ; :: thesis:
then A93: xx in A by XBOOLE_0:def 5;
not xx in {x} by A92, XBOOLE_0:def 5;
then xx <> x by TARSKI:def 1;
then not xx in C by A87, A88, A93, A6, Th15;
hence xx in cP9 by A92, XBOOLE_0:def 5; :: thesis:

end;

then A94: A \ {x} c= A /\ cP9 by A91, XBOOLE_1:19;
A /\ cP9 c= A \ {x}

proof

let xx be object ; :: according to TARSKI:def 3 :: thesis:
assume A95: xx in A /\ cP9 ; :: thesis:
then A96: xx in A by XBOOLE_0:def 4;
xx in cP9 by A95, XBOOLE_0:def 4;
then x <> xx by A88, XBOOLE_0:def 5;
then not xx in {x} by TARSKI:def 1;
hence xx in A \ {x} by A96, XBOOLE_0:def 5; :: thesis:

end;

then A \ {x} = A /\ cP9 by A94;
then reconsider A9 = A \ {x} as StableSet of P9 by Th31;
stability# P9 >= card A9 by Def6;
hence stability# P9 = k by A90, A82, A5, A81, XXREAL_0:1; :: thesis:

end;

then consider Cp9 being Clique-partition of P9 such that
A97: card Cp9 = stability# P9 by A4;
set Cp = Cp9 \/ {( the carrier of P \ cP9)};
A98: Cp9 is finite by A97;
cP9 <> the carrier of P by A11, XBOOLE_1:37;
then A99: cP9 c< the carrier of P ;
then reconsider Cp = Cp9 \/ {( the carrier of P \ cP9)} as a_partition of the carrier of P by A12, Th4;

now :: thesis:

let x be set ; :: thesis:
assume A100: x in Cp ; :: thesis:

per cases by A100, XBOOLE_0:def 3;

suppose x in Cp9 ; :: thesis:

then x is Clique of P9 by Def11;
hence x is Clique of P by Th28; :: thesis:

end;

suppose x in {( the carrier of P \ cP9)} ; :: thesis:

hence x is Clique of P by A6, A11, TARSKI:def 1; :: thesis:

end;

then reconsider Cp = Cp as Clique-partition of P by Def11;
take Cp ; :: thesis:
not the carrier of P \ cP9 in Cp9

proof

assume the carrier of P \ cP9 in Cp9 ; :: thesis:
then the carrier of P c= cP9 \/ cP9 by A12, XBOOLE_1:44;
hence contradiction by A99, XBOOLE_1:60; :: thesis:

end;

hence card Cp = stability# P by A5, A83, A97, A98, CARD_2:41; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence ex C being Clique-partition of R st card C = stability# R by A1; :: thesis:

end;