defpred S₁[ Nat] means for P being finite transitive antisymmetric RelStr st card P = $1 holds
ex C being Clique-partition of P st card C = stability# P;
P: for n being Nat st ( for k being Nat st k < n holds
S₁[k] ) holds
S₁[n]

proof

let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S₁[k] ) implies S₁[n] )
assume A1: for k being Nat st k < n holds
S₁[k] ; :: thesis: S₁[n]
let P be finite transitive antisymmetric RelStr ; :: thesis: ( card P = n implies ex C being Clique-partition of P st card C = stability# P )
assume B1: card P = n ; :: thesis: ex C being Clique-partition of P st card C = stability# P
set wP = stability# P;

per cases ( n = 0 or n > 0 ) ;

suppose S1: n = 0 ; :: thesis: ex C being Clique-partition of P st card C = stability# P

then P is empty by B1;
then reconsider C = {} as Clique-partition of P by EQREL_1:54;
take C ; :: thesis: card C = stability# P
P is empty by B1, S1;
hence card C = stability# P by B1, S1; :: thesis: verum

end;

suppose S1: n > 0 ; :: thesis: ex C being Clique-partition of P st card C = stability# P

per cases ( ex A being StableSet of P st
( card A = stability# P & A <> minimals P & A <> maximals P ) or for A being StableSet of P holds
( not card A = stability# P or A = minimals P or A = maximals P ) ) ;

suppose ex A being StableSet of P st
( card A = stability# P & A <> minimals P & A <> maximals P ) ; :: thesis: ex C being Clique-partition of P st card C = stability# P

then consider A being StableSet of P such that
S2a: card A = stability# P and
S2b: A <> minimals P and
S2c: A <> maximals P ;
set aA = Upper A;
set bA = Lower A;
set cP = the carrier of P;
set Pa = subrelstr (Upper A);
set Pb = subrelstr (Lower A);
reconsider PP = P as non empty finite transitive antisymmetric RelStr by S1, B1;
S2d: Upper A = the carrier of (subrelstr (Upper A)) by YELLOW_0:def 15;
S2e: Lower A = the carrier of (subrelstr (Lower A)) by YELLOW_0:def 15;
not minimals PP c= Upper A by S2b, PCAmin, PCAamin;
then consider mi being set such that
A2a: mi in minimals P and
A2b: not mi in Upper A by TARSKI:def 3;
not maximals PP c= Lower A by S2c, PCAmax, PCAbmax;
then consider ma being set such that
B2a: ma in maximals P and
B2b: not ma in Lower A by TARSKI:def 3;
reconsider Pa = subrelstr (Upper A) as finite transitive antisymmetric RelStr ;
mi in the carrier of P by A2a;
then Upper A c< the carrier of P by A2b, XBOOLE_0:def 8;
then card Pa < card P by S2d, CARD_2:67;
then consider Ca being Clique-partition of Pa such that
C2a: card Ca = stability# Pa by A1, B1;
C2b: stability# Pa = stability# P by S2a, Wsubp1, XBOOLE_1:7;
reconsider Pb = subrelstr (Lower A) as finite transitive antisymmetric RelStr ;
ma in the carrier of P by B2a;
then Lower A c< the carrier of P by B2b, XBOOLE_0:def 8;
then card Pb < card P by S2e, CARD_2:67;
then consider L being Clique-partition of Pb such that
D2a: card L = stability# Pb by A1, B1;
stability# Pb = stability# P by S2a, Wsubp1, XBOOLE_1:7;
then consider C being Clique-partition of P such that
Z: card C = stability# PP by S2a, C2a, C2b, D2a, Main;
take C ; :: thesis: card C = stability# P
thus card C = stability# P by Z; :: thesis: verum

end;

suppose S2: for A being StableSet of P holds
( not card A = stability# P or A = minimals P or A = maximals P ) ; :: thesis: ex C being Clique-partition of P st card C = stability# P

consider S being StableSet of P such that
B2: card S = stability# P by Lwidth;
reconsider PP = P as non empty finite transitive antisymmetric RelStr by S1, B1;
set cR = the carrier of PP;
consider a being Element of minimals P;
D2a: a in minimals PP ;
then reconsider a = a as Element of PP ;
consider b being Element of PP such that
F2: b is_maximal_in [#] PP and
G2: ( a = b or a < b ) by Pminmax;
F2a: b in maximals P by F2, Lmax;
set cP = the carrier of P;
set Cn = {a,b};
set cP9 = the carrier of P \ {a,b};
G2a: the carrier of P = ( the carrier of P \ {a,b}) \/ {a,b} by XBOOLE_1:45;
G2b: the carrier of P \ {a,b} misses {a,b} by XBOOLE_1:79;
then G2c: the carrier of P \ ( the carrier of P \ {a,b}) = {a,b} by G2a, XBOOLE_1:88;
reconsider cP9 = the carrier of P \ {a,b} as Subset of the carrier of PP ;
set P9 = subrelstr cP9;
H2a: cP9 = the carrier of (subrelstr cP9) by YELLOW_0:def 15;
H2: card cP9 = card (subrelstr cP9) by YELLOW_0:def 15;
card cP9 = (card the carrier of P) - (card {a,b}) by CARD_2:63;
then consider C being Clique-partition of (subrelstr cP9) such that
I2: card C = stability# (subrelstr cP9) by A1, B1, H2, XREAL_1:46;
I2a: not {a,b} in C

proof

assume A3: {a,b} in C ; :: thesis: contradiction
a in {a,b} by TARSKI:def 2;
hence contradiction by G2b, ZFMISC_1:55, H2a, A3; :: thesis: verum

end;

set wP = stability# PP;
set wP1 = (stability# PP) - 1;
0 + 1 <= stability# PP by NAT_1:13;
then (0 + 1) - 1 <= (stability# PP) - 1 by XREAL_1:11;
then (stability# PP) - 1 in NAT by INT_1:16;
then reconsider wP1 = (stability# PP) - 1 as Nat ;
set S9 = S /\ cP9;
S /\ the carrier of P = S by XBOOLE_1:28;
then J2aa: S /\ cP9 = S \ {a,b} by XBOOLE_1:49;
J2ab: {a,b} = {a} \/ {b} by ENUMSET1:41;
reconsider S9 = S /\ cP9 as StableSet of (subrelstr cP9) by SPAChain;
J2a: card S9 = wP1

proof

per cases ( S = minimals P or S = maximals PP ) by S2, B2;

suppose S3: S = minimals P ; :: thesis: card S9 = wP1

S9 = S \ {a}

proof

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: S9 = S \ {a}

hence S9 = S \ {a} by J2aa, ENUMSET1:69; :: thesis: verum

end;

suppose A5aa: a <> b ; :: thesis: S9 = S \ {a}

now

assume b in minimals PP ; :: thesis: contradiction
then b is_minimal_in [#] PP by Lmin;
hence contradiction by A5aa, G2, WAYBEL_4:57; :: thesis: verum

end;

hence S9 = S \ {a} by J2aa, J2ab, S3, set00; :: thesis: verum

end;

end;

end;

hence card S9 = (card S) - (card {a}) by S3, EULER_1:5
.= wP1 by B2, CARD_1:50 ;
:: thesis: verum

end;

suppose S3: S = maximals PP ; :: thesis: card S9 = wP1

A4: S9 = S \ {b}

proof

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: S9 = S \ {b}

hence S9 = S \ {b} by J2aa, ENUMSET1:69; :: thesis: verum

end;

suppose A5aa: a <> b ; :: thesis: S9 = S \ {b}

now

assume a in maximals PP ; :: thesis: contradiction
then a is_maximal_in [#] PP by Lmax;
hence contradiction by A5aa, G2, WAYBEL_4:56; :: thesis: verum

end;

hence S9 = S \ {b} by J2aa, J2ab, S3, set00; :: thesis: verum

end;

end;

end;

b in S by S3, F2, Lmax;
hence card S9 = (card S) - (card {b}) by A4, EULER_1:5
.= wP1 by B2, CARD_1:50 ;
:: thesis: verum

end;

end;

end;

for T being StableSet of (subrelstr cP9) holds card T <= card S9

proof

let T be StableSet of (subrelstr cP9); :: thesis: card T <= card S9
assume card T > card S9 ; :: thesis: contradiction
then card T >= (card S9) + 1 by NAT_1:13;
then consider V being StableSet of (subrelstr cP9) such that
B3: card V = (card S9) + 1 by AChain1;
V is StableSet of P by SPAChain1;
then ( V = minimals P or V = maximals P ) by S2, B3, J2a;
hence contradiction by D2a, F2a, H2a, G2b, ZFMISC_1:55; :: thesis: verum

end;

then J2c: (stability# (subrelstr cP9)) + 1 = ((stability# PP) - 1) + 1 by J2a, Lwidth
.= stability# PP ;
set CC = C \/ {{a,b}};
cP9 <> the carrier of P by G2c, XBOOLE_1:37;
then x: cP9 c< the carrier of P by XBOOLE_0:def 8;

now

let x be set ; :: thesis: ( x in C \/ {{a,b}} implies b₁ is Clique of P )
assume A3: x in C \/ {{a,b}} ; :: thesis: b₁ is Clique of P

per cases ( x in C or x in {{a,b}} ) by A3, XBOOLE_0:def 3;

suppose x in C ; :: thesis: b₁ is Clique of P

then x is Clique of (subrelstr cP9) by LCpart;
hence x is Clique of P by SPClique; :: thesis: verum

end;

suppose x in {{a,b}} ; :: thesis: b₁ is Clique of P

then A4: x = {a,b} by TARSKI:def 1;

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: b₁ is Clique of P

then x = {a} by A4, ENUMSET1:69;
hence x is Clique of P ; :: thesis: verum

end;

suppose a <> b ; :: thesis: b₁ is Clique of P

then a <= b by G2, ORDERS_2:def 10;
hence x is Clique of P by A4, Clique36b; :: thesis: verum

end;

end;

end;

end;

end;

then reconsider CC = C \/ {{a,b}} as Clique-partition of P by G2c, H2a, SPpart, LCpart, x;
take CC ; :: thesis: card CC = stability# P
thus card CC = stability# P by I2, J2c, I2a, CARD_2:54; :: thesis: verum

end;

end;

end;

end;

end;

Z: for n being Nat holds S₁[n] from NAT_1:sch 4(P);
let R be finite transitive antisymmetric RelStr ; :: thesis: ex C being Clique-partition of R st card C = stability# R
card R = card R ;
hence ex C being Clique-partition of R st card C = stability# R by Z; :: thesis: verum