defpred S1[ 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
S1[k] ) holds
S1[n]
proof
let n be
Nat;
( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A2:
for
k being
Nat st
k < n holds
S1[
k]
;
S1[n]
let P be
finite transitive antisymmetric RelStr ;
( card P = n implies ex C being Clique-partition of P st card C = stability# P )
assume A3:
card P = n
;
ex C being Clique-partition of P st card C = stability# P
set wP =
stability# P;
per cases
( n = 0 or n > 0 )
;
suppose A5:
n > 0
;
ex C being Clique-partition of P st card C = stability# Pper 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 )
;
ex C being Clique-partition of P st card C = stability# Pthen 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
;
card C = stability# Pthus
card C = stability# P
by A18;
verum end; suppose A19:
for
A being
StableSet of
P holds
( not
card A = stability# P or
A = minimals P or
A = maximals P )
;
ex C being Clique-partition of P st card C = stability# Pconsider 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
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
for
T being
StableSet of
(subrelstr cP9) holds
card T <= card S9
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
;
then reconsider CC =
C \/ {{a,b}} as
Clique-partition of
P by A27, A28, Th4, Def11, A43;
take
CC
;
card CC = stability# Pthus
card CC = stability# P
by A30, A42, A31, CARD_2:41;
verum end; end; end; end;
end;
A46:
for n being Nat holds S1[n]
from NAT_1:sch 4(A1);
let R be finite transitive antisymmetric RelStr ; 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 A46; verum