:: Dilworth's Decomposition Theorem for Posets :: by Piotr Rudnicki :: :: Received September 17, 2009 :: Copyright (c) 2009-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FINSET_1, XBOOLE_0, CARD_1, XXREAL_0, SUBSET_1, TARSKI, ORDINAL1, SETFAM_1, ZFMISC_1, EQREL_1, NAT_1, FUNCT_1, FINSEQ_1, ARYTM_3, RELAT_1, ORDERS_2, RELAT_2, COMBGRAS, STRUCT_0, ORDERS_1, CIRCUIT2, GROUP_10, RAMSEY_1, JORDAN4, WAYBEL_0, WAYBEL_4, YELLOW_0, FUNCT_2, LEXBFS, ARYTM_1, UPROOTS, CARD_3, FINSEQ_2, VALUED_0, SQUARE_1, ORDINAL2, XREAL_0, DILWORTH; notations TARSKI, RELAT_1, RELAT_2, RELSET_1, FINSET_1, SETFAM_1, XBOOLE_0, SUBSET_1, CARD_1, STRUCT_0, WAYBEL_0, WAYBEL_4, ORDERS_2, ORDINAL1, EQREL_1, FUNCT_1, FUNCT_2, NUMBERS, XREAL_0, XXREAL_0, YELLOW_0, XCMPLX_0, ZFMISC_1, LEXBFS, FINSEQ_1, SQUARE_1, UPROOTS, RVSUM_1, INT_5, FINSEQ_2, VALUED_0, GROUP_10, RAMSEY_1, DOMAIN_1; constructors DOMAIN_1, LEXBFS, WAYBEL_4, SQUARE_1, UPROOTS, WSIERP_1, INT_5, SEQ_1, RAMSEY_1, RELSET_1, BINOP_2; registrations STRUCT_0, XXREAL_0, RELSET_1, CARD_1, YELLOW_0, XREAL_0, FINSET_1, XBOOLE_0, NAT_1, INT_1, YELLOW_2, EQREL_1, FINSEQ_1, FUNCT_1, SUBSET_1, ORDINAL1, PEPIN, RVSUM_1, UPROOTS, FUNCT_2, FINSEQ_2, NUMBERS, PNPROC_1, RELAT_1, VALUED_0, ZFMISC_1, ORDERS_2; requirements ARITHM, SUBSET, BOOLE, NUMERALS, REAL; definitions TARSKI, STRUCT_0, FUNCT_1, RELAT_2, WAYBEL_0, XBOOLE_0, SQUARE_1, VALUED_0, ORDERS_2, GROUP_10; theorems CARD_1, CARD_2, NAT_1, XREAL_1, YELLOW_0, XBOOLE_0, TARSKI, ORDERS_2, XBOOLE_1, ZFMISC_1, EQREL_1, INT_1, EULER_1, ENUMSET1, FUNCT_1, FUNCT_2, LEXBFS, FINSEQ_4, RELAT_2, BAGORDER, WAYBEL_0, WAYBEL_4, XXREAL_0, RELAT_1, ORDERS_1, FINSET_1, ORDINAL1, PUA2MSS1, DICKSON, FINSEQ_1, INT_5, RVSUM_1, UPROOTS, FINSEQ_2, CARD_3, FINSEQ_3, GRFUNC_1, RAMSEY_1, SUBSET_1, PRE_POLY, XTUPLE_0; schemes NAT_1, FUNCT_2, XBOOLE_0, CLASSES1, FRAENKEL, TREES_2, RELSET_1; begin :: Preliminaries :: Facts that I could not find in MML. scheme FraenkelFinCard1 { A() -> finite non empty set, P[set], Y() -> finite set, F(set) -> set }: card Y() <= card A() provided A1: Y() = { F(w) where w is Element of A(): P[w] } proof A2: A() is finite; set Z = { F(w) where w is Element of A(): w in A() }; Z is finite from FRAENKEL:sch 21 (A2); then reconsider Z as finite set; A3: Z = { F(w) where w is Element of A(): w in A() }; A4: card Z <= card A() from TREES_2:sch 3(A3); Y() c= Z proof let x be set; assume x in Y(); then ex w being Element of A() st x = F(w) & P[w] by A1; hence x in Z; end; then card Y() <= card Z by NAT_1:43; hence card Y() <= card A() by A4,XXREAL_0:2; end; theorem Th1: :: set00: for X, Y, x being set st not x in X holds X \ (Y \/ {x}) = X \ Y proof let X, Y, x be set; assume not x in X; then A1: not x in X \ Y; thus X \ (Y \/ {x}) = (X \ Y) \ {x} by XBOOLE_1:41 .= X \ Y by A1,ZFMISC_1:57; end; theorem Th2: :: ssf0: for X, Y being set, F being Subset-Family of X, G being Subset-Family of Y holds F \/ G is Subset-Family of X \/ Y proof let X, Y be set, F be Subset-Family of X, G be Subset-Family of Y; A1: F \/ G c= bool X \/ bool Y by XBOOLE_1:13; bool X \/ bool Y c= bool (X \/ Y) by ZFMISC_1:69; hence F \/ G is Subset-Family of X \/ Y by A1,XBOOLE_1:1; end; theorem Th3: :: SPpart0: for X, Y being set, F being a_partition of X, G being a_partition of Y st X misses Y holds F \/ G is a_partition of X \/ Y proof let X, Y be set, F be a_partition of X, G be a_partition of Y such that A1: X misses Y; set PR = F \/ G; set XY = X \/ Y; A2: PR is Subset-Family of XY by Th2; A3: union PR = union F \/ union G by ZFMISC_1:78 .= X \/ union G by EQREL_1:def 4 .= X \/ Y by EQREL_1:def 4; now let A be Subset of XY such that A4: A in PR; A in F or A in G by A4,XBOOLE_0:def 3; hence A <> {} by EQREL_1:def 4; let B be Subset of XY such that A5: B in PR; per cases by A4,A5,XBOOLE_0:def 3; suppose A in F & B in F or A in G & B in G; hence A = B or A misses B by EQREL_1:def 4; end; suppose A in F & B in G or A in G & B in F; hence A = B or A misses B by A1,XBOOLE_1:64; end; end; hence F \/ G is a_partition of X \/ Y by A2,A3,EQREL_1:def 4; end; theorem Th4: :: SPpart: for X, Y being set, F being a_partition of Y st Y c< X holds F \/ { X \ Y } is a_partition of X proof let X, Y be set, F be a_partition of Y; assume A1: Y c< X; then A2: X \ Y <> {} by XBOOLE_1:105; Y c= X by A1,XBOOLE_0:def 8; then A3: Y \/ (X \ Y) = X by XBOOLE_1:45; { X \ Y } is a_partition of X \ Y by A2,EQREL_1:39; hence F \/ { X \ Y } is a_partition of X by A3,Th3,XBOOLE_1:79; end; theorem Th5: :: Sinfset: for X being infinite set, n being Nat ex Y being finite Subset of X st card Y > n proof :: DICKSON:3 let X be infinite set, n be Nat; consider f being Function of NAT, X such that A1: f is one-to-one by DICKSON:3; set Sn = Seg (n+1); reconsider ff = f|Sn as Function of Sn, X by FUNCT_2:32; ff is one-to-one by A1,FUNCT_1:52; then card ff = card rng ff by PRE_POLY:19; then A2: card dom ff = card rng ff by CARD_1:62; reconsider Y = rng ff as finite Subset of X by RELAT_1:def 19; take Y; dom ff = Sn by FUNCT_2:def 1; then card dom ff = n+1 by FINSEQ_1:57; hence card Y > n by A2,NAT_1:13; end; begin :: Cliques and stable sets definition let R be RelStr, S be Subset of R; attr S is connected means :Def1: the InternalRel of R is_connected_in S; end; notation let R be RelStr, S be Subset of R; synonym S is clique for S is connected; end; registration let R be RelStr; cluster trivial -> clique for Subset of R; coherence proof let S be Subset of R; assume A1: S is trivial; let x1, x2 be set; thus thesis by A1,ZFMISC_1:def 10; end; end; registration let R be RelStr; cluster clique for Subset of R; existence proof take {}R; let x1, x2 be set; thus thesis; end; end; definition let R be RelStr; mode Clique of R is clique Subset of R; end; theorem Th6: :: DClique: for R being RelStr, 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 holds a <= b or b <= a proof let R be RelStr, S be Subset of R; set RR = the InternalRel of R; hereby assume S is Clique of R; then A1: RR is_connected_in S by Def1; let a, b be Element of R; assume a in S & b in S & a <> b; then [a,b] in RR or [b,a] in RR by A1,RELAT_2:def 6; hence a <= b or b <= a by ORDERS_2:def 5; end; assume A2: for a, b being Element of R st a in S & b in S & a <> b holds a <= b or b <= a; RR is_connected_in S proof let x, y be set; assume A3: x in S & y in S & x <> y; then reconsider x9 = x, y9 = y as Element of R; x9 <= y9 or y9 <= x9 by A3,A2; hence [x,y] in RR or [y,x] in RR by ORDERS_2:def 5; end; hence S is Clique of R by Def1; end; registration let R be RelStr; cluster finite for Clique of R; existence proof take {}R; thus thesis; end; end; registration let R be reflexive RelStr; cluster connected -> strongly_connected for Subset of R; coherence proof let C be Subset of R; set iR = the InternalRel of R, cR = the carrier of R; assume C is clique; then A1: iR is_connected_in C by Def1; A2: iR is_reflexive_in cR by ORDERS_2:def 2; thus C is strongly_connected proof let x, y be set such that A3: x in C and A4: y in C; per cases; suppose x = y; hence [x,y] in the InternalRel of R or [y,x] in the InternalRel of R by A3,A2,RELAT_2:def 1; end; suppose x <> y; hence [x,y] in the InternalRel of R or [y,x] in the InternalRel of R by A3,A4,A1,RELAT_2:def 6; end; end; end; end; registration let R be non empty RelStr; cluster finite non empty for Clique of R; existence proof {the Element of R} is clique; hence thesis; end; end; theorem :: Clique36a: for R being non empty RelStr, a1,a2 being Element of R st a1 <> a2 & {a1,a2} is Clique of R holds a1 <= a2 or a2 <= a1 proof let R be non empty RelStr, a1,a2 be Element of R; assume A1: a1 <> a2; A2: a1 in {a1,a2} & a2 in {a1,a2} by TARSKI:def 2; assume {a1,a2} is Clique of R; hence thesis by A2,A1,Th6; end; theorem Th8: :: Clique36b: for R being non empty RelStr, a1,a2 being Element of R st a1 <= a2 or a2 <= a1 holds {a1,a2} is Clique of R proof let R be non empty RelStr, a1,a2 be Element of R; assume A1: a1 <= a2 or a2 <= a1; now let x,y be Element of R; assume x in {a1,a2} & y in {a1,a2}; then A2: (x = a1 or x = a2) & (y = a1 or y = a2) by TARSKI:def 2; assume x <> y; hence x <= y or y <= x by A1,A2; end; hence thesis by Th6; end; theorem Th9: :: Clique37: for R being RelStr, C being Clique of R, S being Subset of C holds S is Clique of R proof let R be RelStr, C be Clique of R, S be Subset of C; set iR = the InternalRel of R; A1: iR is_connected_in C by Def1; iR is_connected_in S proof let x1, x2 be set; assume x1 in S & x2 in S & x1<>x2; hence thesis by A1,RELAT_2:def 6; end; hence thesis by Def1,XBOOLE_1:1; end; theorem :: Clique1: for R being RelStr, C being finite Clique of R, n being Nat st n <= card C ex B being finite Clique of R st B c= C & card B = n proof let R be RelStr, C be finite Clique of R, n be Nat such that A1: n <= card C; consider BB being finite Subset of C such that A2: card BB = n by A1,FINSEQ_4:72; reconsider BB as finite Clique of R by Th9; take BB; thus thesis by A2; end; theorem Th11: :: ExtClique for R being transitive RelStr, C being Clique of R, x, y being Element of R st x is_maximal_in C & x <= y holds C \/ {y} is Clique of R proof let R be transitive RelStr, C be Clique of R, x, y be Element of R such that A1: x is_maximal_in C and A2: x <= y; A3: x in C by A1,WAYBEL_4:55; A4: the carrier of R is non empty by A1,WAYBEL_4:55; set Cb = C \/ {y}; A5: Cb c= the carrier of R proof let x be set; assume A6: x in Cb; per cases by A6,XBOOLE_0:def 3; suppose x in C; hence x in the carrier of R; end; suppose x in {y}; then x = y by TARSKI:def 1; hence x in the carrier of R by A4; end; end; now let a, b be Element of R such that A7: a in Cb & b in Cb and A8: a <> b; per cases by A7,XBOOLE_0:def 3; suppose a in C & b in C; hence a <= b or b <= a by A8,Th6; end; suppose that A9: a in C and A10: b in {y}; A11: b = y by A10,TARSKI:def 1; A12: not x < a by A1,A9,WAYBEL_4:55; per cases; suppose x <> a; then a <= x or x <= a by A9,A3,Th6; hence a <= b or b <= a by A2,A11,A12,ORDERS_2:3,def 6; end; suppose x = a; hence a <= b or b <= a by A2,A10,TARSKI:def 1; end; end; suppose that A13: a in {y} and A14: b in C; A15: a = y by A13,TARSKI:def 1; A16: not x < b by A1,A14,WAYBEL_4:55; per cases; suppose x <> b; then b <= x or x <= b by A14,A3,Th6; hence a <= b or b <= a by A2,A15,A16,ORDERS_2:3,def 6; end; suppose x = b; hence a <= b or b <= a by A2,A13,TARSKI:def 1; end; end; suppose a in {y} & b in {y}; then a = y & b = y by TARSKI:def 1; hence a <= b or b <= a by A8; end; end; hence C \/ {y} is Clique of R by A5,Th6; end; theorem Th12: :: ExtCliquemin for R being transitive RelStr, C being Clique of R, x, y being Element of R st x is_minimal_in C & y <= x holds C \/ {y} is Clique of R proof let R be transitive RelStr, C be Clique of R, x, y be Element of R such that A1: x is_minimal_in C and A2: y <= x; A3: x in C by A1,WAYBEL_4:56; A4: the carrier of R is non empty by A1,WAYBEL_4:56; set Cb = C \/ {y}; A5: Cb c= the carrier of R proof let x be set; assume A6: x in Cb; per cases by A6,XBOOLE_0:def 3; suppose x in C; hence x in the carrier of R; end; suppose x in {y}; then x = y by TARSKI:def 1; hence x in the carrier of R by A4; end; end; now let a, b be Element of R such that A7: a in Cb & b in Cb and A8: a <> b; per cases by A7,XBOOLE_0:def 3; suppose a in C & b in C; hence a <= b or b <= a by A8,Th6; end; suppose that A9: a in C and A10: b in {y}; A11: b = y by A10,TARSKI:def 1; A12: not a < x by A1,A9,WAYBEL_4:56; per cases; suppose A13: a <> x; then not a <= x by A12,ORDERS_2:def 6; then x <= a by A9,A3,A13,Th6; hence a <= b or b <= a by A2,A11,ORDERS_2:3; end; suppose x = a; hence a <= b or b <= a by A2,A10,TARSKI:def 1; end; end; suppose that A14: a in {y} and A15: b in C; A16: a = y by A14,TARSKI:def 1; A17: not b < x by A1,A15,WAYBEL_4:56; per cases; suppose A18: b <> x; then not b <= x by A17,ORDERS_2:def 6; then x <= b by A15,A3,A18,Th6; hence a <= b or b <= a by A2,A16,ORDERS_2:3; end; suppose x = b; hence a <= b or b <= a by A2,A14,TARSKI:def 1; end; end; suppose a in {y} & b in {y}; then a = y & b = y by TARSKI:def 1; hence a <= b or b <= a by A8; end; end; hence C \/ {y} is Clique of R by A5,Th6; end; definition let R be RelStr, S be Subset of R; attr S is stable means :Def2: for x, y being Element of R st x in S & y in S & x <> y holds not x <= y & not y <= x; end; registration let R be RelStr; cluster trivial -> stable for Subset of R; coherence proof let S be Subset of R; assume A1: S is trivial; let x, y being Element of R; thus thesis by A1,ZFMISC_1:def 10; end; end; registration let R be RelStr; cluster stable for Subset of R; existence proof reconsider A = {} as Subset of R by XBOOLE_1:2; take A; let x, y be Element of R; thus thesis; end; end; definition let R be RelStr; mode StableSet of R is stable Subset of R; :: other possible names: AntiChain of R, IndependentSet of R end; registration let R be RelStr; cluster finite for StableSet of R; existence proof take {}R; thus thesis; end; end; registration let R be non empty RelStr; cluster finite non empty for StableSet of R; existence proof {the Element of R} is stable; hence thesis; end; end; theorem :: AChain36a: for R being non empty RelStr, a1, a2 being Element of R st a1 <> a2 & {a1,a2} is StableSet of R holds not (a1 <= a2 or a2 <= a1) proof let R be non empty RelStr, a1,a2 be Element of R; assume A1: a1 <> a2; A2: a1 in {a1,a2} & a2 in {a1,a2} by TARSKI:def 2; assume {a1,a2} is StableSet of R; hence thesis by A2,A1,Def2; end; theorem Th14: :: AChain36b: for R being non empty RelStr, a1, a2 being Element of R st not (a1 <= a2 or a2 <= a1) holds {a1,a2} is StableSet of R proof let R be non empty RelStr, a1,a2 be Element of R; assume A1: not (a1 <= a2 or a2 <= a1); set S = {a1,a2}; S is stable proof let x, y be Element of R such that A2: x in S & y in S & x <> y; (x = a1 or x = a2) & (y = a1 or y = a2) by A2,TARSKI:def 2; hence thesis by A1,A2; end; hence thesis; end; theorem Th15: :: ACClique: for R being RelStr, C being Clique of R, A being StableSet of R, a, b being set st a in A & b in A & a in C & b in C holds a = b proof let R be RelStr, C be Clique of R, A be StableSet of R, a, b be set such that A1: a in A & b in A and A2: a in C & b in C; assume A3: a <> b; reconsider a9 = a, b9 = b as Element of R by A1; not a9 <= b9 & not b9 <= a9 by A1,A3,Def2; hence contradiction by A2,A3,Th6; end; theorem Th16: :: AChain0: for R being RelStr, A being StableSet of R, B being Subset of A holds B is StableSet of R proof let R be RelStr, A be StableSet of R, B be Subset of A; reconsider BB = B as Subset of R by XBOOLE_1:1; BB is stable proof let x, y be Element of R such that A1: x in BB & y in BB & x <> y; thus not x <= y & not y <= x by A1,Def2; end; hence thesis; end; theorem Th17: :: AChain1: for R being RelStr, A being finite StableSet of R, n being Nat st n <= card A ex B being finite StableSet of R st card B = n proof let R be RelStr, A be finite StableSet of R, n be Nat such that A1: n <= card A; consider BB being finite Subset of A such that A2: card BB = n by A1,FINSEQ_4:72; reconsider BB as finite StableSet of R by Th16; take BB; thus card BB = n by A2; end; begin :: Clique number and stability number definition let R be RelStr; attr R is with_finite_clique# means :Def3: ex C being finite Clique of R st for D being finite Clique of R holds card D <= card C; end; registration cluster finite -> with_finite_clique# for RelStr; coherence proof let R be RelStr; assume R is finite; then reconsider R9 = R as finite RelStr; defpred P[Nat] means ex c being finite Clique of R st card c = $1; A1: for k being Nat st P[k] holds k <= card R9 by NAT_1:43; card {}R = 0; then A2: ex k being Nat st P[k]; consider k being Nat such that A3: P[k] and A4: for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A1,A2); consider c being finite Clique of R such that A5: card c = k by A3; for D be finite Clique of R holds card(D) <= card(c) by A5,A4; hence R is with_finite_clique# by Def3; end; end; registration let R be with_finite_clique# RelStr; cluster -> finite for Clique of R; coherence proof let D be Clique of R; consider C being finite Clique of R such that A1: for D being finite Clique of R holds card(D) <= card(C) by Def3; assume D is infinite; then consider Y being finite Subset of D such that A2: card Y > card C by Th5; Y is Clique of R by Th9; hence contradiction by A2,A1; end; end; definition let R be with_finite_clique# RelStr; func clique# R -> Nat means :Def4: (ex C being finite Clique of R st card C = it) & for T being finite Clique of R holds card T <= it; existence proof consider A being finite Clique of R such that A1: for B being finite Clique of R holds card(B) <= card(A) by Def3; take itt = card A; thus ex A being finite Clique of R st card A = itt; let T being finite Clique of R; thus card T <= itt by A1; end; uniqueness proof let it1, it2 be Nat such that A2: ex S1 being finite Clique of R st card(S1) = it1 and A3: for T being finite Clique of R holds card(T) <= it1 and A4: ex S2 being finite Clique of R st card(S2) = it2 and A5: for T being finite Clique of R holds card(T) <= it2; consider S1 being finite Clique of R such that A6: card(S1) = it1 by A2; consider S2 being finite Clique of R such that A7: card(S2) = it2 by A4; it1 <= it2 & it2 <= it1 by A6,A7,A3,A5; hence it1 = it2 by XXREAL_0:1; end; end; registration let R be empty RelStr; cluster clique# R -> empty; coherence proof for T being Clique of R holds card T <= card {}R; hence thesis by Def4; end; end; registration let R be with_finite_clique# non empty RelStr; cluster clique# R -> positive; coherence proof card {the Element of R} <= clique# R by Def4; hence thesis; end; end; theorem :: Height3: for R being with_finite_clique# non empty RelStr st [#]R is StableSet of R holds clique# R = 1 proof let R be with_finite_clique# non empty RelStr; assume A1: [#]R is StableSet of R; A2: clique# R >= 0+1 by NAT_1:13; consider A being finite Clique of R such that A3: card A = clique# R by Def4; assume clique# R <> 1; then card A > 1 by A2,A3,XXREAL_0:1; then consider a, b being set such that A4: a in A and A5: b in A and A6: a <> b by NAT_1:59; thus thesis by A4,A5,A6,A1,Th15; end; theorem Th19: :: Height4: for R being with_finite_clique# RelStr st clique# R = 1 holds [#]R is StableSet of R proof let R be with_finite_clique# RelStr; assume A1: clique# R = 1; set cR = the carrier of R; A2: R is non empty by A1; now let a, b be Element of R such that a in cR and b in cR and A3: a <> b; assume a <= b or b <= a; then A4: {a,b} is Clique of R by A2,Th8; card {a,b} = 2 by A3,CARD_2:57; hence contradiction by A4,A1,Def4; end; hence [#]R is StableSet of R by Def2; end; definition let R be RelStr; attr R is with_finite_stability# means :Def5: ex A being finite StableSet of R st for B being finite StableSet of R holds card B <= card A; end; registration cluster finite -> with_finite_stability# for RelStr; coherence proof let R be RelStr; assume R is finite; then reconsider R9 = R as finite RelStr; defpred P[Nat] means ex A being finite StableSet of R9 st card A = $1; A1: for k being Nat st P[k] holds k <= card R9 by NAT_1:43; {}R is StableSet of R & card {} = 0; then A2: ex k being Nat st P[k]; consider k being Nat such that A3: P[k] and A4: for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A1, A2); consider S being finite StableSet of R such that A5: card S = k by A3; take S; let T be finite StableSet of R; thus card T <= card S by A5,A4; end; end; registration let R be with_finite_stability# RelStr; cluster -> finite for StableSet of R; coherence proof consider A being finite StableSet of R such that A1: for B being finite StableSet of R holds card(A) >= card(B) by Def5; given B being StableSet of R such that A2: B is infinite; consider C being finite Subset of B such that A3: card C > card A by A2,Th5; C is StableSet of R by Th16; hence contradiction by A1,A3; end; end; definition let R be with_finite_stability# RelStr; func stability# R -> Nat means :Def6: (ex A being finite StableSet of R st card(A) = it) & for T being finite StableSet of R holds card T <= it; existence proof consider A being finite StableSet of R such that A1: for B being finite StableSet of R holds card(A) >= card(B) by Def5; take itt = card A; thus ex A being finite StableSet of R st card A = itt; let T being finite StableSet of R; thus card(T) <= itt by A1; end; uniqueness proof let it1, it2 be Nat such that A2: ex S1 being finite StableSet of R st card S1 = it1 and A3: for T being finite StableSet of R holds card(T) <= it1 and A4: ex S2 being finite StableSet of R st card S2 = it2 and A5: for T being finite StableSet of R holds card(T) <= it2; consider S1 being finite StableSet of R such that A6: card S1 = it1 by A2; consider S2 being finite StableSet of R such that A7: card S2 = it2 by A4; it1 <= it2 & it2 <= it1 by A3,A5,A6,A7; hence it1 = it2 by XXREAL_0:1; end; end; registration let R be empty RelStr; cluster stability# R -> empty; coherence proof for T being StableSet of R holds card(T) <= card {}R; hence thesis by Def6; end; end; registration let R be with_finite_stability# non empty RelStr; cluster stability# R -> positive; coherence proof card{the Element of R} <= stability# R by Def6; hence thesis; end; end; theorem Th20: :: Width3: for R being with_finite_stability# non empty RelStr st [#]R is Clique of R holds stability# R = 1 proof let R be with_finite_stability# non empty RelStr; assume A1: [#]R is Clique of R; A2: stability# R >= 0+1 by NAT_1:13; consider A being finite StableSet of R such that A3: card(A) = stability# R by Def6; assume stability# R <> 1; then card A > 1 by A2,A3,XXREAL_0:1; then consider a, b being set such that A4: a in A and A5: b in A and A6: a <> b by NAT_1:59; thus thesis by A4,A5,A6,A1,Th15; end; theorem Th21: :: Width4: for R being with_finite_stability# RelStr st stability# R = 1 holds [#]R is Clique of R proof let R be with_finite_stability# RelStr; assume A1: stability# R = 1; set cR = the carrier of R; now let a, b be Element of R such that A2: a in cR and b in cR and A3: a <> b; A4: R is non empty by A2; assume not (a <= b or b <= a); then A5: {a,b} is StableSet of R by A4,Th14; card {a,b} = 2 by A3,CARD_2:57; hence contradiction by A1,Def6,A5; end; hence [#]R is Clique of R by Th6; end; registration :: I have done it through Ramsey. How else to prove it? :: For posets one gets it directly from Dilworth. :: Related: how big the gap between (clique# * stability#) and :: card of the carrier can be? cluster with_finite_clique# with_finite_stability# -> finite for RelStr; coherence proof let R be RelStr; assume A1: R is with_finite_clique#; assume A2: R is with_finite_stability#; assume A3: R is infinite; reconsider R as with_finite_clique# with_finite_stability# RelStr by A1,A2 ; consider C being finite Clique of R such that A4: card C = clique# R by Def4; consider An being finite StableSet of R such that A5: card(An) = stability# R by Def6; set h = clique# R, w = stability# R; A6: 0+1 <= h by A3,NAT_1:13; A7: 0+1 <= w by A3,NAT_1:13; set cR = the carrier of R; A8: cR = [#]R; per cases by A6,A7,XXREAL_0:1; suppose h = 1; then A9: cR is StableSet of R by A8,Th19; consider Y being finite Subset of cR such that A10: card Y > w by A3,Th5; Y is StableSet of R by A9,Th16; hence thesis by A10,Def6; end; suppose w = 1; then A11: cR is Clique of R by A8,Th21; consider Y being finite Subset of cR such that A12: card Y > h by A3,Th5; Y is Clique of R by A11,Th9; hence thesis by A12,Def4; end; suppose A13: h > 1 & w > 1; set m = max(clique# R, stability# R) +1; reconsider m as Nat; consider r being Nat such that A14: for X being finite set, P being a_partition of the_subsets_of_card(2,X) st card X >= r & card P = 2 holds ex S being Subset of X st card S >= m & S is_homogeneous_for P by RAMSEY_1:17; consider Y being finite Subset of R such that A15: card Y > r by A3,Th5; set X = Y \/ An \/ C; reconsider X as finite Subset of R; Y c= Y \/ An & Y \/ An c= Y \/ An \/ C by XBOOLE_1:7; then A16: card Y <= card X by NAT_1:43,XBOOLE_1:1; set A = { {x,y} where x,y is Element of R : x<>y & x in X & y in X & (x <= y or y <= x) }; set B = { {x,y} where x,y is Element of R : x<>y & x in X & y in X & not (x <= y or y <= x) }; set E = the_subsets_of_card(2,X); set P = { A, B }; A17: A c= E proof let x be set; assume x in A; then consider xx, yy being Element of R such that A18: {xx,yy} = x and A19: xx<>yy and A20: xx in X and A21: yy in X and xx <= yy or yy <= xx; x is Subset of X & card x = 2 by A18,A19,A20,A21,CARD_2:57,ZFMISC_1:32; hence thesis; end; A22: B c= E proof let x be set; assume x in B; then consider xx, yy being Element of R such that A23: {xx,yy} = x and A24: xx<>yy and A25: xx in X and A26: yy in X and not (xx <= yy or yy <= xx); x is Subset of X & card x = 2 by A23,A24,A25,A26,CARD_2:57,ZFMISC_1:32; hence thesis; end; A27: A in P & B in P by TARSKI:def 2; A28: now assume A29: A = B; consider a, b being set such that A30: a in An and A31: b in An and A32: a <> b by A13,A5,NAT_1:59; reconsider a, b as Element of R by A30,A31; A33: not (a <= b or b <= a) by A30,A31,A32,Def2; a in Y \/ An & b in Y \/ An by A30,A31,XBOOLE_0:def 3; then a in X & b in X by XBOOLE_0:def 3; then {a,b} in B by A33,A32; then consider aa, bb being Element of R such that A34: {a,b} = {aa, bb} and aa <> bb & aa in X & bb in X and A35: aa <= bb or bb <= aa by A29; a = aa & b = bb or a = bb & b = aa by A34,ZFMISC_1:6; hence contradiction by A35,A30,A31,A32,Def2; end; A36: P c= bool E proof let x be set; assume x in P; then x c= E by A17,A22,TARSKI:def 2; hence thesis; end; A37: union P = E proof thus union P c= E proof let x be set; assume x in union P; then consider Y being set such that A38: x in Y and A39: Y in P by TARSKI:def 4; Y = A or Y = B by A39,TARSKI:def 2; hence thesis by A38,A17,A22; end; thus E c= union P proof let x be set; assume x in E; then consider xx being Subset of X such that A40: x = xx and A41: card xx = 2; consider a, b being set such that A42: a <> b and A43: xx = {a,b} by A41,CARD_2:60; a in xx & b in xx by A43,TARSKI:def 2; then a in X & b in X; then reconsider a, b as Element of R; A44: a in xx & b in xx by A43,TARSKI:def 2; not (a <= b or b <= a) or (a <= b or b <= a); then {a,b} in A or {a,b} in B by A44,A42; hence x in union P by A40,A43,A27,TARSKI:def 4; end; end; for a being Subset of E st a in P holds a<>{} & for b being Subset of E st b in P holds a = b or a misses b proof let a be Subset of E such that A45: a in P; thus a<>{} proof per cases by A45,TARSKI:def 2; suppose A46: a = A; consider aa, bb being set such that A47: aa in C and A48: bb in C and A49: aa <> bb by A13,A4,NAT_1:59; reconsider aa, bb as Element of R by A47,A48; A50: aa <= bb or bb <= aa by A47,A48,A49,Th6; aa in Y \/ An \/ C & bb in Y \/ An \/ C by A47,A48,XBOOLE_0:def 3; then {aa,bb} in A by A50,A49; hence thesis by A46; end; suppose A51: a = B; consider aa, bb being set such that A52: aa in An and A53: bb in An and A54: aa <> bb by A13,A5,NAT_1:59; reconsider aa, bb as Element of R by A52,A53; A55: not (aa <= bb or bb <= aa) by A52,A53,A54,Def2; aa in Y \/ An & bb in Y \/ An by A52,A53,XBOOLE_0:def 3; then aa in X & bb in X by XBOOLE_0:def 3; then {aa,bb} in B by A55,A54; hence thesis by A51; end; end; let b be Subset of E such that A56: b in P; assume A57: a <> b; assume A58: a meets b; (a = A or a = B) & (b = A or b = B) by A45,A56,TARSKI:def 2; then A /\ B <> {} by A57,A58,XBOOLE_0:def 7; then consider x being set such that A59: x in A /\ B by XBOOLE_0:def 1; x in A by A59,XBOOLE_0:def 4; then consider xx, yy being Element of R such that A60: {xx,yy} = x and xx<>yy & xx in X & yy in X and A61: xx <= yy or yy <= xx; x in B by A59,XBOOLE_0:def 4; then consider x2, y2 being Element of R such that A62: {x2,y2} = x and x2<>y2 & x2 in X & y2 in X and A63: not (x2 <= y2 or y2 <= x2); xx = x2 & yy = y2 or xx = y2 & yy = x2 by A60,A62,ZFMISC_1:6; hence contradiction by A61,A63; end; then reconsider P as a_partition of E by A37,A36,EQREL_1:def 4; card P = 2 by A28,CARD_2:57; then consider S being Subset of X such that A64: card S >= m and A65: S is_homogeneous_for P by A16,A14,A15,XXREAL_0:2; reconsider S as finite Subset of R by XBOOLE_1:1; max(clique# R, stability# R) >= clique# R by XXREAL_0:25; then m > clique# R by NAT_1:13; then A66: card S > clique# R by A64,XXREAL_0:2; max(clique# R, stability# R) >= stability# R by XXREAL_0:25; then m > stability# R by NAT_1:13; then A67: card S > stability# R by A64,XXREAL_0:2; consider p being Element of P such that A68: the_subsets_of_card(2,S) c= p by A65,RAMSEY_1:def 1; per cases by TARSKI:def 2; suppose A69: p = A; now let x, y be Element of R such that A70: x in S and A71: y in S and A72: x <> y; {x,y} is Subset of S & card {x,y} = 2 by A70,A71,A72,CARD_2:57,ZFMISC_1:32; then {x,y} in the_subsets_of_card(2,S); then {x,y} in A by A69,A68; then consider xx, yy being Element of R such that A73: {xx,yy} = {x,y} and xx<>yy & xx in X & yy in X and A74: xx <= yy or yy <= xx; xx = x & yy = y or xx = y & yy = x by A73,ZFMISC_1:6; hence x <= y or y <= x by A74; end; then S is Clique of R by Th6; hence contradiction by A66,Def4; end; suppose A75: p = B; S is stable proof let x, y being Element of R such that A76: x in S and A77: y in S and A78: x <> y; {x,y} is Subset of S & card {x,y} = 2 by A76,A77,A78,CARD_2:57,ZFMISC_1:32; then {x,y} in the_subsets_of_card(2,S); then {x,y} in B by A75,A68; then consider xx, yy being Element of R such that A79: {xx,yy} = {x,y} and xx<>yy & xx in X & yy in X and A80: not (xx <= yy or yy <= xx); xx = x & yy = y or xx = y & yy = x by A79,ZFMISC_1:6; hence not x <= y & not y <= x by A80; end; hence contradiction by A67,Def6; end; end; end; end; begin :: Lower and upper sets, minimal and maximal elements definition let R be RelStr, X be Subset of R; func Lower X -> Subset of R equals X \/ downarrow X; coherence; func Upper X -> Subset of R equals X \/ uparrow X; coherence; end; theorem Th22: :: ABAC0: for R being antisymmetric transitive RelStr, A being StableSet of R, z being set st z in Upper A & z in Lower A holds z in A proof let R be antisymmetric transitive RelStr, A be StableSet of R, z be set such that A1: z in Upper A and A2: z in Lower A; per cases; suppose z in A; hence thesis; end; suppose A3: not z in A; then A4: z in uparrow A by A1,XBOOLE_0:def 3; A5: z in downarrow A by A2,A3,XBOOLE_0:def 3; reconsider y = z as Element of R by A1; consider x being Element of R such that A6: x <= y and A7: x in A by A4,WAYBEL_0:def 16; reconsider x9 = z as Element of R by A2; consider y9 being Element of R such that A8: x9 <= y9 and A9: y9 in A by A5,WAYBEL_0:def 15; x <= y9 by A6,A8,YELLOW_0:def 2; then x = y9 by A7,A9,Def2; hence z in A by A6,A7,A8,YELLOW_0:def 3; end; end; theorem Th23: :: ABunion: for R being with_finite_stability# RelStr, A being StableSet of R st card A = stability# R holds Upper A \/ Lower A = [#]R proof let R be with_finite_stability# RelStr, A be StableSet of R such that A1: card A = stability# R; set cP = the carrier of R; cP c= Upper A \/ Lower A proof let x be set; assume A2: x in cP; assume A3: not x in Upper A \/ Lower A; reconsider x as Element of cP by A2; A4: not x in Upper A by A3,XBOOLE_0:def 3; then A5: not x in A by XBOOLE_0:def 3; A6: not x in uparrow A by A4,XBOOLE_0:def 3; not x in Lower A by A3,XBOOLE_0:def 3; then A7: not x in downarrow A by XBOOLE_0:def 3; set Ax = A \/ {x}; A8: {x} c= the carrier of R by A2,ZFMISC_1:31; now let a, b be Element of R such that A9: a in Ax and A10: b in Ax and A11: a <> b; per cases by A9,A10,XBOOLE_0:def 3; suppose a in A & b in A; hence not a <= b & not b <= a by A11,Def2; end; suppose A12: a in A & b in {x}; then b = x by TARSKI:def 1; hence not a <= b & not b <= a by A6,A7,A12,WAYBEL_0:def 15,def 16 ; end; suppose A13: a in {x} & b in A; then a = x by TARSKI:def 1; hence not a <= b & not b <= a by A6,A7,A13,WAYBEL_0:def 15,def 16 ; end; suppose a in {x} & b in {x}; then a = x & b = x by TARSKI:def 1; hence not a <= b & not b <= a by A11; end; end; then A14: Ax is StableSet of R by A8,Def2,XBOOLE_1:8; card Ax = card A + 1 by A5,CARD_2:41; then card Ax > card A by NAT_1:13; hence contradiction by Def6,A1,A14; end; hence Upper A \/ Lower A = [#]R by XBOOLE_0:def 10; end; theorem Th24: :: Pminmin: for R being transitive RelStr, x being Element of R, S being Subset of R st x is_minimal_in Lower S holds x is_minimal_in [#]R proof let R be transitive RelStr, x be Element of R, S be Subset of R such that A1: x is_minimal_in Lower S; set cR = the carrier of R; A2: x in Lower S by A1,WAYBEL_4:56; assume not x is_minimal_in [#]R; then consider y being Element of R such that y in cR and A3: y < x by A2,WAYBEL_4:56; per cases by A2,XBOOLE_0:def 3; suppose A4: x in S; y <= x by A3,ORDERS_2:def 6; then y in downarrow S by A4,WAYBEL_0:def 15; then y in Lower S by XBOOLE_0:def 3; hence thesis by A1,A3,WAYBEL_4:56; end; suppose x in downarrow S; then consider x99 being Element of R such that A5: x <= x99 and A6: x99 in S by WAYBEL_0:def 15; y <= x by A3,ORDERS_2:def 6; then y <= x99 by A5,YELLOW_0:def 2; then y in downarrow S by A6,WAYBEL_0:def 15; then y in Lower S by XBOOLE_0:def 3; hence contradiction by A1,A3,WAYBEL_4:56; end; end; theorem Th25: :: Pmaxmax: for R being transitive RelStr, x being Element of R, S being Subset of R st x is_maximal_in Upper S holds x is_maximal_in [#]R proof let R be transitive RelStr, x be Element of R, S be Subset of R such that A1: x is_maximal_in Upper S; set cR = the carrier of R; A2: x in Upper S by A1,WAYBEL_4:55; assume not x is_maximal_in [#]R; then consider y being Element of R such that y in cR and A3: x < y by A2,WAYBEL_4:55; per cases by A2,XBOOLE_0:def 3; suppose A4: x in S; x <= y by A3,ORDERS_2:def 6; then y in uparrow S by A4,WAYBEL_0:def 16; then y in Upper S by XBOOLE_0:def 3; hence thesis by A1,A3,WAYBEL_4:55; end; suppose x in uparrow S; then consider x99 being Element of R such that A5: x99 <= x and A6: x99 in S by WAYBEL_0:def 16; x <= y by A3,ORDERS_2:def 6; then x99 <= y by A5,YELLOW_0:def 2; then y in uparrow S by A6,WAYBEL_0:def 16; then y in Upper S by XBOOLE_0:def 3; hence contradiction by A1,A3,WAYBEL_4:55; end; end; definition let R be RelStr; set cR = the carrier of R; func minimals R -> Subset of R means :Def9: for x being Element of R holds x in it iff x is_minimal_in [#]R if R is non empty otherwise it = {}; consistency; existence proof defpred P[set] means ex a being Element of R st a = $1 & a is_minimal_in cR; consider X being set such that A1: for x being set holds x in X iff x in cR & P[x] from XBOOLE_0:sch 1; A2: now assume A3: cR is non empty; for x being set st x in X holds x in cR by A1; then reconsider X as Subset of R by TARSKI:def 3; take X; let x be Element of R; x in X implies P[x] by A1; hence x in X iff x is_minimal_in cR by A1,A3; end; now reconsider X = {} as Subset of R by XBOOLE_1:2; take X; thus X = {}; end; hence thesis by A2; end; uniqueness proof let it1, it2 be Subset of R; now assume that R is non empty and A4: for x being Element of R holds x in it1 iff x is_minimal_in cR and A5: for x being Element of R holds x in it2 iff x is_minimal_in cR; now let x be set; now assume A6: x in it1 or x in it2; then reconsider x9 = x as Element of R; x9 is_minimal_in cR by A6,A4,A5; hence x in it1 & x in it2 by A4,A5; end; hence x in it1 iff x in it2; end; hence it1 = it2 by TARSKI:1; end; hence thesis; end; func maximals R -> Subset of R means :Def10: for x being Element of R holds x in it iff x is_maximal_in [#]R if R is non empty otherwise it = {}; consistency; existence proof defpred P[set] means ex a being Element of R st a = $1 & a is_maximal_in cR; consider X being set such that A7: for x being set holds x in X iff x in cR & P[x] from XBOOLE_0:sch 1; A8: now assume A9: cR is non empty; for x being set st x in X holds x in cR by A7; then reconsider X as Subset of R by TARSKI:def 3; take X; let x be Element of R; x in X implies P[x] by A7; hence x in X iff x is_maximal_in cR by A7,A9; end; now reconsider X = {} as Subset of R by XBOOLE_1:2; take X; thus X = {}; end; hence thesis by A8; end; uniqueness proof let it1, it2 be Subset of R; now assume that R is non empty and A10: for x being Element of R holds x in it1 iff x is_maximal_in cR and A11: for x being Element of R holds x in it2 iff x is_maximal_in cR; now let x be set; now assume A12: x in it1 or x in it2; then reconsider x9 = x as Element of R; x9 is_maximal_in cR by A12,A10,A11; hence x in it1 & x in it2 by A10,A11; end; hence x in it1 iff x in it2; end; hence it1 = it2 by TARSKI:1; end; hence thesis; end; end; registration let R be with_finite_clique# non empty antisymmetric transitive RelStr; cluster maximals R -> non empty; coherence proof set cP = the carrier of R, iP = the InternalRel of R; consider CL being finite Clique of R such that A1: for D being finite Clique of R holds card(D) <= card(CL) by Def3; card {the Element of R} <= card CL by A1; then CL <> {}; then consider y being Element of R such that y in CL and A2: y is_maximal_wrt CL, iP by BAGORDER:6; A3: y is_maximal_in CL by A2,WAYBEL_4:def 24; A4: cP = [#]R; now assume not y is_maximal_in cP; then consider z being Element of R such that z in cP and A5: y < z by WAYBEL_4:55; A6: y <= z by A5,ORDERS_2:def 6; set C = CL \/ {z}; reconsider C as finite Clique of R by A6,A3,Th11; not z in CL by A3,A5,WAYBEL_4:55; then card C = card CL + 1 by CARD_2:41; then card CL + 1 <= card CL + 0 by A1; hence contradiction by XREAL_1:6; end; hence thesis by A4,Def10; end; cluster minimals R -> non empty; coherence proof set cP = the carrier of R, iP = the InternalRel of R; consider CL being finite Clique of R such that A7: for D being finite Clique of R holds card(D) <= card(CL) by Def3; card {the Element of R} <= card CL by A7; then CL <> {}; then consider y being Element of R such that y in CL and A8: y is_minimal_wrt CL, iP by BAGORDER:7; A9: y is_minimal_in CL by A8,WAYBEL_4:def 26; A10: cP = [#]R; now assume not y is_minimal_in cP; then consider z being Element of R such that z in cP and A11: z < y by WAYBEL_4:56; A12: z <= y by A11,ORDERS_2:def 6; set C = CL \/ {z}; reconsider C as finite Clique of R by A12,A9,Th12; not z in CL by A9,A11,WAYBEL_4:56; then card C = card CL + 1 by CARD_2:41; then card CL + 1 <= card CL + 0 by A7; hence contradiction by XREAL_1:6; end; hence thesis by A10,Def9; end; end; registration let R be RelStr; cluster minimals R -> stable; coherence proof set mR = minimals R; let x, y be Element of R such that A1: x in mR and A2: y in mR and A3: x <> y; A4: R is non empty by A1; then y is_minimal_in [#]R by A2,Def9; then not y > x by A1,WAYBEL_4:56; hence not x <= y by A3,ORDERS_2:def 6; x is_minimal_in [#]R by A1,A4,Def9; then not x > y by A2,WAYBEL_4:56; hence not y <= x by A3,ORDERS_2:def 6; end; cluster maximals R -> stable; coherence proof set mR = maximals R; let x, y be Element of R such that A5: x in mR and A6: y in mR and A7: x <> y; A8: R is non empty by A5; then x is_maximal_in [#]R by A5,Def10; then not y > x by A6,WAYBEL_4:55; hence not x <= y by A7,ORDERS_2:def 6; y is_maximal_in [#]R by A6,A8,Def10; then not x > y by A5,WAYBEL_4:55; hence not y <= x by A7,ORDERS_2:def 6; end; end; theorem Th26: :: PCAamin: for R being RelStr, A being StableSet of R st not minimals R c= A holds not minimals R c= Upper A proof let R be RelStr, A be StableSet of R; assume not minimals R c= A; then consider x being set such that A1: x in minimals R and A2: not x in A by TARSKI:def 3; assume A3: minimals R c= Upper A; reconsider x9 = x as Element of R by A1; R is non empty by A1; then A4: x9 is_minimal_in [#]R by A1,Def9; x9 in uparrow A by A2,A1,A3,XBOOLE_0:def 3; then consider x99 being Element of R such that A5: x99 <= x9 and A6: x99 in A by WAYBEL_0:def 16; now assume x99 <> x9; then x99 < x9 by A5,ORDERS_2:def 6; hence contradiction by A1,A4,WAYBEL_4:56; end; hence contradiction by A6,A2; end; theorem Th27: :: PCAbmax: for R being RelStr, A being StableSet of R st not maximals R c= A holds not maximals R c= Lower A proof let R be RelStr, A be StableSet of R such that A1: not maximals R c= A; consider x being set such that A2: x in maximals R and A3: not x in A by A1,TARSKI:def 3; assume A4: maximals R c= Lower A; reconsider x9 = x as Element of R by A2; R is non empty by A2; then A5: x9 is_maximal_in [#]R by A2,Def10; x9 in downarrow A by A3,A2,A4,XBOOLE_0:def 3; then consider x99 being Element of R such that A6: x9 <= x99 and A7: x99 in A by WAYBEL_0:def 15; now assume x99 <> x9; then x9 < x99 by A6,ORDERS_2:def 6; hence contradiction by A2,A5,WAYBEL_4:55; end; hence contradiction by A7,A3; end; begin :: Substructures registration let R be RelStr, X be finite Subset of R; cluster subrelstr X -> finite; coherence by YELLOW_0:def 15; end; theorem Th28: :: SPClique: for R being RelStr, S being Subset of R, C being Clique of subrelstr S holds C is Clique of R proof let R be RelStr, S be Subset of R, C be Clique of subrelstr S; A1: the carrier of subrelstr S = S by YELLOW_0:def 15; now let a, b be Element of R such that A2: a in C and A3: b in C and A4: a <> b; reconsider a9 = a, b9 = b as Element of subrelstr S by A2,A3; a9 <= b9 or b9 <= a9 by A2,A3,A4,Th6; hence a <= b or b <= a by YELLOW_0:59; end; hence C is Clique of R by A1,Th6,XBOOLE_1:1; end; theorem Th29: :: SPClique1: for R being RelStr, S being Subset of R, C being Clique of R holds C /\ S is Clique of subrelstr S proof let R be RelStr, S be Subset of R, C be Clique of R; set sS = subrelstr S, CS = C /\ S; A1: CS c= S by XBOOLE_1:17; A2: S = the carrier of sS by YELLOW_0:def 15; now let a, b be Element of sS; assume A3: a in CS; assume A4: b in CS; assume A5: a <> b; A6: a in S & b in S by A3,A4,XBOOLE_0:def 4; A7: S is non empty by A3; R is non empty by A3; then reconsider a9 = a, b9 = b as Element of R by A7,YELLOW_0:58; a9 in C & b9 in C by A3,A4,XBOOLE_0:def 4; then a9 <= b9 or b9 <= a9 by A5,Th6; hence a <= b or b <= a by A6,A2,YELLOW_0:60; end; hence C /\ S is Clique of subrelstr S by Th6,A1,YELLOW_0:def 15; end; theorem Th30: :: SPAChain1: for R being RelStr, S being Subset of R, A being StableSet of subrelstr S holds A is StableSet of R proof let R be RelStr, S be Subset of R, A be StableSet of subrelstr S; set sS = subrelstr S; per cases; suppose R is empty; then the carrier of sS = {} by YELLOW_0:def 15; then A = {}R; hence A is StableSet of R; end; suppose A1: R is non empty; per cases; suppose S is empty; then the carrier of sS = {} by YELLOW_0:def 15; then A = {}R; hence A is StableSet of R; end; suppose A2: S is non empty; S = the carrier of sS by YELLOW_0:def 15; then reconsider A as Subset of R by XBOOLE_1:1; A is stable proof let x, y be Element of R such that A3: x in A and A4: y in A and A5: x <> y; reconsider x9 = x, y9 = y as Element of sS by A3,A4; not x9 <= y9 & not y9 <= x9 by A3,A4,A5,Def2; hence not x <= y & not y <= x by A1,A2,YELLOW_0:60; end; hence thesis; end; end; end; theorem Th31: :: SPAChain: for R being RelStr, S being Subset of R, A being StableSet of R holds A /\ S is StableSet of subrelstr S proof let R be RelStr, S be Subset of R, A be StableSet of R; set sS = subrelstr S, AS = A /\ S; per cases; suppose R is empty; then A /\ S = {}sS; hence A /\ S is StableSet of sS; end; suppose A1: R is non empty; per cases; suppose S is empty; then A /\ S = {}sS; hence A /\ S is StableSet of sS; end; suppose A2: S is non empty; S = the carrier of sS by YELLOW_0:def 15; then reconsider AS as Subset of sS by XBOOLE_1:17; AS is stable proof let x, y be Element of sS such that A3: x in AS and A4: y in AS and A5: x <> y; reconsider x9 = x, y9 = y as Element of R by A1,A2,YELLOW_0:58; A6: x9 in A by A3,XBOOLE_0:def 4; y9 in A by A4,XBOOLE_0:def 4; then not x9 <= y9 & not y9 <= x9 by A6,A5,Def2; hence not x <= y & not y <= x by YELLOW_0:59; end; hence A /\ S is StableSet of sS; end; end; end; theorem Th32: :: SPmax for R being RelStr, S being Subset of R, B being Subset of subrelstr S, x being Element of subrelstr S, y being Element of R st x = y & x is_maximal_in B holds y is_maximal_in B proof let R be RelStr, S be Subset of R, B be Subset of subrelstr S, x be Element of subrelstr S, y be Element of R such that A1: x = y and A2: x is_maximal_in B; A3: x in B by A2,WAYBEL_4:55; assume not y is_maximal_in B; then consider z being Element of R such that A4: z in B and A5: y < z by A1,A3,WAYBEL_4:55; A6: y <= z by A5,ORDERS_2:def 6; reconsider z9 = z as Element of subrelstr S by A4; x <= z9 by A4,A6,A1,YELLOW_0:60; then x < z9 by A5,A1,ORDERS_2:def 6; hence contradiction by A4,A2,WAYBEL_4:55; end; theorem Th33: :: SPmin for R being RelStr, S being Subset of R, B being Subset of subrelstr S, x being Element of subrelstr S, y being Element of R st x = y & x is_minimal_in B holds y is_minimal_in B proof let R be RelStr, S be Subset of R, B be Subset of subrelstr S, x be Element of subrelstr S, y be Element of R such that A1: x = y and A2: x is_minimal_in B; A3: x in B by A2,WAYBEL_4:56; assume not y is_minimal_in B; then consider z being Element of R such that A4: z in B and A5: z < y by A1,A3,WAYBEL_4:56; A6: z <= y by A5,ORDERS_2:def 6; reconsider z9 = z as Element of subrelstr S by A4; z9 <= x by A4,A6,A1,YELLOW_0:60; then z9 < x by A5,A1,ORDERS_2:def 6; hence contradiction by A4,A2,WAYBEL_4:56; end; theorem Th34: :: PbeSmax: for R being transitive RelStr, A being StableSet of R, C being Clique of subrelstr Lower A, a, b being Element of R st a in A & a in C & b in C holds a = b or b <= a proof let R be transitive RelStr, A be StableSet of R, C be Clique of subrelstr Lower A, a, b be Element of R such that A1: a in A and A2: a in C and A3: b in C; set ap = subrelstr Lower A; reconsider a9 = a as Element of ap by A2; A4: b in the carrier of ap by A3; reconsider b9 = b as Element of ap by A3; A5: b9 in Lower A by A4,YELLOW_0:def 15; A6: C is Clique of R by Th28; per cases by A5,XBOOLE_0:def 3; suppose b9 in A; hence thesis by A1,A2,A3,A6,Th15; end; suppose b9 in downarrow A; then consider c being Element of R such that A7: b <= c and A8: c in A by WAYBEL_0:def 15; per cases; suppose A9: a <> b; per cases by A9,A2,A3,Th6; suppose a9 <= b9; then a <= b by YELLOW_0:59; then a <= c by A7,YELLOW_0:def 2; hence thesis by A8,A7,A1,Def2; end; suppose b9 <= a9; hence thesis by YELLOW_0:59; end; end; suppose a = b; hence thesis; end; end; end; theorem Th35: :: PabSmin: for R being transitive RelStr, A being StableSet of R, C being Clique of subrelstr Upper A, a, b being Element of R st a in A & a in C & b in C holds a = b or a <= b proof let R be transitive RelStr, A be StableSet of R, C be Clique of subrelstr Upper A, a, b be Element of R such that A1: a in A and A2: a in C and A3: b in C; set ap = subrelstr Upper A; reconsider a9 = a as Element of ap by A2; A4: b in the carrier of ap by A3; reconsider b9 = b as Element of ap by A3; A5: b9 in Upper A by A4,YELLOW_0:def 15; A6: C is Clique of R by Th28; per cases by A5,XBOOLE_0:def 3; suppose b9 in A; hence thesis by A1,A2,A3,A6,Th15; end; suppose b9 in uparrow A; then consider c being Element of R such that A7: c <= b and A8: c in A by WAYBEL_0:def 16; per cases; suppose A9: a <> b; per cases by A9,A2,A3,Th6; suppose a9 <= b9; hence thesis by YELLOW_0:59; end; suppose b9 <= a9; then b <= a by YELLOW_0:59; then c <= a by A7,YELLOW_0:def 2; hence thesis by A8,A7,A1,Def2; end; end; suppose a = b; hence thesis; end; end; end; registration let R be with_finite_clique# RelStr, S be Subset of R; cluster subrelstr S -> with_finite_clique#; coherence proof consider C being finite Clique of R such that A1: for D being finite Clique of R holds card(D) <= card(C) by Def3; set sS = subrelstr S; defpred P[Nat] means ex c being finite Clique of sS st card c = $1; A2: for k being Nat st P[k] holds k <= card C proof let k be Nat; assume P[k]; then consider c being finite Clique of sS such that A3: card c = k; c is finite Clique of R by Th28; hence thesis by A3,A1; end; card {}sS = 0; then A4: ex k being Nat st P[k]; consider k being Nat such that A5: P[k] and A6: for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A2,A4); consider c being finite Clique of sS such that A7: card c = k by A5; for D being finite Clique of sS holds card(D) <= card(c) by A7,A6; hence sS is with_finite_clique# by Def3; end; end; registration let R be with_finite_stability# RelStr, S be Subset of R; cluster subrelstr S -> with_finite_stability#; coherence proof consider A being finite StableSet of R such that A1: for B being finite StableSet of R holds card(A) >= card(B) by Def5; assume A2: not subrelstr S is with_finite_stability#; defpred P[Nat] means ex C being finite StableSet of subrelstr S st card C = $1 & ex B being finite StableSet of subrelstr S st $1 < card(B); A3: P[0] proof reconsider C = {}(subrelstr S) as finite StableSet of subrelstr S; take C; thus card C = 0; hence thesis by A2,Def5; end; A4: for n being Nat st P[n] holds P[n+1] proof let n be Nat; given C being finite StableSet of subrelstr S such that card C = n and A5: ex B being finite StableSet of subrelstr S st n < card(B); consider B being finite Subset of subrelstr S such that A6: n < card(B) & B is StableSet of subrelstr S by A5; n+1 <= card B by A6,NAT_1:13; then consider BB being finite StableSet of subrelstr S such that A7: card BB = n+1 by A6,Th17; take BB; thus card BB = n+1 by A7; consider Bb being finite StableSet of subrelstr S such that A8: card BB < card(Bb) by A2,Def5; take Bb; thus n+1 < card Bb by A8,A7; end; for n being Nat holds P[n] from NAT_1:sch 2(A3,A4); then consider C being finite StableSet of subrelstr S such that card C = card A and A9: ex B being finite StableSet of subrelstr S st card A < card(B); consider B being finite StableSet of subrelstr S such that A10: card A < card(B) by A9; B is StableSet of R by Th30; hence contradiction by A1,A10; end; end; theorem Th36: :: Pmaxmin: for R being with_finite_clique# non empty antisymmetric transitive RelStr, x being Element of R holds ex y being Element of R st y is_minimal_in [#]R & (y = x or y < x) proof let R be with_finite_clique# non empty antisymmetric transitive RelStr, x be Element of R; set sx = Lower {x}; set sL = subrelstr sx; reconsider sL as with_finite_clique# non empty antisymmetric transitive RelStr; consider y being set such that A1: y in minimals sL by XBOOLE_0:def 1; reconsider y as Element of sL by A1; A2: [#]sL = sx by YELLOW_0:def 15; then A3: y is_minimal_in sx by A1,Def9; reconsider y9 = y as Element of R by YELLOW_0:58; take y9; sx c= the carrier of sL by YELLOW_0:def 15; hence y9 is_minimal_in [#]R by A3,Th33,Th24; per cases; suppose y9 = x; hence thesis; end; suppose y9 <> x; then not y9 in {x} by TARSKI:def 1; then y9 in downarrow x by A2,XBOOLE_0:def 3; then y9 <= x by WAYBEL_0:17; hence thesis by ORDERS_2:def 6; end; end; theorem :: Pam: for R being with_finite_clique# antisymmetric transitive RelStr holds Upper minimals R = [#]R proof let R being with_finite_clique# antisymmetric transitive RelStr; set ap = Upper minimals R; set cR = the carrier of R; cR c= ap proof let x be set; assume A1: x in cR; then reconsider x9 = x as Element of R; A2: R is non empty by A1; then consider y being Element of R such that A3: y is_minimal_in [#]R and A4: y = x9 or y < x9 by Th36; A5: y in minimals R by A3,A2,Def9; per cases by A4; suppose x9 = y; hence thesis by A5,XBOOLE_0:def 3; end; suppose y < x9; then y <= x9 by ORDERS_2:def 6; then x in uparrow minimals R by A5,WAYBEL_0:def 16; hence x in ap by XBOOLE_0:def 3; end; end; hence thesis by XBOOLE_0:def 10; end; theorem Th38: :: Pminmax for R being with_finite_clique# non empty antisymmetric transitive RelStr, x being Element of R ex y being Element of R st y is_maximal_in [#]R & (y = x or x < y) proof let R be with_finite_clique# non empty antisymmetric transitive RelStr, x be Element of R; set ax = Upper {x}; set sU = subrelstr ax; reconsider sU as with_finite_clique# non empty antisymmetric transitive RelStr; consider y being set such that A1: y in maximals sU by XBOOLE_0:def 1; reconsider y as Element of sU by A1; A2: [#]sU = ax by YELLOW_0:def 15; then A3: y is_maximal_in ax by A1,Def10; reconsider y9 = y as Element of R by YELLOW_0:58; take y9; ax c= the carrier of sU by YELLOW_0:def 15; hence y9 is_maximal_in [#]R by A3,Th32,Th25; per cases; suppose y9 = x; hence thesis; end; suppose y9 <> x; then not y9 in {x} by TARSKI:def 1; then y9 in uparrow x by A2,XBOOLE_0:def 3; then x <= y9 by WAYBEL_0:18; hence thesis by ORDERS_2:def 6; end; end; theorem :: Pbm: for R being with_finite_clique# antisymmetric transitive RelStr holds Lower maximals R = [#]R proof let P being with_finite_clique# antisymmetric transitive RelStr; set ap = Lower maximals P; set cP = the carrier of P; cP c= ap proof let x be set; assume A1: x in cP; then reconsider x9 = x as Element of P; A2: P is non empty by A1; then consider y being Element of P such that A3: y is_maximal_in [#]P and A4: y = x9 or y > x9 by Th38; A5: y in maximals P by A3,A2,Def10; per cases by A4; suppose x9 = y; hence thesis by A5,XBOOLE_0:def 3; end; suppose y > x9; then x9 <= y by ORDERS_2:def 6; then x in downarrow maximals P by A5,WAYBEL_0:def 15; hence x in ap by XBOOLE_0:def 3; end; end; hence thesis by XBOOLE_0:def 10; end; theorem Th40: :: PCAmin: for R being with_finite_clique# antisymmetric transitive RelStr, A being StableSet of R st minimals R c= A holds A = minimals R proof let R be with_finite_clique# antisymmetric transitive RelStr, A be StableSet of R such that A1: minimals R c= A; A c= minimals R proof let x be set; assume A2: x in A; then A3: R is non empty; reconsider x9 = x as Element of R by A2; consider y being Element of R such that A4: y is_minimal_in [#]R and A5: y = x9 or y < x9 by A3,Th36; A6: y = x9 or y <= x9 by A5,ORDERS_2:def 6; y in minimals R by A3,A4,Def9; hence x in minimals R by A1,A2,A6,Def2; end; hence A = minimals R by A1,XBOOLE_0:def 10; end; theorem Th41: :: PCAmax: for R being with_finite_clique# antisymmetric transitive RelStr, A being StableSet of R st maximals R c= A holds A = maximals R proof let R be with_finite_clique# antisymmetric transitive RelStr, A be StableSet of R such that A1: maximals R c= A; A c= maximals R proof let x be set; assume A2: x in A; then A3: R is non empty; reconsider x9 = x as Element of R by A2; consider y being Element of R such that A4: y is_maximal_in [#]R and A5: y = x9 or x9 < y by A3,Th38; A6: y = x9 or x9 <= y by A5,ORDERS_2:def 6; y in maximals R by A3,A4,Def10; hence x in maximals R by A1,A2,A6,Def2; end; hence A = maximals R by A1,XBOOLE_0:def 10; end; theorem Th42: :: Hsubp0: for R being with_finite_clique# RelStr, S being Subset of R holds clique# subrelstr S <= clique# R proof let R be with_finite_clique# RelStr, S be Subset of R; set s = subrelstr S; consider c being finite Clique of s such that A1: card c = clique# s by Def4; c is Clique of R by Th28; hence clique# subrelstr S <= clique# R by Def4,A1; end; theorem :: Hsubp1: for R being with_finite_clique# RelStr, C being Clique of R, S being Subset of R st card C = clique# R & C c= S holds clique# subrelstr S = clique# R proof let R be with_finite_clique# RelStr, C be Clique of R, S be Subset of R such that A1: card C = clique# R and A2: C c= S; C = C /\ S by A2,XBOOLE_1:28; then A3: C is Clique of subrelstr S by Th29; consider Cs being Clique of subrelstr S such that A4: card(Cs) = clique# subrelstr S by Def4; A5: card C <= card Cs by A3,A4,Def4; clique# subrelstr S <= clique# R by Th42; hence clique# subrelstr S = clique# R by A4,A1,A5,XXREAL_0:1; end; theorem Th44: :: Wsubp0: for R being with_finite_stability# RelStr, S being Subset of R holds stability# subrelstr S <= stability# R proof let R be with_finite_stability# RelStr, S be Subset of R; consider As being StableSet of subrelstr S such that A1: card(As) = stability# subrelstr S by Def6; As is StableSet of R by Th30; hence stability# subrelstr S <= stability# R by A1,Def6; end; theorem Th45: :: Wsubp1: for R being with_finite_stability# RelStr, A being StableSet of R, S being Subset of R st card A = stability# R & A c= S holds stability# subrelstr S = stability# R proof let R be with_finite_stability# RelStr, A be StableSet of R, S be Subset of R such that A1: card A = stability# R and A2: A c= S; A = A /\ S by A2,XBOOLE_1:28; then A3: A is StableSet of subrelstr S by Th31; consider As being StableSet of subrelstr S such that A4: card(As) = stability# subrelstr S by Def6; A5: card A <= card As by A3,A4,Def6; stability# subrelstr S <= stability# R by Th44; hence stability# subrelstr S = stability# R by A4,A1,A5,XXREAL_0:1; end; begin :: Partitions into cliques and stable sets definition let R be RelStr, P be a_partition of the carrier of R; attr P is Clique-wise means :Def11: for x being set st x in P holds x is Clique of R; end; registration let R be RelStr; cluster Clique-wise for a_partition of the carrier of R; existence proof set cR = the carrier of R; per cases; suppose R is empty; then reconsider S = {} as a_partition of cR by EQREL_1:45; take S ; thus for x being set st x in S holds x is Clique of R; end; suppose A1: R is non empty; take S = SmallestPartition cR; let z being set; assume A2: z in S; S = {{x} where x is Element of cR: not contradiction} by A1,EQREL_1:37; then consider x being Element of cR such that A3: z = {x} and not contradiction by A2; thus z is Clique of R by A3,A1,SUBSET_1:33; end; 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 proof let P be a_partition of the carrier of R such that P is empty; let x be set; thus thesis; end; end; theorem Th46: :: Chpw: for R being finite RelStr, C being Clique-partition of R holds card C >= stability# R proof let R be finite RelStr, C be Clique-partition of R; assume A1: card(C) < stability# R; consider A being StableSet of R such that A2: card A = stability# R by Def6; card card C = card C & card card A = card A; then A3: card C in card A by A1,A2,NAT_1:41; set cR = the carrier of R; per cases; suppose R is empty; hence contradiction by A1; end; suppose A4: R is non empty; defpred P[set,set] means $1 in A & $2 in C & $1 in $2; A5: for x being set st x in A ex y being set st y in C & P[x,y] proof let x be set such that A6: x in A; reconsider x9 = x as Element of R by A6; cR is non empty by A4; then x9 in cR; then x in union C by EQREL_1:def 4; then consider y being set such that A7: x in y and A8: y in C by TARSKI:def 4; take y; thus thesis by A6,A7,A8; end; consider f being Function of A, C such that A9: for x being set st x in A holds P[x,f.x] from FUNCT_2:sch 1(A5); consider x,y being set such that A10: x in A and A11: y in A and A12: x <> y and A13: f.x = f.y by A4,A3,FINSEQ_4:65; f.x in C by A10,FUNCT_2:5; then A14: f.x is Clique of R by Def11; x in f.x & y in f.x by A13,A10,A11,A9; hence contradiction by A14,A10,A11,A12,Th15; end; end; theorem Th47: :: ACpart1: for R being with_finite_stability# RelStr, A being StableSet of R, C being Clique-partition of R st card C = card A 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 let R be with_finite_stability# RelStr, A be StableSet of R, C be Clique-partition of R; assume that A1: card C = card A; set cR = the carrier of R; per cases; suppose A2: R is empty; then the carrier of R is empty; then A3: C = {} by EQREL_1:32; set f = the Function of A, C; dom f = {} by A2; then reconsider f = {} as Function of A, C by RELAT_1:41; A4: f is onto by A3,FUNCT_2:def 3,RELAT_1:38; take f; thus f is bijective by A4; thus thesis; end; suppose A5: R is non empty; defpred P[set,set] means $1 in A & $2 in C & $1 in $2; A6: for x being set st x in A ex y being set st y in C & P[x,y] proof let x be set; assume A7: x in A; then reconsider x9 = x as Element of R; cR is non empty by A5; then x9 in cR; then x9 in union C by EQREL_1:def 4; then consider y being set such that A8: x in y and A9: y in C by TARSKI:def 4; take y; thus thesis by A7,A8,A9; end; consider f being Function of A, C such that A10: for x being set st x in A holds P[x,f.x] from FUNCT_2:sch 1(A6); take f; A11: f is one-to-one proof let x1,x2 be set such that A12: x1 in dom f and A13: x2 in dom f and A14: f.x1 = f.x2; A15: x1 in f.x1 by A12,A10; A16: x2 in f.x2 by A13,A10; f.x1 in C by A5,A12,FUNCT_2:5; then f.x1 is Clique of R by Def11; hence x1 = x2 by A12,A13,A15,A16,A14,Th15; end; C is finite by A1; then rng f = C by A1,A11,FINSEQ_4:63; then f is onto by FUNCT_2:def 3; hence f is bijective by A11; let x be set; assume x in A; hence x in f.x by A10; end; end; theorem Th48: :: ACpart2: for R being finite RelStr, A being StableSet of R, C being Clique-partition of R st card C = card A for c being set st c in C ex a being Element of A st c /\ A = {a} proof let R be finite RelStr, A be StableSet of R, C be Clique-partition of R such that A1: card C = card A; consider f being Function of A, C such that A2: f is bijective and A3: for x being set st x in A holds x in f.x by A1,Th47; let c be set such that A4: c in C; rng f = C by A2,FUNCT_2:def 3; then consider x being set such that A5: x in dom f and A6: c = f.x by A4,FUNCT_1:def 3; A7: x in c by A5,A6,A3; reconsider a = x as Element of A by A5; take a; now let z be set; hereby assume z in c /\ A; then A8: z in c & z in A by XBOOLE_0:def 4; c is Clique of R by A4,Def11; hence z = a by A8,A7,Th15; end; assume z = a; hence z in c /\ A by A7,A5,XBOOLE_0:def 4; end; hence c /\ A = {a} by TARSKI:def 1; end; theorem Th49: :: Glueing lemma: for R being with_finite_stability# antisymmetric transitive non empty RelStr, A being StableSet of R, U being Clique-partition of subrelstr Upper A, L being Clique-partition of subrelstr Lower A st card A = stability# R & card U = stability# R & card L = stability# R ex C being Clique-partition of R st card C = stability# R proof let R be with_finite_stability# antisymmetric transitive non empty RelStr, A be StableSet of R, U be Clique-partition of subrelstr Upper A, L be Clique-partition of subrelstr Lower A such that A1: card A = stability# R and A2: card U = stability# R and A3: card L = stability# R; A4: A is non empty by A1; set aA = Upper A, bA = Lower A; set cR = the carrier of R, Pa = subrelstr aA, Pb = subrelstr bA; A5: aA = the carrier of Pa by YELLOW_0:def 15; A6: bA = the carrier of Pb by YELLOW_0:def 15; reconsider Pa = subrelstr Upper A as with_finite_stability# antisymmetric transitive non empty RelStr by A4; A /\ Upper A = A by XBOOLE_1:21; then A is StableSet of Pa by Th31; then consider f being Function of A, U such that A7: f is bijective and A8: for x being set st x in A holds x in f.x by A1,A2,Th47; A9: dom f = A by A4,FUNCT_2:def 1; A10: rng f = U by A7,FUNCT_2:def 3; reconsider Pb = subrelstr Lower A as with_finite_stability# antisymmetric transitive non empty RelStr by A4; A /\ Lower A = A by XBOOLE_1:21; then A is StableSet of Pb by Th31; then consider g being Function of A, L such that A11: g is bijective and A12: for x being set st x in A holds x in g.x by A1,A3,Th47; A13: dom g = A by A4,FUNCT_2:def 1; A14: rng g = L by A11,FUNCT_2:def 3; set h = f .\/ g; set C = rng h; A15: dom h = dom f \/ dom g by LEXBFS:def 2; A16: C c= bool cR proof let x be set; assume x in C; then consider a being set such that A17: a in dom h and A18: h.a = x by FUNCT_1:def 3; A19: h.a = f.a \/ g.a by A17,A15,LEXBFS:def 2; f.a in U by A17,A15,FUNCT_2:5; then A20: f.a c= cR by A5,XBOOLE_1:1; g.a in L by A17,A15,FUNCT_2:5; then g.a c= cR by A6,XBOOLE_1:1; then x c= cR by A18,A19,A20,XBOOLE_1:8; hence x in bool cR; end; A21: union C = cR proof now let x be set; hereby assume x in union C; then consider Y being set such that A22: x in Y and A23: Y in C by TARSKI:def 4; consider a being set such that A24: a in dom h and A25: Y = h.a by A23,FUNCT_1:def 3; A26: x in f.a \/ g.a by A24,A25,A22,A15,LEXBFS:def 2; per cases by A26,XBOOLE_0:def 3; suppose A27: x in f.a; f.a in U by A24,A15,FUNCT_2:5; then x in aA by A27,A5; hence x in cR; end; suppose A28: x in g.a; g.a in L by A24,A15,FUNCT_2:5; then x in bA by A28,A6; hence x in cR; end; end; assume x in [#]R; then A29: x in Upper A \/ Lower A by A1,Th23; per cases by A29,XBOOLE_0:def 3; suppose x in Upper A; then x in union U by A5,EQREL_1:def 4; then consider Y being set such that A30: x in Y and A31: Y in U by TARSKI:def 4; consider a being set such that A32: a in dom f and A33: Y = f.a by A31,A10,FUNCT_1:def 3; A34: h.a in rng h by A32,A15,A9,A13,FUNCT_1:3; h.a = f.a \/ g.a by A32,A15,A9,A13,LEXBFS:def 2; then x in h.a by A30,A33,XBOOLE_0:def 3; hence x in union C by A34,TARSKI:def 4; end; suppose x in Lower A; then x in union L by A6,EQREL_1:def 4; then consider Y being set such that A35: x in Y and A36: Y in L by TARSKI:def 4; consider a being set such that A37: a in dom g and A38: Y = g.a by A36,A14,FUNCT_1:def 3; A39: h.a in rng h by A37,A15,A9,A13,FUNCT_1:3; h.a = f.a \/ g.a by A37,A15,A9,A13,LEXBFS:def 2; then x in h.a by A35,A38,XBOOLE_0:def 3; hence x in union C by A39,TARSKI:def 4; end; end; hence thesis by TARSKI:1; end; A40: now let a be Subset of cR; assume a in C; then consider x being set such that A41: x in dom h and A42: h.x = a by FUNCT_1:def 3; A43: h.x = f.x \/ g.x by A41,A15,LEXBFS:def 2; set cfx = f.x, cgx = g.x; A44: cfx in U by A41,A15,FUNCT_2:5; then reconsider cfx as Subset of Pa; A45: cgx in L by A41,A15,FUNCT_2:5; then reconsider cgx as Subset of Pb; cfx <> {} by A44,EQREL_1:def 4; hence a <> {} by A42,A43; let b be Subset of cR; assume b in C; then consider y being set such that A46: y in dom h and A47: h.y = b by FUNCT_1:def 3; A48: h.y = f.y \/ g.y by A46,A15,LEXBFS:def 2; set cfy = f.y, cgy = g.y; A49: cfy in U by A46,A15,FUNCT_2:5; then reconsider cfy as Subset of Pa; A50: cgy in L by A46,A15,FUNCT_2:5; then reconsider cgy as Subset of Pb; assume A51: a <> b; then A52: cfx <> cfy by A7,A42,A47,A41,A46,A15,A9,FUNCT_1:def 4; A53: cgx <> cgy by A11,A51,A42,A47,A41,A46,A15,A13,FUNCT_1:def 4; assume a meets b; then a /\ b <> {} by XBOOLE_0:def 7; then consider z being set such that A54: z in a /\ b by XBOOLE_0:def 1; A55: z in a by A54,XBOOLE_0:def 4; A56: z in b by A54,XBOOLE_0:def 4; set cfz = f.z, cgz = g.z; per cases by A55,A56,A42,A47,A43,A48,XBOOLE_0:def 3; suppose z in cfx & z in cfy; then z in cfx /\ cfy by XBOOLE_0:def 4; then cfx meets cfy by XBOOLE_0:def 7; hence contradiction by A44,A49,A52,EQREL_1:def 4; end; suppose A57: z in cfx & z in cgy; then A58: z in A by A5,A6,Th22; A59: z in f.z by A57,A5,A6,Th22,A8; A60: cfz in U by A57,A5,A6,Th22,FUNCT_2:5; then reconsider cfz as Subset of Pa; z in cfx /\ cfz by A57,A59,XBOOLE_0:def 4; then cfz meets cfx by XBOOLE_0:def 7; then cfz = cfx by A44,A60,EQREL_1:def 4; then A61: z = x by A7,A41,A58,A15,A9,FUNCT_1:def 4; A62: z in g.z by A57,A5,A6,Th22,A12; A63: cgz in L by A57,A5,A6,Th22,FUNCT_2:5; then reconsider cgz as Subset of Pb; z in cgz /\ cgy by A57,A62,XBOOLE_0:def 4; then cgz meets cgy by XBOOLE_0:def 7; then cgz = cgy by A50,A63,EQREL_1:def 4; hence contradiction by A61,A51,A42,A47,A11,A46,A58,A15,A13, FUNCT_1:def 4; end; suppose A64: z in cgx & z in cfy; then A65: z in A by A5,A6,Th22; A66: z in f.z by A64,A5,A6,Th22,A8; A67: cfz in U by A64,A5,A6,Th22,FUNCT_2:5; then reconsider cfz as Subset of Pa; z in cfy /\ cfz by A64,A66,XBOOLE_0:def 4; then cfz meets cfy by XBOOLE_0:def 7; then cfz = cfy by A49,A67,EQREL_1:def 4; then A68: z = y by A7,A46,A65,A15,A9,FUNCT_1:def 4; A69: z in g.z by A64,A5,A6,Th22,A12; A70: cgz in L by A64,A5,A6,Th22,FUNCT_2:5; then reconsider cgz as Subset of Pb; z in cgz /\ cgx by A64,A69,XBOOLE_0:def 4; then cgz meets cgx by XBOOLE_0:def 7; then cgz = cgx by A45,A70,EQREL_1:def 4; hence contradiction by A68,A51,A42,A47,A11,A41,A65,A15,A13, FUNCT_1:def 4; end; suppose z in cgx & z in cgy; then z in cgx /\ cgy by XBOOLE_0:def 4; then cgx meets cgy by XBOOLE_0:def 7; hence contradiction by A45,A50,A53,EQREL_1:def 4; end; end; A71: for x being set st x in C holds x is Clique of R proof let c be set; assume c in C; then consider x being set such that A72: x in dom h and A73: c = h.x by FUNCT_1:def 3; A74: c = f.x \/ g.x by A72,A73,A15,LEXBFS:def 2; set cf = f.x, cg = g.x; cf in U by A72,A15,FUNCT_2:5; then A75: cf is Clique of Pa by Def11; then A76: cf is Clique of R by Th28; cg in L by A72,A15,FUNCT_2:5; then A77: cg is Clique of Pb by Def11; then A78: cg is Clique of R by Th28; then reconsider c9 = c as Subset of R by A74,A76,XBOOLE_1:8; now let a, b being Element of R such that A79: a in c9 and A80: b in c9 and A81: a <> b; A82: x in cf by A72,A15,A8; A83: x in cg by A72,A15,A12; reconsider x as Element of R by A72,A15,A9,A13; per cases by A79,A80,A74,XBOOLE_0:def 3; suppose a in f.x & b in f.x; hence a <= b or b <= a by A76,A81,Th6; end; suppose A84: a in f.x & b in g.x; then A85: x = a or x <= a by A82,A72,A15,A75,Th35; x = b or b <= x by A83,A84,A72,A15,A77,Th34; hence a <= b or b <= a by A81,A85,YELLOW_0:def 2; end; suppose A86: a in g.x & b in f.x; then A87: x = a or a <= x by A83,A72,A15,A77,Th34; x = b or x <= b by A82,A86,A72,A15,A75,Th35; hence a <= b or b <= a by A81,A87,YELLOW_0:def 2; end; suppose a in g.x & b in g.x; hence a <= b or b <= a by A78,A81,Th6; end; end; hence c is Clique of R by Th6; end; A88: h is one-to-one proof let x1,x2 be set such that A89: x1 in dom h and A90: x2 in dom h and A91: h.x1 = h.x2; A92: h.x1 is Clique of R by A71,A89,FUNCT_1:3; A93: h.x1 = f.x1 \/ g.x1 by A15,A89,LEXBFS:def 2; x1 in f.x1 & x1 in g.x1 by A89,A15,A8,A12; then A94: x1 in h.x1 by A93,XBOOLE_0:def 3; A95: h.x2 = f.x2 \/ g.x2 by A15,A90,LEXBFS:def 2; x2 in f.x2 & x2 in g.x2 by A90,A15,A8,A12; then x2 in h.x2 by A95,XBOOLE_0:def 3; hence x1 = x2 by A15,A89,A90,A91,A92,A94,Th15; end; reconsider C as Clique-partition of R by A16,A21,A40,A71,Def11,EQREL_1:def 4; take C; card C = card h by A88,PRE_POLY:19 .= card A by A15,A9,A13,CARD_1:62; hence card C = stability# R by A1; end; definition let R be RelStr, P be a_partition of the carrier of R; attr P is StableSet-wise means :Def12: for x being set st x in P holds x is StableSet of R; end; registration let R be RelStr; cluster StableSet-wise for a_partition of the carrier of R; existence proof set cR = the carrier of R; per cases; suppose R is empty; then reconsider S = {} as a_partition of cR by EQREL_1:45; take S; let x be set; thus thesis; end; suppose A1: R is non empty; then reconsider RR = R as non empty RelStr; take S = SmallestPartition cR; let z being set; assume A2: z in S; S = {{x} where x is Element of cR: not contradiction} by A1,EQREL_1:37; then consider x being Element of RR such that A3: z = {x} by A2; thus z is StableSet of R by A3; end; 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 proof let P be a_partition of the carrier of R; let x be set; thus thesis; end; end; theorem :: ColClique: for R being finite RelStr, C being Coloring of R holds card C >= clique# R proof let R be finite RelStr, C be Coloring of R; assume A1: card(C) < clique# R; consider A being Clique of R such that A2: card A = clique# R by Def4; card card C = card C & card card A = card A; then A3: card C in card A by A1,A2,NAT_1:41; set cR = the carrier of R; per cases; suppose R is empty; hence contradiction by A1; end; suppose A4: R is non empty; defpred P[set,set] means $1 in A & $2 in C & $1 in $2; A5: for x being set st x in A ex y being set st y in C & P[x,y] proof let x be set such that A6: x in A; reconsider x9 = x as Element of R by A6; cR is non empty by A4; then x9 in cR; then x in union C by EQREL_1:def 4; then consider y being set such that A7: x in y and A8: y in C by TARSKI:def 4; take y; thus thesis by A6,A7,A8; end; consider f being Function of A, C such that A9: for x being set st x in A holds P[x,f.x] from FUNCT_2:sch 1(A5); consider x,y being set such that A10: x in A and A11: y in A and A12: x <> y and A13: f.x = f.y by A4,A3,FINSEQ_4:65; f.x in C by A10,FUNCT_2:5; then A14: f.x is StableSet of R by Def12; x in f.x & y in f.x by A13,A10,A11,A9; hence contradiction by A14,A10,A11,A12,Th15; end; end; begin :: Dilworth's theorem and a dual :: 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. ::$N Dilworth's Decomposition Theorem theorem Th51: :: Dilworth: Finite case for R being finite antisymmetric transitive RelStr ex C being Clique-partition of R st card(C) = stability# R proof defpred P[Nat] means for P being finite antisymmetric transitive RelStr st card(P) = $1 ex C being Clique-partition of P st card(C) = stability# P; A1: for n being Nat st for k being Nat st k < n holds P[k] holds P[n] proof let n be Nat; assume A2: for k being Nat st k < n holds P[k]; let P be finite antisymmetric transitive RelStr; assume A3: card(P) = n; set wP = stability# P; per cases; suppose A4: n = 0; then P is empty by A3; then reconsider C = {} as Clique-partition of P by EQREL_1:45; take C; P is empty by A3,A4; hence card(C) = stability# P by A3,A4; end; suppose A5: n > 0; per cases; suppose ex A being StableSet of P st card(A) = stability# P & A <> minimals(P) & A <> maximals(P); then consider A being StableSet of P such that A6: card A = stability# P and A7: A <> minimals(P) and A8: A <> maximals(P); set aA = Upper A, bA = Lower A; set cP = the carrier of P, Pa = subrelstr aA, Pb = subrelstr bA; reconsider PP = P as finite non empty antisymmetric transitive RelStr by A5,A3; A9: aA = the carrier of Pa by YELLOW_0:def 15; A10: bA = the carrier of Pb by YELLOW_0:def 15; not minimals PP c= aA by A7,Th40,Th26; then consider mi being set such that A11: mi in minimals P and A12: not mi in aA by TARSKI:def 3; not maximals PP c= bA by A8,Th41,Th27; then consider ma being set such that A13: ma in maximals P and A14: not ma in bA by TARSKI:def 3; reconsider Pa as finite antisymmetric transitive RelStr; mi in cP by A11; then aA c< cP by A12,XBOOLE_0:def 8; then card Pa < card P by A9,CARD_2:48; then consider Ca being Clique-partition of Pa such that A15: card(Ca) = stability# Pa by A2,A3; A16: stability# Pa = wP by A6,Th45,XBOOLE_1:7; reconsider Pb as finite antisymmetric transitive RelStr; ma in cP by A13; then bA c< cP by A14,XBOOLE_0:def 8; then card Pb < card P by A10,CARD_2:48; then consider L being Clique-partition of Pb such that A17: card(L) = stability# Pb by A2,A3; stability# Pb = wP by A6,Th45,XBOOLE_1:7; then consider C being Clique-partition of P such that A18: card C = stability# PP by A6,A15,A16,A17,Th49; take C; thus card(C) = stability# P by A18; end; suppose A19: for A being StableSet of P st card(A) = stability# P holds A = minimals(P) or A = maximals(P); consider S being StableSet of P such that A20: card(S) = stability# P by Def6; reconsider PP = P as finite non empty antisymmetric transitive RelStr by A5,A3; set cR = the carrier of PP; set a = the Element of minimals(P); A21: a in minimals(PP); then reconsider a as Element of PP; consider b being Element of PP such that A22: b is_maximal_in [#]PP and A23: a = b or a < b by Th38; A24: b in maximals(P) by A22,Def10; set cP = the carrier of P; set Cn = {a, b}; set cP9 = cP \ Cn; A25: cP = cP9 \/ Cn by XBOOLE_1:45; A26: cP9 misses {a,b} by XBOOLE_1:79; then A27: cP \ cP9 = {a,b} by A25,XBOOLE_1:88; reconsider cP9 as Subset of cR; set P9 = subrelstr cP9; A28: cP9 = the carrier of P9 by YELLOW_0:def 15; A29: card cP9= card P9 by YELLOW_0:def 15; card cP9 = card cP - card {a,b} by CARD_2:44; then consider C being Clique-partition of P9 such that A30: card(C) = stability# P9 by A2,A3,A29,XREAL_1:44; A31: not {a,b} in C proof assume :: works through typing: Subset-Family -> Subset bool ... A32: {a,b} in C; a in {a,b} by TARSKI:def 2; hence contradiction by A26,A28,A32,ZFMISC_1:49; end; set wP = stability# PP; set wP1 = wP - 1; 0+1 <= wP by NAT_1:13; then 0+1-1 <= wP-1 by XREAL_1:9; then wP1 in NAT by INT_1:3; then reconsider wP1 as Nat; set S9 = S /\ cP9; S /\ cP = S by XBOOLE_1:28; then A33: S9 = S \ {a,b} by XBOOLE_1:49; A34: {a,b} = {a} \/ {b} by ENUMSET1:1; reconsider S9 as StableSet of P9 by Th31; A35: card S9 = wP1 proof per cases by A19,A20; suppose A36: S = minimals(P); S9 = S \ {a} proof per cases; suppose a = b; hence S9 = S \ {a} by A33,ENUMSET1:29; end; suppose A37: a <> b; now assume b in minimals(PP); then b is_minimal_in [#]PP by Def9; hence contradiction by A37,A23,WAYBEL_4:56; end; hence S9 = S \ {a} by A33,A34,A36,Th1; end; end; hence card S9 = card S - card {a} by A36,EULER_1:4 .= wP1 by A20,CARD_1:30; end; suppose A38: S = maximals(PP); A39: S9 = S \ {b} proof per cases; suppose a = b; hence S9 = S \ {b} by A33,ENUMSET1:29; end; suppose A40: a <> b; now assume a in maximals(PP); then a is_maximal_in [#]PP by Def10; hence contradiction by A40,A23,WAYBEL_4:55; end; hence S9 = S \ {b} by A33,A34,A38,Th1; end; end; b in S by A38,A22,Def10; hence card S9 = card S - card {b} by A39,EULER_1:4 .= wP1 by A20,CARD_1:30; end; end; for T being StableSet of P9 holds card(T) <= card(S9) proof let T be StableSet of P9; assume card(T) > card(S9); then card T >= card S9 + 1 by NAT_1:13; then consider V being StableSet of P9 such that A41: card V = card S9 + 1 by Th17; V is StableSet of P by Th30; then V = minimals(P) or V =maximals(P) by A19,A41,A35; hence contradiction by A21,A24,A28,A26,ZFMISC_1:49; end; then A42: stability# P9 + 1 = wP - 1 + 1 by A35,Def6 .= wP; set CC = C \/ {{a,b}}; cP9 <> cP by A27,XBOOLE_1:37; then A43: cP9 c< cP by XBOOLE_0:def 8; now :: Cliques in CC let x be set; assume A44: x in CC; per cases by A44,XBOOLE_0:def 3; suppose x in C; then x is Clique of P9 by Def11; hence x is Clique of P by Th28; end; suppose x in {{a,b}}; then A45: x = {a,b} by TARSKI:def 1; per cases; suppose a = b; then x = {a} by A45,ENUMSET1:29; hence x is Clique of P; end; suppose a <> b; then a <= b by A23,ORDERS_2:def 6; hence x is Clique of P by A45,Th8; end; end; end; then reconsider CC as Clique-partition of P by A27,A28,Th4,Def11,A43; take CC; thus card(CC) = stability# P by A30,A42,A31,CARD_2:41; end; end; end; A46: for n being Nat holds P[n] from NAT_1:sch 4(A1); let R be finite antisymmetric transitive RelStr; card R = card R; hence thesis by A46; end; definition let R be with_finite_stability# non empty RelStr, C be Subset of R; attr C is strong-chain means :Def13: for S being finite non empty 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; registration let R be with_finite_stability# non empty RelStr; cluster strong-chain -> clique for Subset of R; coherence proof let C be Subset of R; assume A1: C is strong-chain; now let a, b be Element of R such that A2: a in C and A3: b in C and A4: a <> b; set S = {a,b}; reconsider S as finite non empty Subset of R; consider P being Clique-partition of subrelstr S such that card P <= stability# R and A5: 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 = {} by A1,Def13; consider c being set such that A6: c in P and A7: S /\ C c= c and for d being set st d in P & d <> c holds C /\ d = {} by A5; c is Clique of subrelstr S by A6,Def11; then A8: c is Clique of R by Th28; a in S & b in S by TARSKI:def 2; then a in S /\ C & b in S /\ C by A2,A3,XBOOLE_0:def 4; hence a <= b or b <= a by A7,A8,A4,Th6; end; hence C is clique by Th6; end; end; registration let R be with_finite_stability# antisymmetric transitive non empty RelStr; cluster 1-element -> strong-chain for Subset of R; coherence proof let C be Subset of R; assume C is 1-element; then consider x being set such that A1: C = {x} by ZFMISC_1:131; let S be finite non empty Subset of R; consider P being Clique-partition of subrelstr S such that A2: card P = stability# subrelstr S by Th51; A3: S = the carrier of subrelstr S by YELLOW_0:def 15; take P; thus card P <= stability# R by A2,Th44; per cases; suppose x in S; then x in union P by A3,EQREL_1:def 4; then consider c being set such that A4: x in c and A5: c in P by TARSKI:def 4; take c; thus c in P by A5; thus S /\ C c= c proof let a be set; assume a in S /\ C; then a in C by XBOOLE_0:def 4; hence thesis by A4,A1,TARSKI:def 1; end; let d be set such that A6: d in P and A7: d <> c; assume C /\ d <> {}; then consider a being set such that A8: a in C /\ d by XBOOLE_0:def 1; reconsider d, c as Subset of S by A6,A5,YELLOW_0:def 15; a in C by A8,XBOOLE_0:def 4; then a = x by A1,TARSKI:def 1; then x in d by A8,XBOOLE_0:def 4; then x in d /\ c by A4,XBOOLE_0:def 4; then d meets c by XBOOLE_0:def 7; hence contradiction by A6,A5,A7,EQREL_1:def 4; end; suppose A9: not x in S; set c = the Element of P; take c; thus c in P; C misses S by A9,A1,ZFMISC_1:50; then S /\ C = {} by XBOOLE_0:def 7; hence S /\ C c= c by XBOOLE_1:2; let d be set such that A10: d in P and d <> c; not x in d by A9,A3,A10; then C misses d by A1,ZFMISC_1:50; hence C /\ d = {} by XBOOLE_0:def 7; end; end; end; theorem Th52: :: Maxsc: for R being with_finite_stability# non empty antisymmetric transitive RelStr ex S being non empty Subset of R st S is strong-chain & not ex D being Subset of R st D is strong-chain & S c< D proof let R be with_finite_stability# non empty antisymmetric transitive RelStr; set E = { C where C is Subset of R: C is strong-chain }; set x = the Element of R; A1: {x} in E; now :: premise of maximal principle let Z be set such that A2: Z c= E and A3: Z is c=-linear; set Y = union Z; take Y; now let B be set; assume B in Z; then B in E by A2; then ex C being Subset of R st C = B & C is strong-chain; hence B c= the carrier of R; end; then reconsider Y9 = Y as Subset of R by ZFMISC_1:76; Y9 is strong-chain proof let S be finite non empty Subset of R; set F = S /\ Y; per cases; suppose A4: F is empty; consider p being Clique-partition of subrelstr S such that A5: card p = stability# subrelstr S by Th51; take p; thus card p <= stability# R by Th44,A5; set c = the Element of p; take c; thus c in p; thus S /\ Y9 c= c by A4,XBOOLE_1:2; let d be set such that A6: d in p and d <> c; d c= the carrier of subrelstr S by A6; then d c= S by YELLOW_0:def 15; hence Y9 /\ d = {} by A4,XBOOLE_1:3,26; end; suppose A7: F is non empty; then A8: Z is non empty by ZFMISC_1:2; defpred P[set,set] means $1 in F & $2 in Z & $1 in $2; A9: for x being set st x in F ex y being set st y in Z & P[x,y] proof let x be set; assume A10: x in F; then x in Y by XBOOLE_0:def 4; then consider y being set such that A11: x in y and A12: y in Z by TARSKI:def 4; take y; thus thesis by A12,A10,A11; end; consider f being Function of F, Z such that A13: for x being set st x in F holds P[x,f.x] from FUNCT_2:sch 1(A9); set rf = rng f; rf c= Z & Z is c=-linear implies rf is c=-linear; then consider m being set such that A14: m in rf and A15: for C being set st C in rf holds C c= m by A3,A7,A8,FINSET_1:12,RELAT_1:def 19; rf c= Z by RELAT_1:def 19; then m in Z by A14; then m in E by A2; then consider C being Subset of R such that A16: m = C and A17: C is strong-chain; A18: F c= C proof let x be set; assume A19: x in F; then A20: x in f.x by A13; f.x c= C by A16,A15,A19,A8,FUNCT_2:4; hence x in C by A20; end; consider p being Clique-partition of subrelstr S such that A21: card p <= stability# R and A22: 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 = {} by A17,Def13; take p; thus card p <= stability# R by A21; consider c being set such that A23: c in p and A24: S /\ C c= c and A25: for d being set st d in p & d <> c holds C /\ d = {} by A22; take c; thus c in p by A23; thus S /\ Y9 c= c proof let x be set; assume x in S /\ Y9; then x in S & x in C by A18,XBOOLE_0:def 4; then x in S /\ C by XBOOLE_0:def 4; hence x in c by A24; end; let d be set such that A26: d in p and A27: d <> c; assume Y9 /\ d <> {}; then consider x being set such that A28: x in Y9 /\ d by XBOOLE_0:def 1; A29: x in Y9 by A28,XBOOLE_0:def 4; A30: x in d by A28,XBOOLE_0:def 4; d is Subset of S by A26,YELLOW_0:def 15; then x in F by A30,A29,XBOOLE_0:def 4; then x in C /\ d by A30,A18,XBOOLE_0:def 4; hence contradiction by A26,A27,A25; end; end; hence Y in E; let X1 be set such that A31: X1 in Z; thus X1 c= Y by A31,ZFMISC_1:74; end; then consider Y being set such that A32: Y in E and A33: for Z being set st Z in E & Z <> Y holds not Y c= Z by A1,ORDERS_1:65; consider C being Subset of R such that A34: Y = C and A35: C is strong-chain by A32; reconsider S = C as non empty Subset of R by A34,A1,A33,XBOOLE_1:2; take S; thus S is strong-chain by A35; let D be Subset of R such that A36: D is strong-chain and A37: S c< D; A38: D in E by A36; D <> S & S c= D by A37,XBOOLE_0:def 8; hence contradiction by A34,A38,A33; end; theorem :: Dilworth: General case for R being with_finite_stability# antisymmetric transitive RelStr ex C being Clique-partition of R st card C = stability# R proof let R be with_finite_stability# antisymmetric transitive RelStr; per cases; suppose R is finite; hence thesis by Th51; end; suppose A1: R is infinite; defpred P[Nat] means for P being with_finite_stability# non empty antisymmetric transitive RelStr st stability# P = $1 ex C being Clique-partition of P st card(C) = stability# P; A2: P[0]; A3: for k be Nat st P[k] holds P[k + 1] proof let k be Nat; assume A4: P[k]; let P be with_finite_stability# non empty antisymmetric transitive RelStr; assume A5: stability# P = k+1; consider C being non empty Subset of P such that A6: C is strong-chain and A7: not ex D being Subset of P st D is strong-chain & C c< D by Th52; set cP = the carrier of P; per cases; suppose A8: C = cP; :: real base case for x being set st x in { C } holds x is Clique of P by A6,TARSKI:def 1; then reconsider Cp = { C } as Clique-partition of P by Def11,A8,EQREL_1:39; take Cp; A9: cP = [#]P; thus card Cp = 1 by CARD_1:30 .= stability# P by A9,A6,A8,Th20; end; suppose C <> cP; then A10: C c< cP by XBOOLE_0:def 8; set cP9 = cP \ C; A11: cP \ cP9 = cP /\ C by XBOOLE_1:48 .= C by XBOOLE_1:28; reconsider cP9 as Subset of P; cP9 <> {} by A10,XBOOLE_1:105; then reconsider P9 = subrelstr cP9 as with_finite_stability# non empty antisymmetric transitive RelStr; A12: cP9 = the carrier of P9 by YELLOW_0:def 15; A13: stability# P9 <= k+1 by A5,Th44; A14: stability# P9 <> k+1 proof assume A15: stability# P9 = k+1; consider A being finite StableSet of P9 such that A16: card(A) = stability# P9 by Def6; reconsider A9 = A as finite non empty StableSet of P by A16,Th30; defpred R[set, set, set] means for c being set st c in $2 holds not $1 /\ $3 c= c or ex d being set st d in $2 & d <> c & $3 /\ d <> {}; defpred Q[finite Subset of P,set] means for p being Clique-partition of subrelstr $1 st card p <= stability# P holds R[$1,p,$2]; defpred P[set,set] means ex S being finite non empty Subset of P st $2 = S & $1 in $2 & Q[S, C\/{$1}]; A17: for x being set st x in A ex y being set st P[x,y] proof let a be set; assume A18: a in A; A c= cP by A12,XBOOLE_1:1; then {a} c= cP by A18,ZFMISC_1:31; then reconsider Ca = C \/ {a} as Subset of P by XBOOLE_1:8; now assume A19: Ca is strong-chain; a in {a} by TARSKI:def 1; then A20: a in Ca by XBOOLE_0:def 3; A21: not a in C by A12,A18,XBOOLE_0:def 5; C c= Ca by XBOOLE_1:7; then C c< Ca by A20,A21,XBOOLE_0:def 8; hence contradiction by A19,A7; end; then consider S being finite non empty Subset of P such that A22: Q[S,Ca] by Def13; take S; take S; thus S = S; now assume A23: not a in S; A24: S /\ C c= S /\ Ca proof let x be set; assume x in S /\ C; then x in S & x in C by XBOOLE_0:def 4; then x in S & x in Ca by XBOOLE_0:def 3; hence x in S /\ Ca by XBOOLE_0:def 4; end; S /\ Ca c= S /\ C proof let x be set; assume A25: x in S /\ Ca; then A26: x in S by XBOOLE_0:def 4; x in Ca by A25,XBOOLE_0:def 4; then x in C or x in {a} by XBOOLE_0:def 3; hence x in S /\ C by A26,A23,TARSKI:def 1,XBOOLE_0:def 4; end; then A27: S /\ C = S /\ Ca by A24,XBOOLE_0:def 10; consider p being Clique-partition of subrelstr S such that A28: card p <= stability# P and A29: not R[S,p,C] by A6,Def13; consider c being set such that A30: c in p and A31: S /\ C c= c and A32: for d being set st d in p & d <> c holds C /\ d = {} by A29; for d being set st d in p & d <> c holds Ca /\ d = {} proof let d be set such that A33: d in p and A34: d <> c; now assume Ca /\ d <> {}; then consider x being set such that A35: x in Ca /\ d by XBOOLE_0:def 1; A36: x in Ca by A35,XBOOLE_0:def 4; A37: x in d by A35,XBOOLE_0:def 4; per cases by A36,XBOOLE_0:def 3; suppose x in C; then x in C /\ d by A37,XBOOLE_0:def 4; hence contradiction by A33,A34,A32; end; suppose x in {a}; then x = a by TARSKI:def 1; then a in the carrier of subrelstr S by A37,A33; hence contradiction by A23,YELLOW_0:def 15; end; end; hence Ca /\ d = {}; end; hence contradiction by A30,A31,A28,A27,A22; end; hence a in S; thus thesis by A22; end; consider f being Function such that A38: dom f = A and A39: for x being set st x in A holds P[x,f.x] from CLASSES1:sch 1(A17); A40: rng f is finite by A38,FINSET_1:8; set SS = union rng f; A41: for x being set st x in rng f holds x is finite proof let x be set; assume x in rng f; then consider a being set such that A42: a in dom f and A43: x = f.a by FUNCT_1:def 3; consider S being finite non empty Subset of P such that A44: f.a = S and a in f.a & Q[S, C \/ {a}] by A38,A42,A39; thus x is finite by A44,A43; end; A45: SS c= cP proof let x be set; assume x in SS; then consider y being set such that A46: x in y and A47: y in rng f by TARSKI:def 4; consider a being set such that A48: a in dom f and A49: y = f.a by A47,FUNCT_1:def 3; consider S being finite non empty Subset of P such that A50: f.a = S and a in f.a & Q[S, C \/ {a}] by A38,A48,A39; thus x in cP by A46,A49,A50; end; A51: A9 c= SS proof let x be set; assume A52: x in A9; then consider S being finite non empty Subset of P such that f.x = S and A53: x in f.x and Q[S, C \/ {x}] by A39; f.x in rng f by A52,A38,FUNCT_1:3; hence x in SS by A53,TARSKI:def 4; end; then reconsider SS as finite non empty Subset of P by A41,A40,A45,FINSET_1:7; set SSp = subrelstr SS; A54: SS = the carrier of SSp by YELLOW_0:def 15; consider p being Clique-partition of SSp such that A55: card p <= stability# P and A56: not R[SS,p,C] by A6,Def13; consider c being set such that A57: c in p and A58: SS /\ C c= c and A59: for d being set st d in p & d <> c holds C /\ d = {} by A56; reconsider c as Element of p by A57; A9 = A9 /\ SS by A51,XBOOLE_1:28; then reconsider A = A9 as finite non empty StableSet of SSp by Th31; A60: stability# SSp >= card A by Def6; card p >= stability# SSp by Th46; then card p >= card A by A60,XXREAL_0:2; then consider a being Element of A such that A61: c /\ A = {a} by Th48,A55,A16,A15,A5,XXREAL_0:1; a in c /\ A by A61,TARSKI:def 1; then A62: a in c by XBOOLE_0:def 4; consider S being finite non empty Subset of P such that A63: f.a = S and A64: a in f.a and A65: Q[S, C \/ {a}] by A39; deffunc F(set) = $1 /\ S; defpred P[set] means $1 meets S; set Sp = { F(e) where e is Element of p: P[e]}; A66: S c= SS proof let x be set; assume A67: x in S; S in rng f by A63,A38,FUNCT_1:3; hence x in SS by A67,TARSKI:def 4; end; then reconsider Sp as a_partition of S by A54,PUA2MSS1:11; for x being set st x in Sp holds x is Clique of subrelstr S proof let x be set; assume x in Sp; then consider e being Element of p such that A68: x = e /\ S and e meets S; e is Clique of SSp by Def11; then e is Clique of P by Th28; hence x is Clique of subrelstr S by A68,Th29; end; then reconsider Sp as Clique-partition of subrelstr S by Def11,YELLOW_0:def 15; A69: Sp = { F(e) where e is Element of p: P[e]}; A70: card Sp <= card p from FraenkelFinCard1(A69); set cc = c /\ S; c meets S by A62,A63,A64,XBOOLE_0:3; then A71: cc in Sp; S /\ (C \/ {a}) c= cc proof let x be set; assume A72: x in S /\ (C \/ {a}); then A73: x in S by XBOOLE_0:def 4; A74: x in C \/ {a} by A72,XBOOLE_0:def 4; per cases by A74,XBOOLE_0:def 3; suppose x in C; then x in SS /\ C by A73,A66,XBOOLE_0:def 4; hence x in cc by A73,A58,XBOOLE_0:def 4; end; suppose x in {a}; then x = a by TARSKI:def 1; hence x in cc by A62,A63,A64,XBOOLE_0:def 4; end; end; then consider d being set such that A75: d in Sp and A76: d <> cc and A77: (C \/ {a}) /\ d <> {} by A71,A70,A55,A65,XXREAL_0:2; consider dd being Element of p such that A78: d = dd /\ S and dd meets S by A75; C /\ dd = {} by A78,A76,A59; then A79: C /\ d = {} /\ S by A78,XBOOLE_1:16 .= {}; C /\ d \/ {a} /\ d <> {} by A77,XBOOLE_1:23; then consider x being set such that A80: x in {a} /\ d by A79,XBOOLE_0:def 1; x in {a} & x in d by A80,XBOOLE_0:def 4; then a in d by TARSKI:def 1; then a in dd by A78,XBOOLE_0:def 4; then c meets dd by A62,XBOOLE_0:3; hence contradiction by A78,A76,EQREL_1:def 4; end; then stability# P9 < k+1 by A13,XXREAL_0:1; then A81: stability# P9 <= k by NAT_1:13; consider A being finite StableSet of P such that A82: card A = stability# P by Def6; A83: stability# P9 = k proof per cases; suppose A84: A /\ C = {}; A c= cP9 proof let x be set; assume A85: x in A; then not x in C by A84,XBOOLE_0:def 4; hence x in cP9 by A85,XBOOLE_0:def 5; end; hence thesis by A5,A14,A82,Th45; end; suppose A /\ C <> {}; then consider x being set such that A86: x in A /\ C by XBOOLE_0:def 1; A87: x in A by A86,XBOOLE_0:def 4; A88: x in C by A86,XBOOLE_0:def 4; set A9 = A \ {x}; {x} c= A by A87,ZFMISC_1:31; then A89: A = A9 \/ {x} by XBOOLE_1:45; x in {x} by TARSKI:def 1; then not x in A9 by XBOOLE_0:def 5; then A90: card A = card A9 + 1 by A89,CARD_2:41; A91: A9 c= A by XBOOLE_1:36; A9 c= cP9 proof let xx be set; assume A92: xx in A9; then A93: xx in A by XBOOLE_0:def 5; not xx in {x} by A92,XBOOLE_0:def 5; then xx <> x by TARSKI:def 1; then not xx in C by A87,A88,A93,A6,Th15; hence xx in cP9 by A92,XBOOLE_0:def 5; end; then A94: A9 c= A /\ cP9 by A91,XBOOLE_1:19; A /\ cP9 c= A9 proof let xx be set; assume A95: xx in A /\ cP9; then A96: xx in A by XBOOLE_0:def 4; xx in cP9 by A95,XBOOLE_0:def 4; then x <> xx by A88,XBOOLE_0:def 5; then not xx in {x} by TARSKI:def 1; hence xx in A9 by A96,XBOOLE_0:def 5; end; then A9 = A /\ cP9 by A94,XBOOLE_0:def 10; then reconsider A9 as StableSet of P9 by Th31; stability# P9 >= card A9 by Def6; hence thesis by A90,A82,A5,A81,XXREAL_0:1; end; end; then consider Cp9 being Clique-partition of P9 such that A97: card(Cp9) = stability# P9 by A4; set Cp = Cp9 \/ { cP \ cP9 }; A98: Cp9 is finite by A97; cP9 <> cP by A11,XBOOLE_1:37; then A99: cP9 c< cP by XBOOLE_0:def 8; then reconsider Cp as a_partition of cP by A12,Th4; now :: chains in Cp; let x be set; assume A100: x in Cp; per cases by A100,XBOOLE_0:def 3; suppose x in Cp9; then x is Clique of P9 by Def11; hence x is Clique of P by Th28; end; suppose x in { cP \ cP9 }; hence x is Clique of P by A6,A11,TARSKI:def 1; end; end; then reconsider Cp as Clique-partition of P by Def11; take Cp; not cP \ cP9 in Cp9 proof assume not thesis; then cP c= cP9 \/ cP9 by A12,XBOOLE_1:44; hence contradiction by A99,XBOOLE_1:60; end; hence card Cp = stability# P by A5,A83,A97,A98,CARD_2:41; end; end; for k being Nat holds P[k] from NAT_1:sch 2(A2,A3); hence thesis by A1; end; end; theorem :: A dual of Dilworth's theorem for R being with_finite_clique# antisymmetric transitive RelStr ex A being Coloring of R st card A = clique# R proof let R be with_finite_clique# antisymmetric transitive RelStr; defpred P[Nat] means for P being with_finite_clique# antisymmetric transitive RelStr st clique# P = $1 ex A being Coloring of P st card A = clique# P; A1: P[0] proof let P be with_finite_clique# antisymmetric transitive RelStr; assume A2: clique# P = 0; then P is empty; then reconsider C = {} as Coloring of P by EQREL_1:45; take C; thus card(C) = clique# P by A2; end; A3: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A4: P[n]; let P be with_finite_clique# antisymmetric transitive RelStr; assume A5: clique# P = n+1; then A6: P is non empty; reconsider PP = P as with_finite_clique# non empty antisymmetric transitive RelStr by A5; set M = maximals(PP); set cP = the carrier of P; set cPM = cP \ M; reconsider cPM as Subset of P; set PM = subrelstr cPM; A7: cPM = the carrier of PM by YELLOW_0:def 15; reconsider PM as with_finite_clique# antisymmetric transitive 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 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 /\ M = {m} proof thus C /\ M c= {m} proof let a be set; assume A16: a in C /\ M; then A17: a in C by XBOOLE_0:def 4; A18: a in M 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 assume A20: a <> m; not m < a9 by A17,A14,WAYBEL_4:55; then not m <= a9 by A20,ORDERS_2:def 6; then a9 <= m by A12,A17,A20,Th6; then a9 < m by A20,ORDERS_2:def 6; hence contradiction by A19,A12,WAYBEL_4:55; end; hence a in {m} by TARSKI:def 1; end; thus {m} c= C /\ M proof let a be set; assume a in {m}; then A21: a = m by TARSKI:def 1; now assume A22: not a in M; 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 per cases; suppose m = y; hence Cm is finite Clique of P by A12,ZFMISC_1:40; end; suppose m <> y; then m <= y by A24,ORDERS_2:def 6; hence Cm is finite Clique of P by A14,Th11; end; end; then reconsider Cm 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; end; hence a in C /\ M by A21,A12,XBOOLE_0:def 4; end; end; A25: cC = C /\ cP \ C /\ M by XBOOLE_1:50; C /\ cP = 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 assume A29: clique# PM = n+1; then A30: Ca <> {} by A8; A31:PM is non 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 per cases; suppose x9 = y; hence Cb is finite Clique of P by A32,A9,ZFMISC_1:40; end; suppose x9 <> y; then x9 <= y by A36,ORDERS_2:def 6; hence Cb is finite Clique of P by A34,Th32,A9,Th11; end; end; then reconsider Cb as finite Clique of P; y in M 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; 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 \/ {M}; A39: cP = cPM \/ M by XBOOLE_1:45; {M} is a_partition of M by EQREL_1:39; then A40: A is a_partition of cP by A39,A7,Th3,XBOOLE_1:79; now let x be set; assume A41: x in A; per cases by A41,XBOOLE_0:def 3; suppose x in Aa; then x is StableSet of PM by Def12; hence x is StableSet of P by Th30; end; suppose x in {M}; hence x is StableSet of P by TARSKI:def 1; end; end; then reconsider A as Coloring of P by A40,Def12; take A; not M in Ab by A7,XBOOLE_1:38; hence card A = clique# P by A5,A38,CARD_2:41; end; for n being Nat holds P[n] from NAT_1:sch 2(A1,A3); hence ex A being Coloring of R st card(A) = clique# R; end; begin :: Erdos-Szekeres theorem ::$N Erdos-Szekeres Theorem theorem Th55: :: CSR for R being finite antisymmetric transitive RelStr, r, s being Nat st card R = r*s+1 holds (ex C being Clique of R st card C >= r+1) or (ex A being StableSet of R st card A >= s+1) proof let R be finite antisymmetric transitive RelStr, r, s be Nat such that A1: card R = r*s+1 and A2: for C being Clique of R holds card C < r+1 and A3: for A being StableSet of R holds card A < s+1; consider p being Clique-partition of R such that A4: card p = stability# R by Th51; consider A being finite StableSet of R such that A5: card A = stability# R by Def6; stability# R < s+1 by A3,A5; then A6: stability# R <= s by NAT_1:13; set wR = stability# R; set cR = the carrier of R; set f = canFS p; A7: len f = card p by UPROOTS:3; A8: dom f = Seg len f by FINSEQ_1:def 3; set f = canFS p; A9: rng f = p by FUNCT_2:def 3; then reconsider f as FinSequence of bool cR by FINSEQ_1:def 4; now let d,e be Nat such that A10: d in dom f and A11: e in dom f and A12: d<>e; A13: f.d in rng f by A10,FUNCT_1:3; A14: f.e in rng f by A11,FUNCT_1:3; then reconsider fd = f.d, fe = f.e as Subset of cR by A13,A9; fd <> fe by A12,A10,A11,FUNCT_1:def 4; hence f.d misses f.e by A13,A14,A9,EQREL_1:def 4; end; then A15: card union rng f = Sum Card f by A7,INT_5:48; reconsider n9 = r as Element of NAT by ORDINAL1:def 12; reconsider h = wR |-> n9 as Element of wR-tuples_on NAT; A16: Sum h = wR*r by RVSUM_1:80; dom f = dom Card f by CARD_3:def 2; then len Card f = wR by A7,A4,FINSEQ_3:29; then reconsider Cf = Card f as Element of wR-tuples_on NAT by FINSEQ_2:92; A17: h is Element of wR-tuples_on REAL by FINSEQ_2:109; A18: Cf is Element of wR-tuples_on REAL by FINSEQ_2:109; now let j being Nat such that A19: j in Seg wR; A20: h.j = r by A19,FINSEQ_2:57; A21: Cf.j = card (f.j) by A19,A7,A8,A4,CARD_3:def 2; f.j in p by A9,A19,A4,A7,A8,FUNCT_1:3; then reconsider fj = f.j as Clique of R by Def11; card fj < r+1 by A2; hence Cf.j <= h.j by A20,A21,NAT_1:13; end; then A22: Sum Cf <= Sum h by A17,A18,RVSUM_1:82; wR*r <= s*r by A6,XREAL_1:64; then Sum Cf <= s*r by A16,A22,XXREAL_0:2; then r*s+1 <= r*s+0 by A15,A9,A1,EQREL_1:def 4; hence contradiction by XREAL_1:6; 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 for f being real-valued FinSequence, n being Nat st card f = n^2+1 & f is one-to-one ex g being real-valued FinSubsequence st g c= f & card g >= n+1 & (g is increasing or g is decreasing) proof let f be real-valued FinSequence, n be Nat such that A1: card f = n^2+1 and A2: f is one-to-one; set cP = f; defpred P[set,set] means ex i,j being Nat, r, s being real number st $1 = [i,r] & $2 = [j,s] & i= n+1; then consider C being Clique of P such that A25: card C >= n+1; set g = C; reconsider g as Subset of f; reconsider g as Function; dom g c= Seg len f proof let x be set; assume x in dom g; then consider y being set such that A26: [x,y] in g by XTUPLE_0:def 12; x in dom f by A26,XTUPLE_0:def 12; hence thesis by FINSEQ_1:def 3; end; then reconsider g as FinSubsequence by FINSEQ_1:def 12; reconsider g as real-valued FinSubsequence; take g; thus g c= f; thus card g >= n+1 by A25; g is increasing proof let e1, e2 be ext-real number such that A27: e1 in dom g and A28: e2 in dom g and A29: e1 < e2; A30: [e1,g.e1] in g by A27,FUNCT_1:1; A31: [e2,g.e2] in g by A28,FUNCT_1:1; then reconsider p1 = [e1,g.e1], p2 = [e2,g.e2] as Element of P by A30; A32: p1 <> p2 by A29,XTUPLE_0:1; per cases by A30,A31,A32,Th6; suppose p1 <= p2; then [p1,p2] in iP by ORDERS_2:def 5; then consider i,j being Nat, r, s being real number such that A33: p1 = [i,r] and A34: p2 = [j,s] and A35: i= n+1; then consider A being StableSet of P such that A39: card A >= n+1; set g = A; reconsider g as Subset of f; reconsider g as Function; A40: dom g c= Seg len f proof let x be set; assume x in dom g; then consider y being set such that A41: [x,y] in g by XTUPLE_0:def 12; x in dom f by A41,XTUPLE_0:def 12; hence thesis by FINSEQ_1:def 3; end; then reconsider g as FinSubsequence by FINSEQ_1:def 12; reconsider g as real-valued FinSubsequence; take g; thus g c= f; thus card g >= n+1 by A39; g is decreasing proof let e1, e2 be ext-real number such that A42: e1 in dom g and A43: e2 in dom g and A44: e1 < e2; A45: [e1,g.e1] in g by A42,FUNCT_1:1; A46: [e2,g.e2] in g by A43,FUNCT_1:1; then reconsider p1 = [e1,g.e1], p2 = [e2,g.e2] as Element of P by A45; A47: p1 <> p2 by A44,XTUPLE_0:1; g.e1 = f.e1 & g.e2 = f.e2 by A42,A43,GRFUNC_1:2; then A48: g.e1 <> g.e2 by A4,A40,A42,A43,A44,A2,FUNCT_1:def 4; reconsider i = e1, j = e2 as Nat by A42,A43; reconsider r = g.e1, s = g.e2 as real number; A49: p1 = [i,r] & p2 = [j,s]; per cases by A48,XXREAL_0:1; suppose g.e1 < g.e2; then [p1,p2] in iP by A45,A3,A44,A49; then p1 <= p2 by ORDERS_2:def 5; hence g.e1 > g.e2 by A45,A46,A47,Def2; end; suppose g.e1 > g.e2; hence thesis; end; end; hence thesis; end; end;