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

:: Facts that I could not find in MML.

scheme :: DILWORTH:sch 1
FraenkelFinCard1{ F₁() -> non empty finite set , P₁[ set ], F₂() -> finite set , F₃( set ) -> set } :

card F₂() <= card F₁()

provided

A1: F₂() = { F₃(w) where w is Element of F₁() : P₁[w] }

proof end;

theorem Th1: :: DILWORTH:1

for X, Y, x being set st not x in X holds
X \ (Y \/ {x}) = X \ Y

proof end;

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)

proof end;

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

proof end;

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

proof end;

theorem Th5: :: DILWORTH:5

for X being infinite set
for n being Nat ex Y being finite Subset of X st card Y > n

proof end;

definition

let R be RelStr ;
let S be Subset of R;

attr S 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 b₁ being Subset of R st b₁ is trivial holds
b₁ is clique

proof end;

end;

registration

let R be RelStr ;

cluster clique for Element of bool the carrier of R;

existence
ex b₁ being Subset of R st b₁ is clique

proof end;

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 & b in S & a <> b & not a <= b holds
b <= a )

proof end;

registration

let R be RelStr ;

cluster finite connected for Element of bool the carrier of R;

existence
ex b₁ being Clique of R st b₁ is finite

proof end;

end;

registration

let R be reflexive RelStr ;

cluster connected -> strongly_connected for Element of bool the carrier of R;

coherence
for b₁ being Subset of R st b₁ is connected holds
b₁ is strongly_connected

proof end;

end;

registration

let R be non empty RelStr ;

cluster non empty finite connected for Element of bool the carrier of R;

existence
ex b₁ being Clique of R st
( b₁ is finite & not b₁ is empty )

proof end;

end;

theorem :: DILWORTH:7

for R being non empty RelStr
for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is Clique of R & not a1 <= a2 holds
a2 <= a1

proof end;

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

proof end;

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

proof end;

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 & card B = n )

proof end;

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 & x <= y holds
C \/ {y} is Clique of R

proof end;

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 & y <= x holds
C \/ {y} is Clique of R

proof end;

definition

let R be RelStr ;
let S be Subset of R;

attr S is stable means :Def2: :: DILWORTH:def 2
for x, y being Element of R st x in S & y in S & x <> y holds
( not x <= y & 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 & y in S & x <> y holds
( not x <= y & not y <= x ) );

registration

let R be RelStr ;

cluster trivial -> stable for Element of bool the carrier of R;

coherence
for b₁ being Subset of R st b₁ is trivial holds
b₁ is stable by ZFMISC_1:def 10;

end;

registration

let R be RelStr ;

cluster stable for Element of bool the carrier of R;

existence
ex b₁ being Subset of R st b₁ is stable

proof end;

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 b₁ being StableSet of R st b₁ is finite

proof end;

end;

registration

let R be non empty RelStr ;

cluster non empty finite stable for Element of bool the carrier of R;

existence
ex b₁ being StableSet of R st
( b₁ is finite & not b₁ is empty )

proof end;

end;

theorem :: DILWORTH:13

for R being non empty RelStr
for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is StableSet of R holds
( not a1 <= a2 & not a2 <= a1 )

proof end;

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 )

proof end;

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 & b in A & a in C & b in C holds
a = b

proof end;

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

proof end;

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

proof end;

definition

let R be RelStr ;

attr R 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 b₁ being RelStr st b₁ is finite holds
b₁ is with_finite_clique#

proof end;

end;

registration

let R be with_finite_clique# RelStr ;

cluster connected -> finite for Element of bool the carrier of R;

coherence
for b₁ being Clique of R holds b₁ is finite

proof end;

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 & ( for T being finite Clique of R holds card T <= it ) );

existence
ex b₁ being Nat st
( ex C being finite Clique of R st card C = b₁ & ( for T being finite Clique of R holds card T <= b₁ ) )

proof end;

uniqueness
for b₁, b₂ being Nat st ex C being finite Clique of R st card C = b₁ & ( for T being finite Clique of R holds card T <= b₁ ) & ex C being finite Clique of R st card C = b₂ & ( for T being finite Clique of R holds card T <= b₂ ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines clique# DILWORTH:def 4 :
for R being with_finite_clique# RelStr
for b₂ being Nat holds
( b₂ = clique# R iff ( ex C being finite Clique of R st card C = b₂ & ( for T being finite Clique of R holds card T <= b₂ ) ) );

registration

let R be empty RelStr ;

cluster clique# R -> empty ;

coherence
clique# R is empty

proof end;

end;

registration

let R be non empty with_finite_clique# RelStr ;

cluster clique# R -> positive ;

coherence
clique# R is positive

proof end;

end;

theorem :: DILWORTH:18

for R being non empty with_finite_clique# RelStr st [#] R is StableSet of R holds
clique# R = 1

proof end;

theorem Th19: :: DILWORTH:19

for R being with_finite_clique# RelStr st clique# R = 1 holds
[#] R is StableSet of R

proof end;

definition

let R be RelStr ;

attr R 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 b₁ being RelStr st b₁ is finite holds
b₁ is with_finite_stability#

proof end;

end;

registration

let R be with_finite_stability# RelStr ;

cluster stable -> finite for Element of bool the carrier of R;

coherence
for b₁ being StableSet of R holds b₁ is finite

proof end;

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 & ( for T being finite StableSet of R holds card T <= it ) );

existence
ex b₁ being Nat st
( ex A being finite StableSet of R st card A = b₁ & ( for T being finite StableSet of R holds card T <= b₁ ) )

proof end;

uniqueness
for b₁, b₂ being Nat st ex A being finite StableSet of R st card A = b₁ & ( for T being finite StableSet of R holds card T <= b₁ ) & ex A being finite StableSet of R st card A = b₂ & ( for T being finite StableSet of R holds card T <= b₂ ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines stability# DILWORTH:def 6 :
for R being with_finite_stability# RelStr
for b₂ being Nat holds
( b₂ = stability# R iff ( ex A being finite StableSet of R st card A = b₂ & ( for T being finite StableSet of R holds card T <= b₂ ) ) );

registration

let R be empty RelStr ;

cluster stability# R -> empty ;

coherence
stability# R is empty

proof end;

end;

registration

let R be non empty with_finite_stability# RelStr ;

cluster stability# R -> positive ;

coherence
stability# R is positive

proof end;

end;

theorem Th20: :: DILWORTH:20

for R being non empty with_finite_stability# RelStr st [#] R is Clique of R holds
stability# R = 1

proof end;

theorem Th21: :: DILWORTH:21

for R being with_finite_stability# RelStr st stability# R = 1 holds
[#] R is Clique of R

proof end;

registration

cluster with_finite_clique# with_finite_stability# -> finite for RelStr ;

coherence
for b₁ being RelStr st b₁ is with_finite_clique# & b₁ is with_finite_stability# holds
b₁ is finite

proof end;

end;

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 & z in Lower A holds
z in A

proof end;

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

proof end;

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

proof end;

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

proof end;

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 b₁ being Subset of R holds verum ;
existence
( ( not R is empty implies ex b₁ being Subset of R st
for x being Element of R holds
( x in b₁ iff x is_minimal_in [#] R ) ) & ( R is empty implies ex b₁ being Subset of R st b₁ = {} ) )

proof end;

uniqueness
for b₁, b₂ being Subset of R holds
( ( not R is empty & ( for x being Element of R holds
( x in b₁ iff x is_minimal_in [#] R ) ) & ( for x being Element of R holds
( x in b₂ iff x is_minimal_in [#] R ) ) implies b₁ = b₂ ) & ( R is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) )

proof end;

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 b₁ being Subset of R holds verum ;
existence
( ( not R is empty implies ex b₁ being Subset of R st
for x being Element of R holds
( x in b₁ iff x is_maximal_in [#] R ) ) & ( R is empty implies ex b₁ being Subset of R st b₁ = {} ) )

proof end;

uniqueness
for b₁, b₂ being Subset of R holds
( ( not R is empty & ( for x being Element of R holds
( x in b₁ iff x is_maximal_in [#] R ) ) & ( for x being Element of R holds
( x in b₂ iff x is_maximal_in [#] R ) ) implies b₁ = b₂ ) & ( R is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) )

proof end;

end;

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

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

registration

let R be non empty transitive antisymmetric with_finite_clique# RelStr ;

cluster maximals R -> non empty ;

coherence
not maximals R is empty

proof end;

cluster minimals R -> non empty ;

coherence
not minimals R is empty

proof end;

end;

registration

let R be RelStr ;

cluster minimals R -> stable ;

coherence
minimals R is stable

proof end;

cluster maximals R -> stable ;

coherence
maximals R is stable

proof end;

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

proof end;

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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 & x is_maximal_in B holds
y is_maximal_in B

proof end;

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 & x is_minimal_in B holds
y is_minimal_in B

proof end;

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 & a in C & b in C & not a = b holds
b <= a

proof end;

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 & a in C & b in C & not a = b holds
a <= b

proof end;

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#

proof end;

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#

proof end;

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 & ( y = x or y < x ) )

proof end;

theorem :: DILWORTH:37

for R being transitive antisymmetric with_finite_clique# RelStr holds Upper (minimals R) = [#] R

proof end;

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 & ( y = x or x < y ) )

proof end;

theorem :: DILWORTH:39

for R being transitive antisymmetric with_finite_clique# RelStr holds Lower (maximals R) = [#] R

proof end;

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

proof end;

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

proof end;

theorem Th42: :: DILWORTH:42

for R being with_finite_clique# RelStr
for S being Subset of R holds clique# (subrelstr S) <= clique# R

proof end;

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 & C c= S holds
clique# (subrelstr S) = clique# R

proof end;

theorem Th44: :: DILWORTH:44

for R being with_finite_stability# RelStr
for S being Subset of R holds stability# (subrelstr S) <= stability# R

proof end;

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 & A c= S holds
stability# (subrelstr S) = stability# R

proof end;

definition

let R be RelStr ;
let P be a_partition of the carrier of R;

attr P 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 V40() with_non-empty_elements Clique-wise for a_partition of the carrier of R;

existence
ex b₁ being a_partition of the carrier of R st b₁ is Clique-wise

proof end;

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 b₁ being a_partition of the carrier of R st b₁ is empty holds
b₁ is Clique-wise ;

end;

theorem Th46: :: DILWORTH:46

for R being finite RelStr
for C being Clique-partition of R holds card C >= stability# R

proof end;

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 & ( for x being set st x in A holds
x in f . x ) )

proof end;

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}

proof end;

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 & card U = stability# R & card L = stability# R holds
ex C being Clique-partition of R st card C = stability# R

proof end;

definition

let R be RelStr ;
let P be a_partition of the carrier of R;

attr P 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 V40() with_non-empty_elements StableSet-wise for a_partition of the carrier of R;

existence
ex b₁ being a_partition of the carrier of R st b₁ is StableSet-wise

proof end;

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 b₁ being a_partition of the carrier of R holds b₁ is StableSet-wise ;

end;

theorem :: DILWORTH:50

for R being finite RelStr
for C being Coloring of R holds card C >= clique# R

proof end;

:: 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.
:: 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

proof end;

definition

let R be non empty with_finite_stability# RelStr ;
let C be Subset of R;

attr C is strong-chain means :: 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 & ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) ) );

end;

:: deftheorem 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 & ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & 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 b₁ being Subset of R st b₁ is strong-chain holds
b₁ is clique

proof end;

end;

registration

let R be non empty transitive antisymmetric with_finite_stability# RelStr ;

cluster 1 -element -> strong-chain for Element of bool the carrier of R;

coherence
for b₁ being Subset of R st b₁ is 1 -element holds
b₁ is strong-chain

proof end;

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 & ( for D being Subset of R holds
( not D is strong-chain or not S c< D ) ) )

proof end;

theorem :: DILWORTH:53

for R being transitive antisymmetric with_finite_stability# RelStr ex C being Clique-partition of R st card C = stability# R

proof end;

theorem :: DILWORTH:54

for R being transitive antisymmetric with_finite_clique# RelStr ex A being Coloring of R st card A = clique# R

proof end;

:: 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 )

proof end;

:: 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 & 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 & f is one-to-one holds
ex g being real-valued FinSubsequence st
( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) )

proof end;