let R be transitive antisymmetric with_finite_clique# RelStr ; :: thesis:
defpred S₁[ Nat] means for P being transitive antisymmetric with_finite_clique# RelStr st clique# P = $1 holds
ex A being Coloring of P st card A = clique# P;
P1: S₁[ 0 ]

proof

let P be transitive antisymmetric with_finite_clique# RelStr ; :: thesis:
assume S1a: clique# P = 0 ; :: thesis:
then P is empty ;
then reconsider C = {} as Coloring of P by EQREL_1:54;
take C ; :: thesis:
thus card C = clique# P by S1a; :: thesis:

end;

P2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume AA: S₁[n] ; :: thesis:
let P be transitive antisymmetric with_finite_clique# RelStr ; :: thesis:
assume A1: clique# P = n + 1 ; :: thesis:
then A1a: not P is empty ;
reconsider PP = P as non empty transitive antisymmetric with_finite_clique# RelStr by A1;
set M = maximals PP;
set cP = the carrier of P;
set cPM = the carrier of P \ (maximals PP);
reconsider cPM = the carrier of P \ (maximals PP) as Subset of P ;
set PM = subrelstr cPM;
cPM: cPM = the carrier of (subrelstr cPM) by YELLOW_0:def 15;
reconsider PM = subrelstr cPM as transitive antisymmetric with_finite_clique# RelStr ;
consider Ca being finite Clique of PM such that
B1a: card Ca = clique# PM by Lheight;
C1b: Ca is Clique of P by SPClique;
consider C being finite Clique of P such that
B1: card C = n + 1 by A1, Lheight;
B1b: C <> {} by B1;
set cC = C /\ cPM;
reconsider cC = C /\ cPM as finite Clique of PM by SPClique1;
consider m being Element of P such that
F1: m in C and
G1: m is_maximal_wrt C,the InternalRel of P by A1a, B1b, BAGORDER:7;
G1a: m is_maximal_in C by G1, WAYBEL_4:def 25;
H1: C /\ (maximals PP) = {m}

proof

thus C /\ (maximals PP) c= {m} :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A2: a in C /\ (maximals PP) ; :: thesis:
then B2: a in C by XBOOLE_0:def 4;
C2: a in maximals PP by A2, XBOOLE_0:def 4;
reconsider a9 = a as Element of P by A2;
D2: a9 is_maximal_in [#] P by C2, Lmax;

now

assume A3: a <> m ; :: thesis:
not m < a9 by B2, G1a, WAYBEL_4:56;
then not m <= a9 by A3, ORDERS_2:def 10;
then a9 <= m by F1, B2, A3, DClique;
then a9 < m by A3, ORDERS_2:def 10;
hence contradiction by D2, F1, WAYBEL_4:56; :: thesis:

end;

hence a in {m} by TARSKI:def 1; :: thesis:

end;

thus {m} c= C /\ (maximals PP) :: thesis:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in {m} ; :: thesis:
then A2: a = m by TARSKI:def 1;

now

assume A3: not a in maximals PP ; :: thesis:
consider y being Element of P such that
B3: y is_maximal_in [#] P and
C3: ( m = y or m < y ) by A1a, Pminmax;
set Cm = C \/ {y};

now

per cases ;

suppose m = y ; :: thesis:

hence C \/ {y} is finite Clique of P by F1, ZFMISC_1:46; :: thesis:

end;

suppose m <> y ; :: thesis:

then m <= y by C3, ORDERS_2:def 10;
hence C \/ {y} is finite Clique of P by G1a, ExtClique; :: thesis:

end;

then reconsider Cm = C \/ {y} as finite Clique of P ;
not y in C by A2, A3, B3, Lmax, C3, G1a, WAYBEL_4:56;
then card Cm = (card C) + 1 by CARD_2:54;
then (n + 1) + 1 <= (n + 1) + 0 by B1, A1, Lheight;
hence contradiction by XREAL_1:8; :: thesis:

end;

hence a in C /\ (maximals PP) by A2, F1, XBOOLE_0:def 4; :: thesis:

end;

D1b: cC = (C /\ the carrier of P) \ (C /\ (maximals PP)) by XBOOLE_1:50;
C /\ the carrier of P = C by XBOOLE_1:28;
then D1: card cC = (card C) - (card {m}) by F1, H1, D1b, EULER_1:5
.= (n + 1) - 1 by B1, CARD_1:50
.= n ;
D1a: clique# PM >= card cC by Lheight;
E1: clique# PM <= clique# P by Hsubp0;

now

assume A2: clique# PM = n + 1 ; :: thesis:
then B2: Ca <> {} by B1a;
B2a: not PM is empty by A2;
then consider x being Element of PM such that
D2e: x in Ca and
D2: x is_maximal_wrt Ca,the InternalRel of PM by B2, BAGORDER:7;
D2a: x is_maximal_in Ca by D2, WAYBEL_4:def 25;
reconsider x9 = x as Element of P by B2a, YELLOW_0:59;
consider y being Element of P such that
E2: y is_maximal_in [#] P and
F2: ( x9 = y or x9 < y ) by Pminmax;
set Cb = Ca \/ {y};

now

per cases ;

suppose x9 = y ; :: thesis:

hence Ca \/ {y} is finite Clique of P by D2e, C1b, ZFMISC_1:46; :: thesis:

end;

suppose x9 <> y ; :: thesis:

then x9 <= y by F2, ORDERS_2:def 10;
hence Ca \/ {y} is finite Clique of P by D2a, SPmax, C1b, ExtClique; :: thesis:

end;

then reconsider Cb = Ca \/ {y} as finite Clique of P ;
y in maximals PP by E2, Lmax;
then not y in Ca by cPM, XBOOLE_0:def 5;
then G2: card Cb = (n + 1) + 1 by B1a, A2, CARD_2:54;
card Cb <= n + 1 by A1, Lheight;
then n + 1 <= n + 0 by G2, XREAL_1:8;
hence contradiction by XREAL_1:8; :: thesis:

end;

then clique# PM < n + 1 by A1, E1, XXREAL_0:1;
then clique# PM <= n by NAT_1:13;
then clique# PM = n by D1, D1a, XXREAL_0:1;
then consider Aa being Coloring of PM such that
K1: card Aa = n by AA;
reconsider Ab = Aa as finite set by K1;
set A = Aa \/ {(maximals PP)};
L1b: the carrier of P = cPM \/ (maximals PP) by XBOOLE_1:45;
{(maximals PP)} is a_partition of maximals PP by EQREL_1:48;
then L1: Aa \/ {(maximals PP)} is a_partition of the carrier of P by XBOOLE_1:79, L1b, cPM, SPpart0;

now

let x be set ; :: thesis:
assume A2: x in Aa \/ {(maximals PP)} ; :: thesis:

per cases by A2, XBOOLE_0:def 3;

suppose x in Aa ; :: thesis:

then x is StableSet of PM by LACpart;
hence x is StableSet of P by SPAChain1; :: thesis:

end;

suppose x in {(maximals PP)} ; :: thesis:

hence x is StableSet of P by TARSKI:def 1; :: thesis:

end;

then reconsider A = Aa \/ {(maximals PP)} as Coloring of P by L1, LACpart;
take A ; :: thesis:
not maximals PP in Ab by cPM, XBOOLE_1:38;
hence card A = clique# P by A1, K1, CARD_2:54; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P1, P2);
hence ex A being Coloring of R st card A = clique# R ; :: thesis: