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;
P:
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 A1:
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 B1:
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 S1:
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 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
;
card C = stability# Pthus
card C = stability# P
by Z;
verum end; suppose S2:
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 B2:
card S = stability# P
by Lwidth;
reconsider PP =
P as non
empty finite transitive antisymmetric RelStr by S1, B1;
set iR = the
InternalRel of
PP;
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 cPP = the
carrier of
PP;
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;
set k =
card (subrelstr cP9);
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
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
for
T being
StableSet of
(subrelstr cP9) holds
card T <= card S9
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;
then reconsider CC =
C \/ {{a,b}} as
Clique-partition of
P by G2c, H2a, SPpart, LCpart, x;
take
CC
;
card CC = stability# Pthus
card CC = stability# P
by I2, J2c, I2a, CARD_2:54;
verum end;
end;
Z:
for n being Nat holds S1[n]
from NAT_1:sch 4(P);
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 Z; verum