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;
A1: S₁[ 0 ]

proof

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

end;

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

proof

let n be Nat; :: thesis:
assume A4: S₁[n] ; :: thesis:
let P be transitive antisymmetric with_finite_clique# RelStr ; :: thesis:
assume A5: clique# P = n + 1 ; :: thesis:
then A6: not P is empty ;
reconsider PP = P as non empty transitive antisymmetric with_finite_clique# RelStr by A5;
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;
A7: 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
A8: card Ca = clique# PM by Def4;
A9: Ca is Clique of P by Th28;
consider C being finite Clique of P such that
A10: card C = n + 1 by A5, Def4;
A11: C <> {} by A10;
set cC = C /\ cPM;
reconsider cC = C /\ cPM as finite Clique of PM by Th29;
consider m being Element of P such that
A12: m in C and
A13: m is_maximal_wrt C, the InternalRel of P by A6, A11, BAGORDER:6;
A14: m is_maximal_in C by A13, WAYBEL_4:def 24;
A15: C /\ (maximals PP) = {m}

proof

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A16: a in C /\ (maximals PP) ; :: thesis:
then A17: a in C by XBOOLE_0:def 4;
A18: a in maximals PP by A16, XBOOLE_0:def 4;
reconsider a9 = a as Element of P by A16;
A19: a9 is_maximal_in [#] P by A18, Def10;

now :: thesis:

assume A20: a <> m ; :: thesis:
not m < a9 by A17, A14, WAYBEL_4:55;
then not m <= a9 by A20;
then a9 <= m by A12, A17, A20, Th6;
then a9 < m by A20;
hence contradiction by A19, A12, WAYBEL_4:55; :: thesis:

end;

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

end;

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

proof

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

now :: thesis:

assume A22: not a in maximals PP ; :: thesis:
consider y being Element of P such that
A23: y is_maximal_in [#] P and
A24: ( m = y or m < y ) by A6, Th38;
set Cm = C \/ {y};

now :: thesis:

per cases ;

suppose m = y ; :: thesis:

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

end;

suppose m <> y ; :: thesis:

then m <= y by A24;
hence C \/ {y} is finite Clique of P by A14, Th11; :: thesis:

end;

then reconsider Cm = C \/ {y} as finite Clique of P ;
not y in C by A21, A22, A23, Def10, A24, A14, WAYBEL_4:55;
then card Cm = (card C) + 1 by CARD_2:41;
then (n + 1) + 1 <= (n + 1) + 0 by A10, A5, Def4;
hence contradiction by XREAL_1:6; :: thesis:

end;

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

end;

A25: cC = (C /\ the carrier of P) \ (C /\ (maximals PP)) by XBOOLE_1:50;
C /\ the carrier of P = C by XBOOLE_1:28;
then A26: card cC = (card C) - (card {m}) by A12, A15, A25, EULER_1:4
.= (n + 1) - 1 by A10, CARD_1:30
.= n ;
A27: clique# PM >= card cC by Def4;
A28: clique# PM <= clique# P by Th42;

now :: thesis:

assume A29: clique# PM = n + 1 ; :: thesis:
then A30: Ca <> {} by A8;
A31: not PM is empty by A29;
then consider x being Element of PM such that
A32: x in Ca and
A33: x is_maximal_wrt Ca, the InternalRel of PM by A30, BAGORDER:6;
A34: x is_maximal_in Ca by A33, WAYBEL_4:def 24;
reconsider x9 = x as Element of P by A31, YELLOW_0:58;
consider y being Element of P such that
A35: y is_maximal_in [#] P and
A36: ( x9 = y or x9 < y ) by Th38;
set Cb = Ca \/ {y};

now :: thesis:

per cases ;

suppose x9 = y ; :: thesis:

hence Ca \/ {y} is finite Clique of P by A32, A9, ZFMISC_1:40; :: thesis:

end;

suppose x9 <> y ; :: thesis:

then x9 <= y by A36;
hence Ca \/ {y} is finite Clique of P by A34, Th32, A9, Th11; :: thesis:

end;

then reconsider Cb = Ca \/ {y} as finite Clique of P ;
y in maximals PP by A35, Def10;
then not y in Ca by A7, XBOOLE_0:def 5;
then A37: card Cb = (n + 1) + 1 by A8, A29, CARD_2:41;
card Cb <= n + 1 by A5, Def4;
then n + 1 <= n + 0 by A37, XREAL_1:6;
hence contradiction by XREAL_1:6; :: thesis:

end;

then clique# PM < n + 1 by A5, A28, XXREAL_0:1;
then clique# PM <= n by NAT_1:13;
then clique# PM = n by A26, A27, XXREAL_0:1;
then consider Aa being Coloring of PM such that
A38: card Aa = n by A4;
reconsider Ab = Aa as finite set by A38;
set A = Aa \/ {(maximals PP)};
A39: the carrier of P = cPM \/ (maximals PP) by XBOOLE_1:45;
{(maximals PP)} is a_partition of maximals PP by EQREL_1:39;
then A40: Aa \/ {(maximals PP)} is a_partition of the carrier of P by A39, A7, Th3, XBOOLE_1:79;

now :: thesis:

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

per cases by A41, XBOOLE_0:def 3;

suppose x in Aa ; :: thesis:

then x is StableSet of PM by Def12;
hence x is StableSet of P by Th30; :: 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 A40, Def12;
take A ; :: thesis:
not maximals PP in Ab by A7, XBOOLE_1:38;
hence card A = clique# P by A5, A38, CARD_2:41; :: thesis:

end;

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