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;
A1: for n being Nat st ( for k being Nat st k < n holds
S₁[k] ) holds
S₁[n]

proof

let n be Nat; :: thesis:
assume A2: for k being Nat st k < n holds
S₁[k] ; :: thesis:
let P be finite transitive antisymmetric RelStr ; :: thesis:
assume A3: card P = n ; :: thesis:
set wP = stability# P;

per cases ;

suppose A4: n = 0 ; :: thesis:

then P is empty by A3;
then reconsider C = {} as Clique-partition of P by EQREL_1:45;
take C ; :: thesis:
P is empty by A3, A4;
hence card C = stability# P ; :: thesis:

end;

suppose A5: n > 0 ; :: thesis:

per cases ;

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

then consider A being StableSet of P such that
A6: card A = stability# P and
A7: A <> minimals P and
A8: 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 A5, A3;
A9: Upper A = the carrier of (subrelstr (Upper A)) by YELLOW_0:def 15;
A10: Lower A = the carrier of (subrelstr (Lower A)) by YELLOW_0:def 15;
not minimals PP c= Upper A by A7, Th40, Th26;
then consider mi being object such that
A11: mi in minimals P and
A12: not mi in Upper A ;
not maximals PP c= Lower A by A8, Th41, Th27;
then consider ma being object such that
A13: ma in maximals P and
A14: not ma in Lower A ;
reconsider Pa = subrelstr (Upper A) as finite transitive antisymmetric RelStr ;
mi in the carrier of P by A11;
then Upper A c< the carrier of P by A12;
then card Pa < card P by A9, CARD_2:48;
then consider Ca being Clique-partition of Pa such that
A15: card Ca = stability# Pa by A2, A3;
A16: stability# Pa = stability# P by A6, Th45, XBOOLE_1:7;
reconsider Pb = subrelstr (Lower A) as finite transitive antisymmetric RelStr ;
ma in the carrier of P by A13;
then Lower A c< the carrier of P by A14;
then card Pb < card P by A10, CARD_2:48;
then consider L being Clique-partition of Pb such that
A17: card L = stability# Pb by A2, A3;
stability# Pb = stability# P by A6, Th45, XBOOLE_1:7;
then consider C being Clique-partition of P such that
A18: card C = stability# PP by A6, A15, A16, A17, Th49;
take C ; :: thesis:
thus card C = stability# P by A18; :: thesis:

end;

suppose A19: for A being StableSet of P holds
( not card A = stability# P or A = minimals P or A = maximals P ) ; :: thesis:

consider S being StableSet of P such that
A20: card S = stability# P by Def6;
reconsider PP = P as non empty finite transitive antisymmetric RelStr by A5, A3;
set cR = the carrier of PP;
set a = the Element of minimals P;
A21: the Element of minimals P in minimals PP ;
then reconsider a = the Element of minimals P as Element of PP ;
consider b being Element of PP such that
A22: b is_maximal_in [#] PP and
A23: ( a = b or a < b ) by Th38;
A24: b in maximals P by A22, Def10;
set cP = the carrier of P;
set Cn = {a,b};
set cP9 = the carrier of P \ {a,b};
A25: the carrier of P = ( the carrier of P \ {a,b}) \/ {a,b} by XBOOLE_1:45;
A26: the carrier of P \ {a,b} misses {a,b} by XBOOLE_1:79;
then A27: the carrier of P \ ( the carrier of P \ {a,b}) = {a,b} by A25, XBOOLE_1:88;
reconsider cP9 = the carrier of P \ {a,b} as Subset of the carrier of PP ;
set P9 = subrelstr cP9;
A28: cP9 = the carrier of (subrelstr cP9) by YELLOW_0:def 15;
A29: card cP9 = card (subrelstr cP9) by YELLOW_0:def 15;
card cP9 = (card the carrier of P) - (card {a,b}) by CARD_2:44;
then consider C being Clique-partition of (subrelstr cP9) such that
A30: card C = stability# (subrelstr cP9) by A2, A3, A29, XREAL_1:44;
A31: not {a,b} in C

proof

assume A32: {a,b} in C ; :: thesis:
a in {a,b} by TARSKI:def 2;
hence contradiction by A26, A28, A32, ZFMISC_1:49; :: thesis:

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:9;
then (stability# PP) - 1 in NAT by INT_1:3;
then reconsider wP1 = (stability# PP) - 1 as Nat ;
set S9 = S /\ cP9;
S /\ the carrier of P = S by XBOOLE_1:28;
then A33: S /\ cP9 = S \ {a,b} by XBOOLE_1:49;
A34: {a,b} = {a} \/ {b} by ENUMSET1:1;
reconsider S9 = S /\ cP9 as StableSet of (subrelstr cP9) by Th31;
A35: card S9 = wP1

proof

per cases by A19, A20;

suppose A36: S = minimals P ; :: thesis:

S9 = S \ {a}

proof

per cases ;

suppose a = b ; :: thesis:

hence S9 = S \ {a} by A33, ENUMSET1:29; :: thesis:

end;

suppose A37: a <> b ; :: thesis:

now :: thesis:

assume b in minimals PP ; :: thesis:
then b is_minimal_in [#] PP by Def9;
hence contradiction by A37, A23, WAYBEL_4:56; :: thesis:

end;

hence S9 = S \ {a} by A33, A34, A36, Th1; :: thesis:

end;

hence card S9 = (card S) - (card {a}) by A36, EULER_1:4
.= wP1 by A20, CARD_1:30 ;
:: thesis:

end;

suppose A38: S = maximals PP ; :: thesis:

A39: S9 = S \ {b}

proof

per cases ;

suppose a = b ; :: thesis:

hence S9 = S \ {b} by A33, ENUMSET1:29; :: thesis:

end;

suppose A40: a <> b ; :: thesis:

now :: thesis:

assume a in maximals PP ; :: thesis:
then a is_maximal_in [#] PP by Def10;
hence contradiction by A40, A23, WAYBEL_4:55; :: thesis:

end;

hence S9 = S \ {b} by A33, A34, A38, Th1; :: thesis:

end;

b in S by A38, A22, Def10;
hence card S9 = (card S) - (card {b}) by A39, EULER_1:4
.= wP1 by A20, CARD_1:30 ;
:: thesis:

end;

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

proof

let T be StableSet of (subrelstr cP9); :: thesis:
assume card T > card S9 ; :: thesis:
then card T >= (card S9) + 1 by NAT_1:13;
then consider V being StableSet of (subrelstr cP9) such that
A41: card V = (card S9) + 1 by Th17;
V is StableSet of P by Th30;
then ( V = minimals P or V = maximals P ) by A19, A41, A35;
hence contradiction by A21, A24, A28, A26, ZFMISC_1:49; :: thesis:

end;

then A42: (stability# (subrelstr cP9)) + 1 = ((stability# PP) - 1) + 1 by A35, Def6
.= stability# PP ;
set CC = C \/ {{a,b}};
cP9 <> the carrier of P by A27, XBOOLE_1:37;
then A43: cP9 c< the carrier of P ;

now :: thesis:

let x be set ; :: thesis:
assume A44: x in C \/ {{a,b}} ; :: thesis:

per cases by A44, XBOOLE_0:def 3;

suppose x in C ; :: thesis:

then x is Clique of (subrelstr cP9) by Def11;
hence x is Clique of P by Th28; :: thesis:

end;

suppose x in {{a,b}} ; :: thesis:

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

per cases ;

suppose a = b ; :: thesis:

then x = {a} by A45, ENUMSET1:29;
hence x is Clique of P ; :: thesis:

end;

suppose a <> b ; :: thesis:

then a <= b by A23;
hence x is Clique of P by A45, Th8; :: thesis:

end;

then reconsider CC = C \/ {{a,b}} as Clique-partition of P by A27, A28, Th4, Def11, A43;
take CC ; :: thesis:
thus card CC = stability# P by A30, A42, A31, CARD_2:41; :: thesis:

end;

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