:: Dilworth's Decomposition Theorem for Posets
:: by Piotr Rudnicki
::
:: Received September 17, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users


begin

:: Facts that I could not find in MML.
scheme :: DILWORTH:sch 1
FraenkelFinCard1{ F1() ->  non empty finite set , P1[ set ], F2() ->  finite set , F3( set ) ->  set } :
 card F2() <= card F1()
provided
A1: F2() =  {  F3(w) where w is Element of F1() : P1[w]  }
proofend;

theorem Th1: :: DILWORTH:1
for X, Y, x being set st not x in X holds
X \ (Y \/ {x}) = X \ Y
proofend;

theorem Th2: :: DILWORTH:2
for X, Y being set
for F being Subset-Family of X
for G being Subset-Family of Y holds F \/ G is Subset-Family of (X \/ Y)
proofend;

theorem Th3: :: DILWORTH:3
for X, Y being set
for F being a_partition of X
for G being a_partition of Y st X misses Y holds
F \/ G is a_partition of X \/ Y
proofend;

theorem Th4: :: DILWORTH:4
for X, Y being set
for F being a_partition of Y st Y c< X holds
F \/ {(X \ Y)} is a_partition of X
proofend;

theorem Th5: :: DILWORTH:5
for X being infinite set
for n being Nat ex Y being finite Subset of X st card Y > n
proofend;

begin

definition
let R be RelStr ;
let S be Subset of R;
attrS is connected  means :Def1: :: DILWORTH:def 1
 the InternalRel of R is_connected_in S;
end;

:: deftheorem Def1 defines connected DILWORTH:def_1_:_
 for R being RelStr
for S being Subset of R holds
( S is connected iff the InternalRel of R is_connected_in S );

notation
let R be RelStr ;
let S be Subset of R;
synonym  clique S for  connected ;
end;

registration
let R be RelStr ;
cluster trivial  ->  clique for Element of bool the carrier of R;
coherence
 for b1 being Subset of R st b1 is trivial holds
b1 is clique
proofend;
end;

registration
let R be RelStr ;
cluster clique for Element of bool the carrier of R;
existence
 ex b1 being Subset of R st b1 is clique
proofend;
end;

definition
let R be RelStr ;
mode Clique of R is clique Subset of R;
end;

theorem Th6: :: DILWORTH:6
for R being RelStr
for S being Subset of R holds
( S is Clique of R iff for a, b being Element of R st a in S &amp; b in S &amp; a <> b &amp; not a <= b holds
b <= a )
proofend;

registration
let R be RelStr ;
cluster finite connected for Element of bool the carrier of R;
existence
 ex b1 being Clique of R st b1 is finite
proofend;
end;

registration
let R be reflexive RelStr ;
cluster connected  ->  strongly_connected for Element of bool the carrier of R;
coherence
 for b1 being Subset of R st b1 is connected holds
b1 is strongly_connected
proofend;
end;

registration
let R be non empty RelStr ;
cluster non empty finite connected for Element of bool the carrier of R;
existence
 ex b1 being Clique of R st
( b1 is finite &amp; not b1 is empty )
proofend;
end;

theorem :: DILWORTH:7
for R being non empty RelStr
for a1, a2 being Element of R st a1 <> a2 &amp; {a1,a2} is Clique of R &amp; not a1 <= a2 holds
a2 <= a1
proofend;

theorem Th8: :: DILWORTH:8
for R being non empty RelStr
for a1, a2 being Element of R st ( a1 <= a2 or a2 <= a1 ) holds
{a1,a2} is Clique of R
proofend;

theorem Th9: :: DILWORTH:9
for R being RelStr
for C being Clique of R
for S being Subset of C holds S is Clique of R
proofend;

theorem :: DILWORTH:10
for R being RelStr
for C being finite Clique of R
for n being Nat st n <= card C holds
ex B being finite Clique of R st
( B c= C &amp; card B = n )
proofend;

theorem Th11: :: DILWORTH:11
for R being transitive RelStr
for C being Clique of R
for x, y being Element of R st x is_maximal_in C &amp; x <= y holds
C \/ {y} is Clique of R
proofend;

theorem Th12: :: DILWORTH:12
for R being transitive RelStr
for C being Clique of R
for x, y being Element of R st x is_minimal_in C &amp; y <= x holds
C \/ {y} is Clique of R
proofend;

definition
let R be RelStr ;
let S be Subset of R;
attrS is stable  means :Def2: :: DILWORTH:def 2
 for x, y being Element of R st x in S &amp; y in S &amp; x <> y holds
( not x <= y &amp; not y <= x );
end;

:: deftheorem Def2 defines stable DILWORTH:def_2_:_
 for R being RelStr
for S being Subset of R holds
( S is stable iff for x, y being Element of R st x in S &amp; y in S &amp; x <> y holds
( not x <= y &amp; not y <= x ) );

registration
let R be RelStr ;
cluster trivial  ->  stable for Element of bool the carrier of R;
coherence
 for b1 being Subset of R st b1 is trivial holds
b1 is stable
proofend;
end;

registration
let R be RelStr ;
cluster stable for Element of bool the carrier of R;
existence
 ex b1 being Subset of R st b1 is stable
proofend;
end;

definition
let R be RelStr ;
mode StableSet of R is stable Subset of R;
end;

registration
let R be RelStr ;
cluster finite stable for Element of bool the carrier of R;
existence
 ex b1 being StableSet of R st b1 is finite
proofend;
end;

registration
let R be non empty RelStr ;
cluster non empty finite stable for Element of bool the carrier of R;
existence
 ex b1 being StableSet of R st
( b1 is finite &amp; not b1 is empty )
proofend;
end;

theorem :: DILWORTH:13
for R being non empty RelStr
for a1, a2 being Element of R st a1 <> a2 &amp; {a1,a2} is StableSet of R holds
( not a1 <= a2 &amp; not a2 <= a1 )
proofend;

theorem Th14: :: DILWORTH:14
for R being non empty RelStr
for a1, a2 being Element of R holds
( a1 <= a2 or a2 <= a1 or {a1,a2} is StableSet of R )
proofend;

theorem Th15: :: DILWORTH:15
for R being RelStr
for C being Clique of R
for A being StableSet of R
for a, b being set st a in A &amp; b in A &amp; a in C &amp; b in C holds
a = b
proofend;

theorem Th16: :: DILWORTH:16
for R being RelStr
for A being StableSet of R
for B being Subset of A holds B is StableSet of R
proofend;

theorem Th17: :: DILWORTH:17
for R being RelStr
for A being finite StableSet of R
for n being Nat st n <= card A holds
ex B being finite StableSet of R st card B = n
proofend;

begin

definition
let R be RelStr ;
attrR is with_finite_clique#  means :Def3: :: DILWORTH:def 3
 ex C being finite Clique of R st
for D being finite Clique of R holds card D <= card C;
end;

:: deftheorem Def3 defines with_finite_clique# DILWORTH:def_3_:_
 for R being RelStr holds
( R is with_finite_clique# iff ex C being finite Clique of R st
for D being finite Clique of R holds card D <= card C );

registration
cluster finite  ->  with_finite_clique# for RelStr ;
coherence
 for b1 being RelStr st b1 is finite holds
b1 is with_finite_clique#
proofend;
end;

registration
let R be with_finite_clique# RelStr ;
cluster connected  ->  finite for Element of bool the carrier of R;
coherence
 for b1 being Clique of R holds b1 is finite
proofend;
end;

definition
let R be with_finite_clique# RelStr ;
func clique# R ->  Nat means :Def4: :: DILWORTH:def 4
( ex C being finite Clique of R st card C = it &amp; ( for T being finite Clique of R holds card T <= it ) );
existence
 ex b1 being Nat st
( ex C being finite Clique of R st card C = b1 &amp; ( for T being finite Clique of R holds card T <= b1 ) )
proofend;
uniqueness
 for b1, b2 being Nat st ex C being finite Clique of R st card C = b1 &amp; ( for T being finite Clique of R holds card T <= b1 ) &amp; ex C being finite Clique of R st card C = b2 &amp; ( for T being finite Clique of R holds card T <= b2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines clique# DILWORTH:def_4_:_
 for R being with_finite_clique# RelStr
for b2 being Nat holds
( b2 = clique# R iff ( ex C being finite Clique of R st card C = b2 &amp; ( for T being finite Clique of R holds card T <= b2 ) ) );

registration
let R be empty RelStr ;
cluster clique# R ->  empty ;
coherence
 clique# R is empty
proofend;
end;

registration
let R be non empty with_finite_clique# RelStr ;
cluster clique# R ->  positive ;
coherence
 clique# R is positive
proofend;
end;

theorem :: DILWORTH:18
for R being non empty with_finite_clique# RelStr st [#] R is StableSet of R holds
clique# R = 1
proofend;

theorem Th19: :: DILWORTH:19
for R being with_finite_clique# RelStr st clique# R = 1 holds
[#] R is StableSet of R
proofend;

definition
let R be RelStr ;
attrR is with_finite_stability#  means :Def5: :: DILWORTH:def 5
 ex A being finite StableSet of R st
for B being finite StableSet of R holds card B <= card A;
end;

:: deftheorem Def5 defines with_finite_stability# DILWORTH:def_5_:_
 for R being RelStr holds
( R is with_finite_stability# iff ex A being finite StableSet of R st
for B being finite StableSet of R holds card B <= card A );

registration
cluster finite  ->  with_finite_stability# for RelStr ;
coherence
 for b1 being RelStr st b1 is finite holds
b1 is with_finite_stability#
proofend;
end;

registration
let R be with_finite_stability# RelStr ;
cluster stable  ->  finite for Element of bool the carrier of R;
coherence
 for b1 being StableSet of R holds b1 is finite
proofend;
end;

definition
let R be with_finite_stability# RelStr ;
func stability# R ->  Nat means :Def6: :: DILWORTH:def 6
( ex A being finite StableSet of R st card A = it &amp; ( for T being finite StableSet of R holds card T <= it ) );
existence
 ex b1 being Nat st
( ex A being finite StableSet of R st card A = b1 &amp; ( for T being finite StableSet of R holds card T <= b1 ) )
proofend;
uniqueness
 for b1, b2 being Nat st ex A being finite StableSet of R st card A = b1 &amp; ( for T being finite StableSet of R holds card T <= b1 ) &amp; ex A being finite StableSet of R st card A = b2 &amp; ( for T being finite StableSet of R holds card T <= b2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines stability# DILWORTH:def_6_:_
 for R being with_finite_stability# RelStr
for b2 being Nat holds
( b2 = stability# R iff ( ex A being finite StableSet of R st card A = b2 &amp; ( for T being finite StableSet of R holds card T <= b2 ) ) );

registration
let R be empty RelStr ;
cluster stability# R ->  empty ;
coherence
 stability# R is empty
proofend;
end;

registration
let R be non empty with_finite_stability# RelStr ;
cluster stability# R ->  positive ;
coherence
 stability# R is positive
proofend;
end;

theorem Th20: :: DILWORTH:20
for R being non empty with_finite_stability# RelStr st [#] R is Clique of R holds
stability# R = 1
proofend;

theorem Th21: :: DILWORTH:21
for R being with_finite_stability# RelStr st stability# R = 1 holds
[#] R is Clique of R
proofend;

registration
cluster with_finite_clique# with_finite_stability#  ->  finite for RelStr ;
coherence
 for b1 being RelStr st b1 is with_finite_clique# &amp; b1 is with_finite_stability# holds
b1 is finite
proofend;
end;

begin

definition
let R be RelStr ;
let X be Subset of R;
func Lower X ->  Subset of R equals :: DILWORTH:def 7
X \/ (downarrow X);
coherence
 X \/ (downarrow X) is Subset of R ;
func Upper X ->  Subset of R equals :: DILWORTH:def 8
X \/ (uparrow X);
coherence
 X \/ (uparrow X) is Subset of R ;
end;

:: deftheorem  defines Lower DILWORTH:def_7_:_
 for R being RelStr
for X being Subset of R holds Lower X = X \/ (downarrow X);

:: deftheorem  defines Upper DILWORTH:def_8_:_
 for R being RelStr
for X being Subset of R holds Upper X = X \/ (uparrow X);

theorem Th22: :: DILWORTH:22
for R being transitive antisymmetric RelStr
for A being StableSet of R
for z being set st z in Upper A &amp; z in Lower A holds
z in A
proofend;

theorem Th23: :: DILWORTH:23
for R being with_finite_stability# RelStr
for A being StableSet of R st card A = stability# R holds
(Upper A) \/ (Lower A) = [#] R
proofend;

theorem Th24: :: DILWORTH:24
for R being transitive RelStr
for x being Element of R
for S being Subset of R st x is_minimal_in Lower S holds
x is_minimal_in [#] R
proofend;

theorem Th25: :: DILWORTH:25
for R being transitive RelStr
for x being Element of R
for S being Subset of R st x is_maximal_in Upper S holds
x is_maximal_in [#] R
proofend;

definition
let R be RelStr ;
set cR = the carrier of R;
func minimals R ->  Subset of R means :Def9: :: DILWORTH:def 9
 for x being Element of R holds
( x in it iff x is_minimal_in [#] R ) if  not R is empty
otherwise it = {} ;
consistency
 for b1 being Subset of R holds verum ;
existence
 ( ( not R is empty implies ex b1 being Subset of R st
for x being Element of R holds
( x in b1 iff x is_minimal_in [#] R ) ) &amp; ( R is empty implies ex b1 being Subset of R st b1 = {} ) )
proofend;
uniqueness
 for b1, b2 being Subset of R holds
( ( not R is empty &amp; ( for x being Element of R holds
( x in b1 iff x is_minimal_in [#] R ) ) &amp; ( for x being Element of R holds
( x in b2 iff x is_minimal_in [#] R ) ) implies b1 = b2 ) &amp; ( R is empty &amp; b1 = {} &amp; b2 = {} implies b1 = b2 ) )
proofend;
func maximals R ->  Subset of R means :Def10: :: DILWORTH:def 10
 for x being Element of R holds
( x in it iff x is_maximal_in [#] R ) if  not R is empty
otherwise it = {} ;
consistency
 for b1 being Subset of R holds verum ;
existence
 ( ( not R is empty implies ex b1 being Subset of R st
for x being Element of R holds
( x in b1 iff x is_maximal_in [#] R ) ) &amp; ( R is empty implies ex b1 being Subset of R st b1 = {} ) )
proofend;
uniqueness
 for b1, b2 being Subset of R holds
( ( not R is empty &amp; ( for x being Element of R holds
( x in b1 iff x is_maximal_in [#] R ) ) &amp; ( for x being Element of R holds
( x in b2 iff x is_maximal_in [#] R ) ) implies b1 = b2 ) &amp; ( R is empty &amp; b1 = {} &amp; b2 = {} implies b1 = b2 ) )
proofend;
end;

:: deftheorem Def9 defines minimals DILWORTH:def_9_:_
 for R being RelStr
for b2 being Subset of R holds
( ( not R is empty implies ( b2 = minimals R iff for x being Element of R holds
( x in b2 iff x is_minimal_in [#] R ) ) ) &amp; ( R is empty implies ( b2 = minimals R iff b2 = {} ) ) );

:: deftheorem Def10 defines maximals DILWORTH:def_10_:_
 for R being RelStr
for b2 being Subset of R holds
( ( not R is empty implies ( b2 = maximals R iff for x being Element of R holds
( x in b2 iff x is_maximal_in [#] R ) ) ) &amp; ( R is empty implies ( b2 = maximals R iff b2 = {} ) ) );

registration
let R be non empty transitive antisymmetric with_finite_clique# RelStr ;
cluster maximals R ->  non empty ;
coherence
 not maximals R is empty
proofend;
cluster minimals R ->  non empty ;
coherence
 not minimals R is empty
proofend;
end;

registration
let R be RelStr ;
cluster minimals R ->  stable ;
coherence
 minimals R is stable
proofend;
cluster maximals R ->  stable ;
coherence
 maximals R is stable
proofend;
end;

theorem Th26: :: DILWORTH:26
for R being RelStr
for A being StableSet of R st not minimals R c= A holds
not minimals R c= Upper A
proofend;

theorem Th27: :: DILWORTH:27
for R being RelStr
for A being StableSet of R st not maximals R c= A holds
not maximals R c= Lower A
proofend;

begin

registration
let R be RelStr ;
let X be finite Subset of R;
cluster subrelstr X ->  finite ;
coherence
 subrelstr X is finite by YELLOW_0:def_15;
end;

theorem Th28: :: DILWORTH:28
for R being RelStr
for S being Subset of R
for C being Clique of (subrelstr S) holds C is Clique of R
proofend;

theorem Th29: :: DILWORTH:29
for R being RelStr
for S being Subset of R
for C being Clique of R holds C /\ S is Clique of (subrelstr S)
proofend;

theorem Th30: :: DILWORTH:30
for R being RelStr
for S being Subset of R
for A being StableSet of (subrelstr S) holds A is StableSet of R
proofend;

theorem Th31: :: DILWORTH:31
for R being RelStr
for S being Subset of R
for A being StableSet of R holds A /\ S is StableSet of (subrelstr S)
proofend;

theorem Th32: :: DILWORTH:32
for R being RelStr
for S being Subset of R
for B being Subset of (subrelstr S)
for x being Element of (subrelstr S)
for y being Element of R st x = y &amp; x is_maximal_in B holds
y is_maximal_in B
proofend;

theorem Th33: :: DILWORTH:33
for R being RelStr
for S being Subset of R
for B being Subset of (subrelstr S)
for x being Element of (subrelstr S)
for y being Element of R st x = y &amp; x is_minimal_in B holds
y is_minimal_in B
proofend;

theorem Th34: :: DILWORTH:34
for R being transitive RelStr
for A being StableSet of R
for C being Clique of (subrelstr (Lower A))
for a, b being Element of R st a in A &amp; a in C &amp; b in C &amp; not a = b holds
b <= a
proofend;

theorem Th35: :: DILWORTH:35
for R being transitive RelStr
for A being StableSet of R
for C being Clique of (subrelstr (Upper A))
for a, b being Element of R st a in A &amp; a in C &amp; b in C &amp; not a = b holds
a <= b
proofend;

registration
let R be with_finite_clique# RelStr ;
let S be Subset of R;
cluster subrelstr S ->  with_finite_clique# ;
coherence
 subrelstr S is with_finite_clique#
proofend;
end;

registration
let R be with_finite_stability# RelStr ;
let S be Subset of R;
cluster subrelstr S ->  with_finite_stability# ;
coherence
 subrelstr S is with_finite_stability#
proofend;
end;

theorem Th36: :: DILWORTH:36
for R being non empty transitive antisymmetric with_finite_clique# RelStr
for x being Element of R ex y being Element of R st
( y is_minimal_in [#] R &amp; ( y = x or y < x ) )
proofend;

theorem :: DILWORTH:37
for R being transitive antisymmetric with_finite_clique# RelStr holds Upper (minimals R) = [#] R
proofend;

theorem Th38: :: DILWORTH:38
for R being non empty transitive antisymmetric with_finite_clique# RelStr
for x being Element of R ex y being Element of R st
( y is_maximal_in [#] R &amp; ( y = x or x < y ) )
proofend;

theorem :: DILWORTH:39
for R being transitive antisymmetric with_finite_clique# RelStr holds Lower (maximals R) = [#] R
proofend;

theorem Th40: :: DILWORTH:40
for R being transitive antisymmetric with_finite_clique# RelStr
for A being StableSet of R st minimals R c= A holds
A = minimals R
proofend;

theorem Th41: :: DILWORTH:41
for R being transitive antisymmetric with_finite_clique# RelStr
for A being StableSet of R st maximals R c= A holds
A = maximals R
proofend;

theorem Th42: :: DILWORTH:42
for R being with_finite_clique# RelStr
for S being Subset of R holds clique# (subrelstr S) <= clique# R
proofend;

theorem :: DILWORTH:43
for R being with_finite_clique# RelStr
for C being Clique of R
for S being Subset of R st card C = clique# R &amp; C c= S holds
clique# (subrelstr S) = clique# R
proofend;

theorem Th44: :: DILWORTH:44
for R being with_finite_stability# RelStr
for S being Subset of R holds stability# (subrelstr S) <= stability# R
proofend;

theorem Th45: :: DILWORTH:45
for R being with_finite_stability# RelStr
for A being StableSet of R
for S being Subset of R st card A = stability# R &amp; A c= S holds
stability# (subrelstr S) = stability# R
proofend;

begin

definition
let R be RelStr ;
let P be a_partition of the carrier of R;
attrP is Clique-wise  means :Def11: :: DILWORTH:def 11
 for x being set st x in P holds
x is Clique of R;
end;

:: deftheorem Def11 defines Clique-wise DILWORTH:def_11_:_
 for R being RelStr
for P being a_partition of the carrier of R holds
( P is Clique-wise iff for x being set st x in P holds
x is Clique of R );

registration
let R be RelStr ;
cluster with_non-empty_elements Clique-wise for a_partition of the carrier of R;
existence
 ex b1 being a_partition of the carrier of R st b1 is Clique-wise
proofend;
end;

definition
let R be RelStr ;
mode Clique-partition of R is Clique-wise a_partition of the carrier of R;
end;

registration
let R be empty RelStr ;
cluster empty  ->  Clique-wise for a_partition of the carrier of R;
coherence
 for b1 being a_partition of the carrier of R st b1 is empty holds
b1 is Clique-wise
proofend;
end;

theorem Th46: :: DILWORTH:46
for R being finite RelStr
for C being Clique-partition of R holds card C >= stability# R
proofend;

theorem Th47: :: DILWORTH:47
for R being with_finite_stability# RelStr
for A being StableSet of R
for C being Clique-partition of R st card C = card A holds
ex f being Function of A,C st
( f is bijective &amp; ( for x being set st x in A holds
x in f . x ) )
proofend;

theorem Th48: :: DILWORTH:48
for R being finite RelStr
for A being StableSet of R
for C being Clique-partition of R st card C = card A holds
for c being set st c in C holds
ex a being Element of A st c /\ A = {a}
proofend;

theorem Th49: :: DILWORTH:49
for R being non empty transitive antisymmetric with_finite_stability# RelStr
for A being StableSet of R
for U being Clique-partition of (subrelstr (Upper A))
for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R &amp; card U = stability# R &amp; card L = stability# R holds
ex C being Clique-partition of R st card C = stability# R
proofend;

definition
let R be RelStr ;
let P be a_partition of the carrier of R;
attrP is StableSet-wise  means :Def12: :: DILWORTH:def 12
 for x being set st x in P holds
x is StableSet of R;
end;

:: deftheorem Def12 defines StableSet-wise DILWORTH:def_12_:_
 for R being RelStr
for P being a_partition of the carrier of R holds
( P is StableSet-wise iff for x being set st x in P holds
x is StableSet of R );

registration
let R be RelStr ;
cluster with_non-empty_elements StableSet-wise for a_partition of the carrier of R;
existence
 ex b1 being a_partition of the carrier of R st b1 is StableSet-wise
proofend;
end;

definition
let R be RelStr ;
mode Coloring of R is StableSet-wise a_partition of the carrier of R;
end;

registration
let R be empty RelStr ;
cluster  ->  StableSet-wise for a_partition of the carrier of R;
coherence
 for b1 being a_partition of the carrier of R holds b1 is StableSet-wise
proofend;
end;

theorem :: DILWORTH:50
for R being finite RelStr
for C being Coloring of R holds card C >= clique# R
proofend;

begin

:: There seems to be little theory of antisymmetric transitive relations.
:: Posets are required to be reflexive and antisymmetric while
:: strict posets to be irreflexive and asymmetric (and both are
:: required to be transitive.) Since asymmetric implies antisymmetric,
:: it seems that the common ground would be antisymmetric and transitive
:: relations.
:: [WP: ] Dilworth's_Decomposition_Theorem
theorem Th51: :: DILWORTH:51
for R being finite transitive antisymmetric RelStr ex C being Clique-partition of R st card C = stability# R
proofend;

definition
let R be non empty with_finite_stability# RelStr ;
let C be Subset of R;
attrC is strong-chain  means :Def13: :: DILWORTH:def 13
 for S being non empty finite Subset of R ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R &amp; ex c being set st
( c in P &amp; S /\ C c= c &amp; ( for d being set st d in P &amp; d <> c holds
C /\ d = {} ) ) );
end;

:: deftheorem Def13 defines strong-chain DILWORTH:def_13_:_
 for R being non empty with_finite_stability# RelStr
for C being Subset of R holds
( C is strong-chain iff for S being non empty finite Subset of R ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R &amp; ex c being set st
( c in P &amp; S /\ C c= c &amp; ( for d being set st d in P &amp; d <> c holds
C /\ d = {} ) ) ) );

registration
let R be non empty with_finite_stability# RelStr ;
cluster strong-chain  ->  clique for Element of bool the carrier of R;
coherence
 for b1 being Subset of R st b1 is strong-chain holds
b1 is clique
proofend;
end;

registration
let R be non empty transitive antisymmetric with_finite_stability# RelStr ;
cluster1 -element  ->  strong-chain for Element of bool the carrier of R;
coherence
 for b1 being Subset of R st b1 is 1 -element holds
b1 is strong-chain
proofend;
end;

theorem Th52: :: DILWORTH:52
for R being non empty transitive antisymmetric with_finite_stability# RelStr ex S being non empty Subset of R st
( S is strong-chain &amp; ( for D being Subset of R holds
( not D is strong-chain or not S c< D ) ) )
proofend;

theorem :: DILWORTH:53
for R being transitive antisymmetric with_finite_stability# RelStr ex C being Clique-partition of R st card C = stability# R
proofend;

theorem :: DILWORTH:54
for R being transitive antisymmetric with_finite_clique# RelStr ex A being Coloring of R st card A = clique# R
proofend;

begin

:: [WP: ] Erdos-Szekeres_Theorem
theorem Th55: :: DILWORTH:55
for R being finite transitive antisymmetric RelStr
for r, s being Nat holds
( not card R = (r * s) + 1 or ex C being Clique of R st card C >= r + 1 or ex A being StableSet of R st card A >= s + 1 )
proofend;

:: In a sequence of n^2+1 (distinct) real numbers there is a monotone
:: subsequence of length at least n+1.
:: Let F be the sequence. Define a RelStr with the carrier equal F (a set
:: of ordered pairs) and the relation defined as: if a = [i,F.i] in F and
:: b = [j,F.j] in F, for some i and j, then a < b iff i < j &amp; F.i < F.j.
:: The relation is asymmetric and transitive.
:: Considered defining FinSubsequence of f but have given up.
:: There is not much gain from having FinSubsequence of f instead of
:: FinSubsequence st g c= f
theorem :: DILWORTH:56
for f being real-valued FinSequence
for n being Nat st card f = (n ^2) + 1 &amp; f is one-to-one holds
ex g being real-valued FinSubsequence st
( g c= f &amp; card g >= n + 1 &amp; ( g is increasing or g is decreasing ) )
proofend;