:: DILWORTH semantic presentation begin scheme :: DILWORTH:sch 1 FraenkelFinCard1{ F1() -> non empty finite set , P1[ set ], F2() -> finite set , F3( set ) -> set } : card F2() <= card F1() provided A1: F2() = { F3(w) where w is Element of F1() : P1[w] } proof A2: F1() is finite ; set Z = { F3(w) where w is Element of F1() : w in F1() } ; { F3(w) where w is Element of F1() : w in F1() } is finite from FRAENKEL:sch_21(A2); then reconsider Z = { F3(w) where w is Element of F1() : w in F1() } as finite set ; A3: Z = { F3(w) where w is Element of F1() : w in F1() } ; A4: card Z <= card F1() from TREES_2:sch_3(A3); F2() c= Z proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F2() or x in Z ) assume x in F2() ; ::_thesis: x in Z then ex w being Element of F1() st ( x = F3(w) & P1[w] ) by A1; hence x in Z ; ::_thesis: verum end; then card F2() <= card Z by NAT_1:43; hence card F2() <= card F1() by A4, XXREAL_0:2; ::_thesis: verum end; theorem Th1: :: DILWORTH:1 for X, Y, x being set st not x in X holds X \ (Y \/ {x}) = X \ Y proof let X, Y, x be set ; ::_thesis: ( not x in X implies X \ (Y \/ {x}) = X \ Y ) assume not x in X ; ::_thesis: X \ (Y \/ {x}) = X \ Y 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 ; ::_thesis: verum end; theorem Th2: :: DILWORTH:2 for X, Y being set for F being Subset-Family of X for G being Subset-Family of Y holds F \/ G is Subset-Family of (X \/ Y) proof let X, Y be set ; ::_thesis: for F being Subset-Family of X for G being Subset-Family of Y holds F \/ G is Subset-Family of (X \/ Y) let F be Subset-Family of X; ::_thesis: for G being Subset-Family of Y holds F \/ G is Subset-Family of (X \/ Y) let G be Subset-Family of Y; ::_thesis: F \/ G is Subset-Family of (X \/ 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; ::_thesis: verum end; theorem Th3: :: DILWORTH:3 for X, Y being set for F being a_partition of X for G being a_partition of Y st X misses Y holds F \/ G is a_partition of X \/ Y proof let X, Y be set ; ::_thesis: for F being a_partition of X for G being a_partition of Y st X misses Y holds F \/ G is a_partition of X \/ Y let F be a_partition of X; ::_thesis: for G being a_partition of Y st X misses Y holds F \/ G is a_partition of X \/ Y let G be a_partition of Y; ::_thesis: ( X misses Y implies F \/ G is a_partition of X \/ Y ) assume A1: X misses Y ; ::_thesis: F \/ G is a_partition of X \/ Y set PR = F \/ G; set XY = X \/ Y; A2: F \/ G is Subset-Family of (X \/ Y) by Th2; A3: union (F \/ G) = (union F) \/ (union G) by ZFMISC_1:78 .= X \/ (union G) by EQREL_1:def_4 .= X \/ Y by EQREL_1:def_4 ; now__::_thesis:_for_A_being_Subset_of_(X_\/_Y)_st_A_in_F_\/_G_holds_ (_A_<>_{}_&_(_for_B_being_Subset_of_(X_\/_Y)_holds_ (_not_B_in_F_\/_G_or_A_=_B_or_A_misses_B_)_)_) let A be Subset of (X \/ Y); ::_thesis: ( A in F \/ G implies ( A <> {} & ( for B being Subset of (X \/ Y) holds ( not B in F \/ G or b2 = b3 or b2 misses b3 ) ) ) ) assume A4: A in F \/ G ; ::_thesis: ( A <> {} & ( for B being Subset of (X \/ Y) holds ( not B in F \/ G or b2 = b3 or b2 misses b3 ) ) ) ( A in F or A in G ) by A4, XBOOLE_0:def_3; hence A <> {} by EQREL_1:def_4; ::_thesis: for B being Subset of (X \/ Y) holds ( not B in F \/ G or b2 = b3 or b2 misses b3 ) let B be Subset of (X \/ Y); ::_thesis: ( not B in F \/ G or b1 = b2 or b1 misses b2 ) assume A5: B in F \/ G ; ::_thesis: ( b1 = b2 or b1 misses b2 ) percases ( ( A in F & B in F ) or ( A in G & B in G ) or ( A in F & B in G ) or ( A in G & B in F ) ) by A4, A5, XBOOLE_0:def_3; suppose ( ( A in F & B in F ) or ( A in G & B in G ) ) ; ::_thesis: ( b1 = b2 or b1 misses b2 ) hence ( A = B or A misses B ) by EQREL_1:def_4; ::_thesis: verum end; suppose ( ( A in F & B in G ) or ( A in G & B in F ) ) ; ::_thesis: ( b1 = b2 or b1 misses b2 ) hence ( A = B or A misses B ) by A1, XBOOLE_1:64; ::_thesis: verum end; end; end; hence F \/ G is a_partition of X \/ Y by A2, A3, EQREL_1:def_4; ::_thesis: verum end; theorem Th4: :: DILWORTH:4 for X, Y being set for F being a_partition of Y st Y c< X holds F \/ {(X \ Y)} is a_partition of X proof let X, Y be set ; ::_thesis: for F being a_partition of Y st Y c< X holds F \/ {(X \ Y)} is a_partition of X let F be a_partition of Y; ::_thesis: ( Y c< X implies F \/ {(X \ Y)} is a_partition of X ) assume A1: Y c< X ; ::_thesis: F \/ {(X \ Y)} is a_partition of 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; ::_thesis: verum end; theorem Th5: :: DILWORTH:5 for X being infinite set for n being Nat ex Y being finite Subset of X st card Y > n proof let X be infinite set ; ::_thesis: for n being Nat ex Y being finite Subset of X st card Y > n let n be Nat; ::_thesis: ex Y being finite Subset of X st card Y > n 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 | (Seg (n + 1)) as Function of (Seg (n + 1)),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 ; ::_thesis: card Y > n dom ff = Seg (n + 1) by FUNCT_2:def_1; then card (dom ff) = n + 1 by FINSEQ_1:57; hence card Y > n by A2, NAT_1:13; ::_thesis: verum end; begin definition let R be RelStr ; let S be Subset of R; attrS is connected means :Def1: :: DILWORTH:def 1 the InternalRel of R is_connected_in S; end; :: deftheorem Def1 defines connected DILWORTH:def_1_:_ for R being RelStr for S being Subset of R holds ( S is connected iff the InternalRel of R is_connected_in S ); notation let R be RelStr ; let S be Subset of R; synonym clique S for connected ; end; registration let R be RelStr ; cluster trivial -> clique for Element of bool the carrier of R; coherence for b1 being Subset of R st b1 is trivial holds b1 is clique proof let S be Subset of R; ::_thesis: ( S is trivial implies S is clique ) assume A1: S is trivial ; ::_thesis: S is clique let x1, x2 be set ; :: according to RELAT_2:def_6,DILWORTH:def_1 ::_thesis: ( not x1 in S or not x2 in S or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R ) thus ( not x1 in S or not x2 in S or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R ) by A1, ZFMISC_1:def_10; ::_thesis: verum end; end; registration let R be RelStr ; cluster clique for Element of bool the carrier of R; existence ex b1 being Subset of R st b1 is clique proof take {} R ; ::_thesis: {} R is clique let x1, x2 be set ; :: according to RELAT_2:def_6,DILWORTH:def_1 ::_thesis: ( not x1 in {} R or not x2 in {} R or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R ) thus ( not x1 in {} R or not x2 in {} R or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R ) ; ::_thesis: verum end; end; definition let R be RelStr ; mode Clique of R is clique Subset of R; end; theorem Th6: :: DILWORTH:6 for R being RelStr for S being Subset of R holds ( S is Clique of R iff for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds b <= a ) proof let R be RelStr ; ::_thesis: for S being Subset of R holds ( S is Clique of R iff for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds b <= a ) let S be Subset of R; ::_thesis: ( S is Clique of R iff for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds b <= a ) set RR = the InternalRel of R; hereby ::_thesis: ( ( for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds b <= a ) implies S is Clique of R ) assume S is Clique of R ; ::_thesis: for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds b <= a then A1: the InternalRel of R is_connected_in S by Def1; let a, b be Element of R; ::_thesis: ( a in S & b in S & a <> b & not a <= b implies b <= a ) assume ( a in S & b in S & a <> b ) ; ::_thesis: ( a <= b or b <= a ) then ( [a,b] in the InternalRel of R or [b,a] in the InternalRel of R ) by A1, RELAT_2:def_6; hence ( a <= b or b <= a ) by ORDERS_2:def_5; ::_thesis: verum end; assume A2: for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds b <= a ; ::_thesis: S is Clique of R the InternalRel of R is_connected_in S proof let x, y be set ; :: according to RELAT_2:def_6 ::_thesis: ( not x in S or not y in S or x = y or [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) assume A3: ( x in S & y in S & x <> y ) ; ::_thesis: ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) then reconsider x9 = x, y9 = y as Element of R ; ( x9 <= y9 or y9 <= x9 ) by A3, A2; hence ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) by ORDERS_2:def_5; ::_thesis: verum end; hence S is Clique of R by Def1; ::_thesis: verum end; registration let R be RelStr ; cluster finite connected for Element of bool the carrier of R; existence ex b1 being Clique of R st b1 is finite proof take {} R ; ::_thesis: {} R is finite thus {} R is finite ; ::_thesis: verum end; end; registration let R be reflexive RelStr ; cluster connected -> strongly_connected for Element of bool the carrier of R; coherence for b1 being Subset of R st b1 is connected holds b1 is strongly_connected proof let C be Subset of R; ::_thesis: ( C is connected implies C is strongly_connected ) set iR = the InternalRel of R; set cR = the carrier of R; assume C is clique ; ::_thesis: C is strongly_connected then A1: the InternalRel of R is_connected_in C by Def1; A2: the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def_2; thus C is strongly_connected ::_thesis: verum proof let x, y be set ; :: according to RELAT_2:def_7,ORDERS_2:def_7 ::_thesis: ( not x in C or not y in C or [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) assume that A3: x in C and A4: y in C ; ::_thesis: ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) percases ( x = y or x <> y ) ; suppose x = y ; ::_thesis: ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) hence ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) by A3, A2, RELAT_2:def_1; ::_thesis: verum end; suppose x <> y ; ::_thesis: ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) hence ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) by A3, A4, A1, RELAT_2:def_6; ::_thesis: verum end; end; end; end; end; registration let R be non empty RelStr ; cluster non empty finite connected for Element of bool the carrier of R; existence ex b1 being Clique of R st ( b1 is finite & not b1 is empty ) proof { the Element of R} is clique ; hence ex b1 being Clique of R st ( b1 is finite & not b1 is empty ) ; ::_thesis: verum end; end; theorem :: DILWORTH:7 for R being non empty RelStr for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is Clique of R & not a1 <= a2 holds a2 <= a1 proof let R be non empty RelStr ; ::_thesis: for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is Clique of R & not a1 <= a2 holds a2 <= a1 let a1, a2 be Element of R; ::_thesis: ( a1 <> a2 & {a1,a2} is Clique of R & not a1 <= a2 implies a2 <= a1 ) assume A1: a1 <> a2 ; ::_thesis: ( not {a1,a2} is Clique of R or a1 <= a2 or a2 <= a1 ) A2: ( a1 in {a1,a2} & a2 in {a1,a2} ) by TARSKI:def_2; assume {a1,a2} is Clique of R ; ::_thesis: ( a1 <= a2 or a2 <= a1 ) hence ( a1 <= a2 or a2 <= a1 ) by A2, A1, Th6; ::_thesis: verum end; theorem Th8: :: DILWORTH:8 for R being non empty RelStr for a1, a2 being Element of R st ( a1 <= a2 or a2 <= a1 ) holds {a1,a2} is Clique of R proof let R be non empty RelStr ; ::_thesis: for a1, a2 being Element of R st ( a1 <= a2 or a2 <= a1 ) holds {a1,a2} is Clique of R let a1, a2 be Element of R; ::_thesis: ( ( a1 <= a2 or a2 <= a1 ) implies {a1,a2} is Clique of R ) assume A1: ( a1 <= a2 or a2 <= a1 ) ; ::_thesis: {a1,a2} is Clique of R now__::_thesis:_for_x,_y_being_Element_of_R_st_x_in_{a1,a2}_&_y_in_{a1,a2}_&_x_<>_y_&_not_x_<=_y_holds_ y_<=_x let x, y be Element of R; ::_thesis: ( x in {a1,a2} & y in {a1,a2} & x <> y & not x <= y implies y <= x ) assume ( x in {a1,a2} & y in {a1,a2} ) ; ::_thesis: ( not x <> y or x <= y or y <= x ) then A2: ( ( x = a1 or x = a2 ) & ( y = a1 or y = a2 ) ) by TARSKI:def_2; assume x <> y ; ::_thesis: ( x <= y or y <= x ) hence ( x <= y or y <= x ) by A1, A2; ::_thesis: verum end; hence {a1,a2} is Clique of R by Th6; ::_thesis: verum end; theorem Th9: :: DILWORTH:9 for R being RelStr for C being Clique of R for S being Subset of C holds S is Clique of R proof let R be RelStr ; ::_thesis: for C being Clique of R for S being Subset of C holds S is Clique of R let C be Clique of R; ::_thesis: for S being Subset of C holds S is Clique of R let S be Subset of C; ::_thesis: S is Clique of R set iR = the InternalRel of R; A1: the InternalRel of R is_connected_in C by Def1; the InternalRel of R is_connected_in S proof let x1, x2 be set ; :: according to RELAT_2:def_6 ::_thesis: ( not x1 in S or not x2 in S or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R ) assume ( x1 in S & x2 in S & x1 <> x2 ) ; ::_thesis: ( [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R ) hence ( [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R ) by A1, RELAT_2:def_6; ::_thesis: verum end; hence S is Clique of R by Def1, XBOOLE_1:1; ::_thesis: verum end; theorem :: DILWORTH:10 for R being RelStr for C being finite Clique of R for n being Nat st n <= card C holds ex B being finite Clique of R st ( B c= C & card B = n ) proof let R be RelStr ; ::_thesis: for C being finite Clique of R for n being Nat st n <= card C holds ex B being finite Clique of R st ( B c= C & card B = n ) let C be finite Clique of R; ::_thesis: for n being Nat st n <= card C holds ex B being finite Clique of R st ( B c= C & card B = n ) let n be Nat; ::_thesis: ( n <= card C implies ex B being finite Clique of R st ( B c= C & card B = n ) ) assume A1: n <= card C ; ::_thesis: ex B being finite Clique of R st ( B c= C & card B = n ) consider BB being finite Subset of C such that A2: card BB = n by A1, FINSEQ_4:72; reconsider BB = BB as finite Clique of R by Th9; take BB ; ::_thesis: ( BB c= C & card BB = n ) thus ( BB c= C & card BB = n ) by A2; ::_thesis: verum end; theorem Th11: :: DILWORTH:11 for R being transitive RelStr for C being Clique of R for x, y being Element of R st x is_maximal_in C & x <= y holds C \/ {y} is Clique of R proof let R be transitive RelStr ; ::_thesis: for C being Clique of R for x, y being Element of R st x is_maximal_in C & x <= y holds C \/ {y} is Clique of R let C be Clique of R; ::_thesis: for x, y being Element of R st x is_maximal_in C & x <= y holds C \/ {y} is Clique of R let x, y be Element of R; ::_thesis: ( x is_maximal_in C & x <= y implies C \/ {y} is Clique of R ) assume that A1: x is_maximal_in C and A2: x <= y ; ::_thesis: C \/ {y} is Clique of R A3: x in C by A1, WAYBEL_4:55; A4: not the carrier of R is empty by A1, WAYBEL_4:55; set Cb = C \/ {y}; A5: C \/ {y} c= the carrier of R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C \/ {y} or x in the carrier of R ) assume A6: x in C \/ {y} ; ::_thesis: x in the carrier of R percases ( x in C or x in {y} ) by A6, XBOOLE_0:def_3; suppose x in C ; ::_thesis: x in the carrier of R hence x in the carrier of R ; ::_thesis: verum end; suppose x in {y} ; ::_thesis: x in the carrier of R then x = y by TARSKI:def_1; hence x in the carrier of R by A4; ::_thesis: verum end; end; end; now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_C_\/_{y}_&_b_in_C_\/_{y}_&_a_<>_b_&_not_a_<=_b_holds_ b_<=_a let a, b be Element of R; ::_thesis: ( a in C \/ {y} & b in C \/ {y} & a <> b & not b1 <= b2 implies b2 <= b1 ) assume that A7: ( a in C \/ {y} & b in C \/ {y} ) and A8: a <> b ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) percases ( ( a in C & b in C ) or ( a in C & b in {y} ) or ( a in {y} & b in C ) or ( a in {y} & b in {y} ) ) by A7, XBOOLE_0:def_3; suppose ( a in C & b in C ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) hence ( a <= b or b <= a ) by A8, Th6; ::_thesis: verum end; supposethat A9: a in C and A10: b in {y} ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) A11: b = y by A10, TARSKI:def_1; A12: not x < a by A1, A9, WAYBEL_4:55; percases ( x <> a or x = a ) ; suppose x <> a ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) then ( a <= x or x <= a ) by A9, A3, Th6; hence ( a <= b or b <= a ) by A2, A11, A12, ORDERS_2:3, ORDERS_2:def_6; ::_thesis: verum end; suppose x = a ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) hence ( a <= b or b <= a ) by A2, A10, TARSKI:def_1; ::_thesis: verum end; end; end; supposethat A13: a in {y} and A14: b in C ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) A15: a = y by A13, TARSKI:def_1; A16: not x < b by A1, A14, WAYBEL_4:55; percases ( x <> b or x = b ) ; suppose x <> b ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) then ( b <= x or x <= b ) by A14, A3, Th6; hence ( a <= b or b <= a ) by A2, A15, A16, ORDERS_2:3, ORDERS_2:def_6; ::_thesis: verum end; suppose x = b ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) hence ( a <= b or b <= a ) by A2, A13, TARSKI:def_1; ::_thesis: verum end; end; end; suppose ( a in {y} & b in {y} ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) then ( a = y & b = y ) by TARSKI:def_1; hence ( a <= b or b <= a ) by A8; ::_thesis: verum end; end; end; hence C \/ {y} is Clique of R by A5, Th6; ::_thesis: verum end; theorem Th12: :: DILWORTH:12 for R being transitive RelStr for C being Clique of R for x, y being Element of R st x is_minimal_in C & y <= x holds C \/ {y} is Clique of R proof let R be transitive RelStr ; ::_thesis: for C being Clique of R for x, y being Element of R st x is_minimal_in C & y <= x holds C \/ {y} is Clique of R let C be Clique of R; ::_thesis: for x, y being Element of R st x is_minimal_in C & y <= x holds C \/ {y} is Clique of R let x, y be Element of R; ::_thesis: ( x is_minimal_in C & y <= x implies C \/ {y} is Clique of R ) assume that A1: x is_minimal_in C and A2: y <= x ; ::_thesis: C \/ {y} is Clique of R A3: x in C by A1, WAYBEL_4:56; A4: not the carrier of R is empty by A1, WAYBEL_4:56; set Cb = C \/ {y}; A5: C \/ {y} c= the carrier of R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C \/ {y} or x in the carrier of R ) assume A6: x in C \/ {y} ; ::_thesis: x in the carrier of R percases ( x in C or x in {y} ) by A6, XBOOLE_0:def_3; suppose x in C ; ::_thesis: x in the carrier of R hence x in the carrier of R ; ::_thesis: verum end; suppose x in {y} ; ::_thesis: x in the carrier of R then x = y by TARSKI:def_1; hence x in the carrier of R by A4; ::_thesis: verum end; end; end; now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_C_\/_{y}_&_b_in_C_\/_{y}_&_a_<>_b_&_not_a_<=_b_holds_ b_<=_a let a, b be Element of R; ::_thesis: ( a in C \/ {y} & b in C \/ {y} & a <> b & not b1 <= b2 implies b2 <= b1 ) assume that A7: ( a in C \/ {y} & b in C \/ {y} ) and A8: a <> b ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) percases ( ( a in C & b in C ) or ( a in C & b in {y} ) or ( a in {y} & b in C ) or ( a in {y} & b in {y} ) ) by A7, XBOOLE_0:def_3; suppose ( a in C & b in C ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) hence ( a <= b or b <= a ) by A8, Th6; ::_thesis: verum end; supposethat A9: a in C and A10: b in {y} ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) A11: b = y by A10, TARSKI:def_1; A12: not a < x by A1, A9, WAYBEL_4:56; percases ( a <> x or x = a ) ; supposeA13: a <> x ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) 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; ::_thesis: verum end; suppose x = a ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) hence ( a <= b or b <= a ) by A2, A10, TARSKI:def_1; ::_thesis: verum end; end; end; supposethat A14: a in {y} and A15: b in C ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) A16: a = y by A14, TARSKI:def_1; A17: not b < x by A1, A15, WAYBEL_4:56; percases ( b <> x or x = b ) ; supposeA18: b <> x ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) 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; ::_thesis: verum end; suppose x = b ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) hence ( a <= b or b <= a ) by A2, A14, TARSKI:def_1; ::_thesis: verum end; end; end; suppose ( a in {y} & b in {y} ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) then ( a = y & b = y ) by TARSKI:def_1; hence ( a <= b or b <= a ) by A8; ::_thesis: verum end; end; end; hence C \/ {y} is Clique of R by A5, Th6; ::_thesis: verum end; definition let R be RelStr ; let S be Subset of R; attrS is stable means :Def2: :: DILWORTH:def 2 for x, y being Element of R st x in S & y in S & x <> y holds ( not x <= y & not y <= x ); end; :: deftheorem Def2 defines stable DILWORTH:def_2_:_ for R being RelStr for S being Subset of R holds ( S is stable iff for x, y being Element of R st x in S & y in S & x <> y holds ( not x <= y & not y <= x ) ); registration let R be RelStr ; cluster trivial -> stable for Element of bool the carrier of R; coherence for b1 being Subset of R st b1 is trivial holds b1 is stable proof let S be Subset of R; ::_thesis: ( S is trivial implies S is stable ) assume A1: S is trivial ; ::_thesis: S is stable let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in S & y in S & x <> y implies ( not x <= y & not y <= x ) ) thus ( x in S & y in S & x <> y implies ( not x <= y & not y <= x ) ) by A1, ZFMISC_1:def_10; ::_thesis: verum end; end; registration let R be RelStr ; cluster stable for Element of bool the carrier of R; existence ex b1 being Subset of R st b1 is stable proof reconsider A = {} as Subset of R by XBOOLE_1:2; take A ; ::_thesis: A is stable let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in A & y in A & x <> y implies ( not x <= y & not y <= x ) ) thus ( x in A & y in A & x <> y implies ( not x <= y & not y <= x ) ) ; ::_thesis: verum end; end; definition let R be RelStr ; mode StableSet of R is stable Subset of R; end; registration let R be RelStr ; cluster finite stable for Element of bool the carrier of R; existence ex b1 being StableSet of R st b1 is finite proof take {} R ; ::_thesis: {} R is finite thus {} R is finite ; ::_thesis: verum end; end; registration let R be non empty RelStr ; cluster non empty finite stable for Element of bool the carrier of R; existence ex b1 being StableSet of R st ( b1 is finite & not b1 is empty ) proof { the Element of R} is stable ; hence ex b1 being StableSet of R st ( b1 is finite & not b1 is empty ) ; ::_thesis: verum end; end; theorem :: DILWORTH:13 for R being non empty RelStr for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is StableSet of R holds ( not a1 <= a2 & not a2 <= a1 ) proof let R be non empty RelStr ; ::_thesis: for a1, a2 being Element of R st a1 <> a2 & {a1,a2} is StableSet of R holds ( not a1 <= a2 & not a2 <= a1 ) let a1, a2 be Element of R; ::_thesis: ( a1 <> a2 & {a1,a2} is StableSet of R implies ( not a1 <= a2 & not a2 <= a1 ) ) assume A1: a1 <> a2 ; ::_thesis: ( not {a1,a2} is StableSet of R or ( not a1 <= a2 & not a2 <= a1 ) ) A2: ( a1 in {a1,a2} & a2 in {a1,a2} ) by TARSKI:def_2; assume {a1,a2} is StableSet of R ; ::_thesis: ( not a1 <= a2 & not a2 <= a1 ) hence ( not a1 <= a2 & not a2 <= a1 ) by A2, A1, Def2; ::_thesis: verum end; theorem Th14: :: DILWORTH:14 for R being non empty RelStr for a1, a2 being Element of R holds ( a1 <= a2 or a2 <= a1 or {a1,a2} is StableSet of R ) proof let R be non empty RelStr ; ::_thesis: for a1, a2 being Element of R holds ( a1 <= a2 or a2 <= a1 or {a1,a2} is StableSet of R ) let a1, a2 be Element of R; ::_thesis: ( a1 <= a2 or a2 <= a1 or {a1,a2} is StableSet of R ) assume A1: ( not a1 <= a2 & not a2 <= a1 ) ; ::_thesis: {a1,a2} is StableSet of R set S = {a1,a2}; {a1,a2} is stable proof let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in {a1,a2} & y in {a1,a2} & x <> y implies ( not x <= y & not y <= x ) ) assume A2: ( x in {a1,a2} & y in {a1,a2} & x <> y ) ; ::_thesis: ( not x <= y & not y <= x ) ( ( x = a1 or x = a2 ) & ( y = a1 or y = a2 ) ) by A2, TARSKI:def_2; hence ( not x <= y & not y <= x ) by A1, A2; ::_thesis: verum end; hence {a1,a2} is StableSet of R ; ::_thesis: verum end; theorem Th15: :: DILWORTH:15 for R being RelStr for C being Clique of R for A being StableSet of R for a, b being set st a in A & b in A & a in C & b in C holds a = b proof let R be RelStr ; ::_thesis: for C being Clique of R for A being StableSet of R for a, b being set st a in A & b in A & a in C & b in C holds a = b let C be Clique of R; ::_thesis: for A being StableSet of R for a, b being set st a in A & b in A & a in C & b in C holds a = b let A be StableSet of R; ::_thesis: for a, b being set st a in A & b in A & a in C & b in C holds a = b let a, b be set ; ::_thesis: ( a in A & b in A & a in C & b in C implies a = b ) assume that A1: ( a in A & b in A ) and A2: ( a in C & b in C ) ; ::_thesis: a = b assume A3: a <> b ; ::_thesis: contradiction 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; ::_thesis: verum end; theorem Th16: :: DILWORTH:16 for R being RelStr for A being StableSet of R for B being Subset of A holds B is StableSet of R proof let R be RelStr ; ::_thesis: for A being StableSet of R for B being Subset of A holds B is StableSet of R let A be StableSet of R; ::_thesis: for B being Subset of A holds B is StableSet of R let B be Subset of A; ::_thesis: B is StableSet of R reconsider BB = B as Subset of R by XBOOLE_1:1; BB is stable proof let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in BB & y in BB & x <> y implies ( not x <= y & not y <= x ) ) assume A1: ( x in BB & y in BB & x <> y ) ; ::_thesis: ( not x <= y & not y <= x ) thus ( not x <= y & not y <= x ) by A1, Def2; ::_thesis: verum end; hence B is StableSet of R ; ::_thesis: verum end; theorem Th17: :: DILWORTH:17 for R being RelStr for A being finite StableSet of R for n being Nat st n <= card A holds ex B being finite StableSet of R st card B = n proof let R be RelStr ; ::_thesis: for A being finite StableSet of R for n being Nat st n <= card A holds ex B being finite StableSet of R st card B = n let A be finite StableSet of R; ::_thesis: for n being Nat st n <= card A holds ex B being finite StableSet of R st card B = n let n be Nat; ::_thesis: ( n <= card A implies ex B being finite StableSet of R st card B = n ) assume A1: n <= card A ; ::_thesis: ex B being finite StableSet of R st card B = n consider BB being finite Subset of A such that A2: card BB = n by A1, FINSEQ_4:72; reconsider BB = BB as finite StableSet of R by Th16; take BB ; ::_thesis: card BB = n thus card BB = n by A2; ::_thesis: verum end; begin definition let R be RelStr ; attrR is with_finite_clique# means :Def3: :: DILWORTH:def 3 ex C being finite Clique of R st for D being finite Clique of R holds card D <= card C; end; :: deftheorem Def3 defines with_finite_clique# DILWORTH:def_3_:_ for R being RelStr holds ( R is with_finite_clique# iff ex C being finite Clique of R st for D being finite Clique of R holds card D <= card C ); registration cluster finite -> with_finite_clique# for RelStr ; coherence for b1 being RelStr st b1 is finite holds b1 is with_finite_clique# proof let R be RelStr ; ::_thesis: ( R is finite implies R is with_finite_clique# ) assume R is finite ; ::_thesis: R is with_finite_clique# then reconsider R9 = R as finite RelStr ; defpred S1[ Nat] means ex c being finite Clique of R st card c = c1; A1: for k being Nat st S1[k] holds k <= card R9 by NAT_1:43; card ({} R) = 0 ; then A2: ex k being Nat st S1[k] ; consider k being Nat such that A3: S1[k] and A4: for n being Nat st S1[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 being finite Clique of R holds card D <= card c by A5, A4; hence R is with_finite_clique# by Def3; ::_thesis: verum end; end; registration let R be with_finite_clique# RelStr ; cluster connected -> finite for Element of bool the carrier of R; coherence for b1 being Clique of R holds b1 is finite proof let D be Clique of R; ::_thesis: D is finite 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; end; definition let R be with_finite_clique# RelStr ; func clique# R -> Nat means :Def4: :: DILWORTH:def 4 ( ex C being finite Clique of R st card C = it & ( for T being finite Clique of R holds card T <= it ) ); existence ex b1 being Nat st ( ex C being finite Clique of R st card C = b1 & ( for T being finite Clique of R holds card T <= b1 ) ) 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; ::_thesis: ( ex C being finite Clique of R st card C = itt & ( for T being finite Clique of R holds card T <= itt ) ) thus ex A being finite Clique of R st card A = itt ; ::_thesis: for T being finite Clique of R holds card T <= itt let T be finite Clique of R; ::_thesis: card T <= itt thus card T <= itt by A1; ::_thesis: verum end; uniqueness for b1, b2 being Nat st ex C being finite Clique of R st card C = b1 & ( for T being finite Clique of R holds card T <= b1 ) & ex C being finite Clique of R st card C = b2 & ( for T being finite Clique of R holds card T <= b2 ) holds b1 = b2 proof let it1, it2 be Nat; ::_thesis: ( ex C being finite Clique of R st card C = it1 & ( for T being finite Clique of R holds card T <= it1 ) & ex C being finite Clique of R st card C = it2 & ( for T being finite Clique of R holds card T <= it2 ) implies it1 = it2 ) assume 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 ; ::_thesis: it1 = 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; ::_thesis: verum end; end; :: deftheorem Def4 defines clique# DILWORTH:def_4_:_ for R being with_finite_clique# RelStr for b2 being Nat holds ( b2 = clique# R iff ( ex C being finite Clique of R st card C = b2 & ( for T being finite Clique of R holds card T <= b2 ) ) ); registration let R be empty RelStr ; cluster clique# R -> empty ; coherence clique# R is empty proof for T being Clique of R holds card T <= card ({} R) ; hence clique# R is empty by Def4; ::_thesis: verum end; end; registration let R be non empty with_finite_clique# RelStr ; cluster clique# R -> positive ; coherence clique# R is positive proof card { the Element of R} <= clique# R by Def4; hence clique# R is positive ; ::_thesis: verum end; end; theorem :: DILWORTH:18 for R being non empty with_finite_clique# RelStr st [#] R is StableSet of R holds clique# R = 1 proof let R be non empty with_finite_clique# RelStr ; ::_thesis: ( [#] R is StableSet of R implies clique# R = 1 ) assume A1: [#] R is StableSet of R ; ::_thesis: clique# R = 1 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 ; ::_thesis: contradiction 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 contradiction by A4, A5, A6, A1, Th15; ::_thesis: verum end; theorem Th19: :: DILWORTH:19 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 ; ::_thesis: ( clique# R = 1 implies [#] R is StableSet of R ) assume A1: clique# R = 1 ; ::_thesis: [#] R is StableSet of R set cR = the carrier of R; A2: not R is empty by A1; now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_the_carrier_of_R_&_b_in_the_carrier_of_R_&_a_<>_b_holds_ (_not_a_<=_b_&_not_b_<=_a_) let a, b be Element of R; ::_thesis: ( a in the carrier of R & b in the carrier of R & a <> b implies ( not a <= b & not b <= a ) ) assume that a in the carrier of R and b in the carrier of R and A3: a <> b ; ::_thesis: ( not a <= b & not b <= a ) assume ( a <= b or b <= a ) ; ::_thesis: contradiction 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; ::_thesis: verum end; hence [#] R is StableSet of R by Def2; ::_thesis: verum end; definition let R be RelStr ; attrR is with_finite_stability# means :Def5: :: DILWORTH:def 5 ex A being finite StableSet of R st for B being finite StableSet of R holds card B <= card A; end; :: deftheorem Def5 defines with_finite_stability# DILWORTH:def_5_:_ for R being RelStr holds ( R is with_finite_stability# iff ex A being finite StableSet of R st for B being finite StableSet of R holds card B <= card A ); registration cluster finite -> with_finite_stability# for RelStr ; coherence for b1 being RelStr st b1 is finite holds b1 is with_finite_stability# proof let R be RelStr ; ::_thesis: ( R is finite implies R is with_finite_stability# ) assume R is finite ; ::_thesis: R is with_finite_stability# then reconsider R9 = R as finite RelStr ; defpred S1[ Nat] means ex A being finite StableSet of R9 st card A = c1; A1: for k being Nat st S1[k] holds k <= card R9 by NAT_1:43; ( {} R is StableSet of R & card {} = 0 ) ; then A2: ex k being Nat st S1[k] ; consider k being Nat such that A3: S1[k] and A4: for n being Nat st S1[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 ; :: according to DILWORTH:def_5 ::_thesis: for B being finite StableSet of R holds card B <= card S let T be finite StableSet of R; ::_thesis: card T <= card S thus card T <= card S by A5, A4; ::_thesis: verum end; end; registration let R be with_finite_stability# RelStr ; cluster stable -> finite for Element of bool the carrier of R; coherence for b1 being StableSet of R holds b1 is finite 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; end; definition let R be with_finite_stability# RelStr ; func stability# R -> Nat means :Def6: :: DILWORTH:def 6 ( ex A being finite StableSet of R st card A = it & ( for T being finite StableSet of R holds card T <= it ) ); existence ex b1 being Nat st ( ex A being finite StableSet of R st card A = b1 & ( for T being finite StableSet of R holds card T <= b1 ) ) 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; ::_thesis: ( ex A being finite StableSet of R st card A = itt & ( for T being finite StableSet of R holds card T <= itt ) ) thus ex A being finite StableSet of R st card A = itt ; ::_thesis: for T being finite StableSet of R holds card T <= itt let T be finite StableSet of R; ::_thesis: card T <= itt thus card T <= itt by A1; ::_thesis: verum end; uniqueness for b1, b2 being Nat st ex A being finite StableSet of R st card A = b1 & ( for T being finite StableSet of R holds card T <= b1 ) & ex A being finite StableSet of R st card A = b2 & ( for T being finite StableSet of R holds card T <= b2 ) holds b1 = b2 proof let it1, it2 be Nat; ::_thesis: ( ex A being finite StableSet of R st card A = it1 & ( for T being finite StableSet of R holds card T <= it1 ) & ex A being finite StableSet of R st card A = it2 & ( for T being finite StableSet of R holds card T <= it2 ) implies it1 = it2 ) assume 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 ; ::_thesis: it1 = 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; ::_thesis: verum end; end; :: deftheorem Def6 defines stability# DILWORTH:def_6_:_ for R being with_finite_stability# RelStr for b2 being Nat holds ( b2 = stability# R iff ( ex A being finite StableSet of R st card A = b2 & ( for T being finite StableSet of R holds card T <= b2 ) ) ); registration let R be empty RelStr ; cluster stability# R -> empty ; coherence stability# R is empty proof for T being StableSet of R holds card T <= card ({} R) ; hence stability# R is empty by Def6; ::_thesis: verum end; end; registration let R be non empty with_finite_stability# RelStr ; cluster stability# R -> positive ; coherence stability# R is positive proof card { the Element of R} <= stability# R by Def6; hence stability# R is positive ; ::_thesis: verum end; end; theorem Th20: :: DILWORTH:20 for R being non empty with_finite_stability# RelStr st [#] R is Clique of R holds stability# R = 1 proof let R be non empty with_finite_stability# RelStr ; ::_thesis: ( [#] R is Clique of R implies stability# R = 1 ) assume A1: [#] R is Clique of R ; ::_thesis: stability# R = 1 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 ; ::_thesis: contradiction 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 contradiction by A4, A5, A6, A1, Th15; ::_thesis: verum end; theorem Th21: :: DILWORTH:21 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 ; ::_thesis: ( stability# R = 1 implies [#] R is Clique of R ) assume A1: stability# R = 1 ; ::_thesis: [#] R is Clique of R set cR = the carrier of R; now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_the_carrier_of_R_&_b_in_the_carrier_of_R_&_a_<>_b_&_not_a_<=_b_holds_ b_<=_a let a, b be Element of R; ::_thesis: ( a in the carrier of R & b in the carrier of R & a <> b & not a <= b implies b <= a ) assume that A2: a in the carrier of R and b in the carrier of R and A3: a <> b ; ::_thesis: ( a <= b or b <= a ) A4: not R is empty by A2; assume ( not a <= b & not b <= a ) ; ::_thesis: contradiction 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; ::_thesis: verum end; hence [#] R is Clique of R by Th6; ::_thesis: verum end; registration cluster with_finite_clique# with_finite_stability# -> finite for RelStr ; coherence for b1 being RelStr st b1 is with_finite_clique# & b1 is with_finite_stability# holds b1 is finite proof let R be RelStr ; ::_thesis: ( R is with_finite_clique# & R is with_finite_stability# implies R is finite ) assume A1: R is with_finite_clique# ; ::_thesis: ( not R is with_finite_stability# or R is finite ) assume A2: R is with_finite_stability# ; ::_thesis: R is finite assume A3: R is infinite ; ::_thesis: contradiction reconsider R = 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; set w = stability# R; A6: 0 + 1 <= clique# R by A3, NAT_1:13; A7: 0 + 1 <= stability# R by A3, NAT_1:13; set cR = the carrier of R; A8: the carrier of R = [#] R ; percases ( clique# R = 1 or stability# R = 1 or ( clique# R > 1 & stability# R > 1 ) ) by A6, A7, XXREAL_0:1; suppose clique# R = 1 ; ::_thesis: contradiction then A9: the carrier of R is StableSet of R by A8, Th19; consider Y being finite Subset of the carrier of R such that A10: card Y > stability# R by A3, Th5; Y is StableSet of R by A9, Th16; hence contradiction by A10, Def6; ::_thesis: verum end; suppose stability# R = 1 ; ::_thesis: contradiction then A11: the carrier of R is Clique of R by A8, Th21; consider Y being finite Subset of the carrier of R such that A12: card Y > clique# R by A3, Th5; Y is Clique of R by A11, Th9; hence contradiction by A12, Def4; ::_thesis: verum end; supposeA13: ( clique# R > 1 & stability# R > 1 ) ; ::_thesis: contradiction set m = (max ((clique# R),(stability# R))) + 1; reconsider m = (max ((clique# R),(stability# R))) + 1 as Nat ; consider r being Nat such that A14: for X being finite set for 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 = (Y \/ An) \/ C 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 & not y <= x ) } ; set E = the_subsets_of_card (2,X); set P = { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } }; A17: { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } c= the_subsets_of_card (2,X) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or x in the_subsets_of_card (2,X) ) assume x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } ; ::_thesis: x in the_subsets_of_card (2,X) 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 x in the_subsets_of_card (2,X) ; ::_thesis: verum end; A22: { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } c= the_subsets_of_card (2,X) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } or x in the_subsets_of_card (2,X) ) assume x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ; ::_thesis: x in the_subsets_of_card (2,X) 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 & not yy <= xx ) ; ( x is Subset of X & card x = 2 ) by A23, A24, A25, A26, CARD_2:57, ZFMISC_1:32; hence x in the_subsets_of_card (2,X) ; ::_thesis: verum end; A27: ( { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } & { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ) by TARSKI:def_2; A28: now__::_thesis:_not__{__{x,y}_where_x,_y_is_Element_of_R_:_(_x_<>_y_&_x_in_X_&_y_in_X_&_(_x_<=_y_or_y_<=_x_)_)__}__=__{__{x,y}_where_x,_y_is_Element_of_R_:_(_x_<>_y_&_x_in_X_&_y_in_X_&_not_x_<=_y_&_not_y_<=_x_)__}_ assume A29: { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ; ::_thesis: contradiction 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 = a, b = b as Element of R by A30, A31; A33: ( not a <= b & not 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 { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } 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; ::_thesis: verum end; A36: { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } c= bool (the_subsets_of_card (2,X)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or x in bool (the_subsets_of_card (2,X)) ) assume x in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ; ::_thesis: x in bool (the_subsets_of_card (2,X)) then x c= the_subsets_of_card (2,X) by A17, A22, TARSKI:def_2; hence x in bool (the_subsets_of_card (2,X)) ; ::_thesis: verum end; A37: union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } = the_subsets_of_card (2,X) proof thus union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } c= the_subsets_of_card (2,X) :: according to XBOOLE_0:def_10 ::_thesis: the_subsets_of_card (2,X) c= union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or x in the_subsets_of_card (2,X) ) assume x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ; ::_thesis: x in the_subsets_of_card (2,X) then consider Y being set such that A38: x in Y and A39: Y in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } by TARSKI:def_4; ( Y = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or Y = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) by A39, TARSKI:def_2; hence x in the_subsets_of_card (2,X) by A38, A17, A22; ::_thesis: verum end; thus the_subsets_of_card (2,X) c= union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the_subsets_of_card (2,X) or x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ) assume x in the_subsets_of_card (2,X) ; ::_thesis: x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } 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 = a, b = b as Element of R ; A44: ( a in xx & b in xx ) by A43, TARSKI:def_2; ( ( not a <= b & not b <= a ) or a <= b or b <= a ) ; then ( {a,b} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or {a,b} in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) by A44, A42; hence x in union { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } by A40, A43, A27, TARSKI:def_4; ::_thesis: verum end; end; for a being Subset of (the_subsets_of_card (2,X)) st a in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } holds ( a <> {} & ( for b being Subset of (the_subsets_of_card (2,X)) holds ( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b ) ) ) proof let a be Subset of (the_subsets_of_card (2,X)); ::_thesis: ( a in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } implies ( a <> {} & ( for b being Subset of (the_subsets_of_card (2,X)) holds ( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b ) ) ) ) assume A45: a in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ; ::_thesis: ( a <> {} & ( for b being Subset of (the_subsets_of_card (2,X)) holds ( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b ) ) ) thus a <> {} ::_thesis: for b being Subset of (the_subsets_of_card (2,X)) holds ( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b ) proof percases ( a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) by A45, TARSKI:def_2; supposeA46: a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } ; ::_thesis: 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 = aa, bb = 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 { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } by A50, A49; hence a <> {} by A46; ::_thesis: verum end; supposeA51: a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ; ::_thesis: a <> {} 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 = aa, bb = bb as Element of R by A52, A53; A55: ( not aa <= bb & not 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 { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by A55, A54; hence a <> {} by A51; ::_thesis: verum end; end; end; let b be Subset of (the_subsets_of_card (2,X)); ::_thesis: ( not b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } or a = b or a misses b ) assume A56: b in { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } ; ::_thesis: ( a = b or a misses b ) assume A57: a <> b ; ::_thesis: a misses b assume A58: a meets b ; ::_thesis: contradiction ( ( a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or a = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) & ( b = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or b = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) ) by A45, A56, TARSKI:def_2; then { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } /\ { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } <> {} by A57, A58, XBOOLE_0:def_7; then consider x being set such that A59: x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } /\ { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } by XBOOLE_0:def_1; x in { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } 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 { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } 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 & not y2 <= x2 ) ; ( ( xx = x2 & yy = y2 ) or ( xx = y2 & yy = x2 ) ) by A60, A62, ZFMISC_1:6; hence contradiction by A61, A63; ::_thesis: verum end; then reconsider P = { { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } , { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } } as a_partition of the_subsets_of_card (2,X) 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 = 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; percases ( p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } or p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ) by TARSKI:def_2; supposeA69: p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } ; ::_thesis: contradiction now__::_thesis:_for_x,_y_being_Element_of_R_st_x_in_S_&_y_in_S_&_x_<>_y_&_not_x_<=_y_holds_ y_<=_x let x, y be Element of R; ::_thesis: ( x in S & y in S & x <> y & not x <= y implies y <= x ) assume that A70: x in S and A71: y in S and A72: x <> y ; ::_thesis: ( x <= y or y <= x ) ( {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 { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & ( x <= y or y <= x ) ) } 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; ::_thesis: verum end; then S is Clique of R by Th6; hence contradiction by A66, Def4; ::_thesis: verum end; supposeA75: p = { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } ; ::_thesis: contradiction S is stable proof let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in S & y in S & x <> y implies ( not x <= y & not y <= x ) ) assume that A76: x in S and A77: y in S and A78: x <> y ; ::_thesis: ( not x <= y & not y <= x ) ( {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 { {x,y} where x, y is Element of R : ( x <> y & x in X & y in X & not x <= y & not y <= x ) } 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 & not 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; ::_thesis: verum end; hence contradiction by A67, Def6; ::_thesis: verum end; end; end; end; end; end; begin definition let R be RelStr ; let X be Subset of R; func Lower X -> Subset of R equals :: DILWORTH:def 7 X \/ (downarrow X); coherence X \/ (downarrow X) is Subset of R ; func Upper X -> Subset of R equals :: DILWORTH:def 8 X \/ (uparrow X); coherence X \/ (uparrow X) is Subset of R ; end; :: deftheorem defines Lower DILWORTH:def_7_:_ for R being RelStr for X being Subset of R holds Lower X = X \/ (downarrow X); :: deftheorem defines Upper DILWORTH:def_8_:_ for R being RelStr for X being Subset of R holds Upper X = X \/ (uparrow X); theorem Th22: :: DILWORTH:22 for R being transitive antisymmetric RelStr for A being StableSet of R for z being set st z in Upper A & z in Lower A holds z in A proof let R be transitive antisymmetric RelStr ; ::_thesis: for A being StableSet of R for z being set st z in Upper A & z in Lower A holds z in A let A be StableSet of R; ::_thesis: for z being set st z in Upper A & z in Lower A holds z in A let z be set ; ::_thesis: ( z in Upper A & z in Lower A implies z in A ) assume that A1: z in Upper A and A2: z in Lower A ; ::_thesis: z in A percases ( z in A or not z in A ) ; suppose z in A ; ::_thesis: z in A hence z in A ; ::_thesis: verum end; supposeA3: not z in A ; ::_thesis: 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; ::_thesis: verum end; end; end; theorem Th23: :: DILWORTH:23 for R being with_finite_stability# RelStr for A being StableSet of R st card A = stability# R holds (Upper A) \/ (Lower A) = [#] R proof let R be with_finite_stability# RelStr ; ::_thesis: for A being StableSet of R st card A = stability# R holds (Upper A) \/ (Lower A) = [#] R let A be StableSet of R; ::_thesis: ( card A = stability# R implies (Upper A) \/ (Lower A) = [#] R ) assume A1: card A = stability# R ; ::_thesis: (Upper A) \/ (Lower A) = [#] R set cP = the carrier of R; the carrier of R c= (Upper A) \/ (Lower A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R or x in (Upper A) \/ (Lower A) ) assume A2: x in the carrier of R ; ::_thesis: x in (Upper A) \/ (Lower A) assume A3: not x in (Upper A) \/ (Lower A) ; ::_thesis: contradiction reconsider x = x as Element of the carrier of R 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__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_A_\/_{x}_&_b_in_A_\/_{x}_&_a_<>_b_holds_ (_not_a_<=_b_&_not_b_<=_a_) let a, b be Element of R; ::_thesis: ( a in A \/ {x} & b in A \/ {x} & a <> b implies ( not b1 <= b2 & not b2 <= b1 ) ) assume that A9: a in A \/ {x} and A10: b in A \/ {x} and A11: a <> b ; ::_thesis: ( not b1 <= b2 & not b2 <= b1 ) percases ( ( a in A & b in A ) or ( a in A & b in {x} ) or ( a in {x} & b in A ) or ( a in {x} & b in {x} ) ) by A9, A10, XBOOLE_0:def_3; suppose ( a in A & b in A ) ; ::_thesis: ( not b1 <= b2 & not b2 <= b1 ) hence ( not a <= b & not b <= a ) by A11, Def2; ::_thesis: verum end; supposeA12: ( a in A & b in {x} ) ; ::_thesis: ( not b1 <= b2 & not b2 <= b1 ) then b = x by TARSKI:def_1; hence ( not a <= b & not b <= a ) by A6, A7, A12, WAYBEL_0:def_15, WAYBEL_0:def_16; ::_thesis: verum end; supposeA13: ( a in {x} & b in A ) ; ::_thesis: ( not b1 <= b2 & not b2 <= b1 ) then a = x by TARSKI:def_1; hence ( not a <= b & not b <= a ) by A6, A7, A13, WAYBEL_0:def_15, WAYBEL_0:def_16; ::_thesis: verum end; suppose ( a in {x} & b in {x} ) ; ::_thesis: ( not b1 <= b2 & not b2 <= b1 ) then ( a = x & b = x ) by TARSKI:def_1; hence ( not a <= b & not b <= a ) by A11; ::_thesis: verum end; end; end; then A14: A \/ {x} is StableSet of R by A8, Def2, XBOOLE_1:8; card (A \/ {x}) = (card A) + 1 by A5, CARD_2:41; then card (A \/ {x}) > card A by NAT_1:13; hence contradiction by Def6, A1, A14; ::_thesis: verum end; hence (Upper A) \/ (Lower A) = [#] R by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th24: :: DILWORTH:24 for R being transitive RelStr for x being Element of R for S being Subset of R st x is_minimal_in Lower S holds x is_minimal_in [#] R proof let R be transitive RelStr ; ::_thesis: for x being Element of R for S being Subset of R st x is_minimal_in Lower S holds x is_minimal_in [#] R let x be Element of R; ::_thesis: for S being Subset of R st x is_minimal_in Lower S holds x is_minimal_in [#] R let S be Subset of R; ::_thesis: ( x is_minimal_in Lower S implies x is_minimal_in [#] R ) assume A1: x is_minimal_in Lower S ; ::_thesis: x is_minimal_in [#] R set cR = the carrier of R; A2: x in Lower S by A1, WAYBEL_4:56; assume not x is_minimal_in [#] R ; ::_thesis: contradiction then consider y being Element of R such that y in the carrier of R and A3: y < x by A2, WAYBEL_4:56; percases ( x in S or x in downarrow S ) by A2, XBOOLE_0:def_3; supposeA4: x in S ; ::_thesis: contradiction 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 contradiction by A1, A3, WAYBEL_4:56; ::_thesis: verum end; suppose x in downarrow S ; ::_thesis: contradiction 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; ::_thesis: verum end; end; end; theorem Th25: :: DILWORTH:25 for R being transitive RelStr for x being Element of R for S being Subset of R st x is_maximal_in Upper S holds x is_maximal_in [#] R proof let R be transitive RelStr ; ::_thesis: for x being Element of R for S being Subset of R st x is_maximal_in Upper S holds x is_maximal_in [#] R let x be Element of R; ::_thesis: for S being Subset of R st x is_maximal_in Upper S holds x is_maximal_in [#] R let S be Subset of R; ::_thesis: ( x is_maximal_in Upper S implies x is_maximal_in [#] R ) assume A1: x is_maximal_in Upper S ; ::_thesis: x is_maximal_in [#] R set cR = the carrier of R; A2: x in Upper S by A1, WAYBEL_4:55; assume not x is_maximal_in [#] R ; ::_thesis: contradiction then consider y being Element of R such that y in the carrier of R and A3: x < y by A2, WAYBEL_4:55; percases ( x in S or x in uparrow S ) by A2, XBOOLE_0:def_3; supposeA4: x in S ; ::_thesis: contradiction 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 contradiction by A1, A3, WAYBEL_4:55; ::_thesis: verum end; suppose x in uparrow S ; ::_thesis: contradiction 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; ::_thesis: verum end; end; end; definition let R be RelStr ; set cR = the carrier of R; func minimals R -> Subset of R means :Def9: :: DILWORTH:def 9 for x being Element of R holds ( x in it iff x is_minimal_in [#] R ) if not R is empty otherwise it = {} ; consistency for b1 being Subset of R holds verum ; existence ( ( not R is empty implies ex b1 being Subset of R st for x being Element of R holds ( x in b1 iff x is_minimal_in [#] R ) ) & ( R is empty implies ex b1 being Subset of R st b1 = {} ) ) proof defpred S1[ set ] means ex a being Element of R st ( a = $1 & a is_minimal_in the carrier of R ); consider X being set such that A1: for x being set holds ( x in X iff ( x in the carrier of R & S1[x] ) ) from XBOOLE_0:sch_1(); A2: now__::_thesis:_(_not_the_carrier_of_R_is_empty_implies_ex_X_being_Subset_of_R_st_ for_x_being_Element_of_R_holds_ (_x_in_X_iff_x_is_minimal_in_the_carrier_of_R_)_) assume A3: not the carrier of R is empty ; ::_thesis: ex X being Subset of R st for x being Element of R holds ( x in X iff x is_minimal_in the carrier of R ) for x being set st x in X holds x in the carrier of R by A1; then reconsider X = X as Subset of R by TARSKI:def_3; take X = X; ::_thesis: for x being Element of R holds ( x in X iff x is_minimal_in the carrier of R ) let x be Element of R; ::_thesis: ( x in X iff x is_minimal_in the carrier of R ) ( x in X implies S1[x] ) by A1; hence ( x in X iff x is_minimal_in the carrier of R ) by A1, A3; ::_thesis: verum end; now__::_thesis:_ex_X_being_Subset_of_R_st_X_=_{} reconsider X = {} as Subset of R by XBOOLE_1:2; take X = X; ::_thesis: X = {} thus X = {} ; ::_thesis: verum end; hence ( ( not R is empty implies ex b1 being Subset of R st for x being Element of R holds ( x in b1 iff x is_minimal_in [#] R ) ) & ( R is empty implies ex b1 being Subset of R st b1 = {} ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Subset of R holds ( ( not R is empty & ( for x being Element of R holds ( x in b1 iff x is_minimal_in [#] R ) ) & ( for x being Element of R holds ( x in b2 iff x is_minimal_in [#] R ) ) implies b1 = b2 ) & ( R is empty & b1 = {} & b2 = {} implies b1 = b2 ) ) proof let it1, it2 be Subset of R; ::_thesis: ( ( not R is empty & ( for x being Element of R holds ( x in it1 iff x is_minimal_in [#] R ) ) & ( for x being Element of R holds ( x in it2 iff x is_minimal_in [#] R ) ) implies it1 = it2 ) & ( R is empty & it1 = {} & it2 = {} implies it1 = it2 ) ) now__::_thesis:_(_not_R_is_empty_&_(_for_x_being_Element_of_R_holds_ (_x_in_it1_iff_x_is_minimal_in_the_carrier_of_R_)_)_&_(_for_x_being_Element_of_R_holds_ (_x_in_it2_iff_x_is_minimal_in_the_carrier_of_R_)_)_implies_it1_=_it2_) assume that not R is empty and A4: for x being Element of R holds ( x in it1 iff x is_minimal_in the carrier of R ) and A5: for x being Element of R holds ( x in it2 iff x is_minimal_in the carrier of R ) ; ::_thesis: it1 = it2 now__::_thesis:_for_x_being_set_holds_ (_x_in_it1_iff_x_in_it2_) let x be set ; ::_thesis: ( x in it1 iff x in it2 ) now__::_thesis:_(_(_x_in_it1_or_x_in_it2_)_implies_(_x_in_it1_&_x_in_it2_)_) assume A6: ( x in it1 or x in it2 ) ; ::_thesis: ( x in it1 & x in it2 ) then reconsider x9 = x as Element of R ; x9 is_minimal_in the carrier of R by A6, A4, A5; hence ( x in it1 & x in it2 ) by A4, A5; ::_thesis: verum end; hence ( x in it1 iff x in it2 ) ; ::_thesis: verum end; hence it1 = it2 by TARSKI:1; ::_thesis: verum end; hence ( ( not R is empty & ( for x being Element of R holds ( x in it1 iff x is_minimal_in [#] R ) ) & ( for x being Element of R holds ( x in it2 iff x is_minimal_in [#] R ) ) implies it1 = it2 ) & ( R is empty & it1 = {} & it2 = {} implies it1 = it2 ) ) ; ::_thesis: verum end; func maximals R -> Subset of R means :Def10: :: DILWORTH:def 10 for x being Element of R holds ( x in it iff x is_maximal_in [#] R ) if not R is empty otherwise it = {} ; consistency for b1 being Subset of R holds verum ; existence ( ( not R is empty implies ex b1 being Subset of R st for x being Element of R holds ( x in b1 iff x is_maximal_in [#] R ) ) & ( R is empty implies ex b1 being Subset of R st b1 = {} ) ) proof defpred S1[ set ] means ex a being Element of R st ( a = $1 & a is_maximal_in the carrier of R ); consider X being set such that A7: for x being set holds ( x in X iff ( x in the carrier of R & S1[x] ) ) from XBOOLE_0:sch_1(); A8: now__::_thesis:_(_not_the_carrier_of_R_is_empty_implies_ex_X_being_Subset_of_R_st_ for_x_being_Element_of_R_holds_ (_x_in_X_iff_x_is_maximal_in_the_carrier_of_R_)_) assume A9: not the carrier of R is empty ; ::_thesis: ex X being Subset of R st for x being Element of R holds ( x in X iff x is_maximal_in the carrier of R ) for x being set st x in X holds x in the carrier of R by A7; then reconsider X = X as Subset of R by TARSKI:def_3; take X = X; ::_thesis: for x being Element of R holds ( x in X iff x is_maximal_in the carrier of R ) let x be Element of R; ::_thesis: ( x in X iff x is_maximal_in the carrier of R ) ( x in X implies S1[x] ) by A7; hence ( x in X iff x is_maximal_in the carrier of R ) by A7, A9; ::_thesis: verum end; now__::_thesis:_ex_X_being_Subset_of_R_st_X_=_{} reconsider X = {} as Subset of R by XBOOLE_1:2; take X = X; ::_thesis: X = {} thus X = {} ; ::_thesis: verum end; hence ( ( not R is empty implies ex b1 being Subset of R st for x being Element of R holds ( x in b1 iff x is_maximal_in [#] R ) ) & ( R is empty implies ex b1 being Subset of R st b1 = {} ) ) by A8; ::_thesis: verum end; uniqueness for b1, b2 being Subset of R holds ( ( not R is empty & ( for x being Element of R holds ( x in b1 iff x is_maximal_in [#] R ) ) & ( for x being Element of R holds ( x in b2 iff x is_maximal_in [#] R ) ) implies b1 = b2 ) & ( R is empty & b1 = {} & b2 = {} implies b1 = b2 ) ) proof let it1, it2 be Subset of R; ::_thesis: ( ( not R is empty & ( for x being Element of R holds ( x in it1 iff x is_maximal_in [#] R ) ) & ( for x being Element of R holds ( x in it2 iff x is_maximal_in [#] R ) ) implies it1 = it2 ) & ( R is empty & it1 = {} & it2 = {} implies it1 = it2 ) ) now__::_thesis:_(_not_R_is_empty_&_(_for_x_being_Element_of_R_holds_ (_x_in_it1_iff_x_is_maximal_in_the_carrier_of_R_)_)_&_(_for_x_being_Element_of_R_holds_ (_x_in_it2_iff_x_is_maximal_in_the_carrier_of_R_)_)_implies_it1_=_it2_) assume that not R is empty and A10: for x being Element of R holds ( x in it1 iff x is_maximal_in the carrier of R ) and A11: for x being Element of R holds ( x in it2 iff x is_maximal_in the carrier of R ) ; ::_thesis: it1 = it2 now__::_thesis:_for_x_being_set_holds_ (_x_in_it1_iff_x_in_it2_) let x be set ; ::_thesis: ( x in it1 iff x in it2 ) now__::_thesis:_(_(_x_in_it1_or_x_in_it2_)_implies_(_x_in_it1_&_x_in_it2_)_) assume A12: ( x in it1 or x in it2 ) ; ::_thesis: ( x in it1 & x in it2 ) then reconsider x9 = x as Element of R ; x9 is_maximal_in the carrier of R by A12, A10, A11; hence ( x in it1 & x in it2 ) by A10, A11; ::_thesis: verum end; hence ( x in it1 iff x in it2 ) ; ::_thesis: verum end; hence it1 = it2 by TARSKI:1; ::_thesis: verum end; hence ( ( not R is empty & ( for x being Element of R holds ( x in it1 iff x is_maximal_in [#] R ) ) & ( for x being Element of R holds ( x in it2 iff x is_maximal_in [#] R ) ) implies it1 = it2 ) & ( R is empty & it1 = {} & it2 = {} implies it1 = it2 ) ) ; ::_thesis: verum end; end; :: deftheorem Def9 defines minimals DILWORTH:def_9_:_ for R being RelStr for b2 being Subset of R holds ( ( not R is empty implies ( b2 = minimals R iff for x being Element of R holds ( x in b2 iff x is_minimal_in [#] R ) ) ) & ( R is empty implies ( b2 = minimals R iff b2 = {} ) ) ); :: deftheorem Def10 defines maximals DILWORTH:def_10_:_ for R being RelStr for b2 being Subset of R holds ( ( not R is empty implies ( b2 = maximals R iff for x being Element of R holds ( x in b2 iff x is_maximal_in [#] R ) ) ) & ( R is empty implies ( b2 = maximals R iff b2 = {} ) ) ); registration let R be non empty transitive antisymmetric with_finite_clique# RelStr ; cluster maximals R -> non empty ; coherence not maximals R is empty proof set cP = the carrier of R; set 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, the InternalRel of R by BAGORDER:6; A3: y is_maximal_in CL by A2, WAYBEL_4:def_24; A4: the carrier of R = [#] R ; now__::_thesis:_y_is_maximal_in_the_carrier_of_R assume not y is_maximal_in the carrier of R ; ::_thesis: contradiction then consider z being Element of R such that z in the carrier of R and A5: y < z by WAYBEL_4:55; A6: y <= z by A5, ORDERS_2:def_6; set C = CL \/ {z}; reconsider C = CL \/ {z} 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; ::_thesis: verum end; hence not maximals R is empty by A4, Def10; ::_thesis: verum end; cluster minimals R -> non empty ; coherence not minimals R is empty proof set cP = the carrier of R; set 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, the InternalRel of R by BAGORDER:7; A9: y is_minimal_in CL by A8, WAYBEL_4:def_26; A10: the carrier of R = [#] R ; now__::_thesis:_y_is_minimal_in_the_carrier_of_R assume not y is_minimal_in the carrier of R ; ::_thesis: contradiction then consider z being Element of R such that z in the carrier of R and A11: z < y by WAYBEL_4:56; A12: z <= y by A11, ORDERS_2:def_6; set C = CL \/ {z}; reconsider C = CL \/ {z} 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; ::_thesis: verum end; hence not minimals R is empty by A10, Def9; ::_thesis: verum end; end; registration let R be RelStr ; cluster minimals R -> stable ; coherence minimals R is stable proof set mR = minimals R; let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in minimals R & y in minimals R & x <> y implies ( not x <= y & not y <= x ) ) assume that A1: x in minimals R and A2: y in minimals R and A3: x <> y ; ::_thesis: ( not x <= y & not y <= x ) A4: not R is 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; ::_thesis: not y <= x 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; ::_thesis: verum end; cluster maximals R -> stable ; coherence maximals R is stable proof set mR = maximals R; let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in maximals R & y in maximals R & x <> y implies ( not x <= y & not y <= x ) ) assume that A5: x in maximals R and A6: y in maximals R and A7: x <> y ; ::_thesis: ( not x <= y & not y <= x ) A8: not R is 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; ::_thesis: not y <= x 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; ::_thesis: verum end; end; theorem Th26: :: DILWORTH:26 for R being RelStr for A being StableSet of R st not minimals R c= A holds not minimals R c= Upper A proof let R be RelStr ; ::_thesis: for A being StableSet of R st not minimals R c= A holds not minimals R c= Upper A let A be StableSet of R; ::_thesis: ( not minimals R c= A implies not minimals R c= Upper A ) assume not minimals R c= A ; ::_thesis: not minimals R c= Upper 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 ; ::_thesis: contradiction reconsider x9 = x as Element of R by A1; not R is 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__::_thesis:_not_x99_<>_x9 assume x99 <> x9 ; ::_thesis: contradiction then x99 < x9 by A5, ORDERS_2:def_6; hence contradiction by A1, A4, WAYBEL_4:56; ::_thesis: verum end; hence contradiction by A6, A2; ::_thesis: verum end; theorem Th27: :: DILWORTH:27 for R being RelStr for A being StableSet of R st not maximals R c= A holds not maximals R c= Lower A proof let R be RelStr ; ::_thesis: for A being StableSet of R st not maximals R c= A holds not maximals R c= Lower A let A be StableSet of R; ::_thesis: ( not maximals R c= A implies not maximals R c= Lower A ) assume A1: not maximals R c= A ; ::_thesis: not maximals R c= Lower 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 ; ::_thesis: contradiction reconsider x9 = x as Element of R by A2; not R is 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__::_thesis:_not_x99_<>_x9 assume x99 <> x9 ; ::_thesis: contradiction then x9 < x99 by A6, ORDERS_2:def_6; hence contradiction by A2, A5, WAYBEL_4:55; ::_thesis: verum end; hence contradiction by A7, A3; ::_thesis: verum end; begin registration let R be RelStr ; let X be finite Subset of R; cluster subrelstr X -> finite ; coherence subrelstr X is finite by YELLOW_0:def_15; end; theorem Th28: :: DILWORTH:28 for R being RelStr for S being Subset of R for C being Clique of (subrelstr S) holds C is Clique of R proof let R be RelStr ; ::_thesis: for S being Subset of R for C being Clique of (subrelstr S) holds C is Clique of R let S be Subset of R; ::_thesis: for C being Clique of (subrelstr S) holds C is Clique of R let C be Clique of (subrelstr S); ::_thesis: C is Clique of R A1: the carrier of (subrelstr S) = S by YELLOW_0:def_15; now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_C_&_b_in_C_&_a_<>_b_&_not_a_<=_b_holds_ b_<=_a let a, b be Element of R; ::_thesis: ( a in C & b in C & a <> b & not a <= b implies b <= a ) assume that A2: a in C and A3: b in C and A4: a <> b ; ::_thesis: ( a <= b or b <= a ) 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; ::_thesis: verum end; hence C is Clique of R by A1, Th6, XBOOLE_1:1; ::_thesis: verum end; theorem Th29: :: DILWORTH:29 for R being RelStr for S being Subset of R for C being Clique of R holds C /\ S is Clique of (subrelstr S) proof let R be RelStr ; ::_thesis: for S being Subset of R for C being Clique of R holds C /\ S is Clique of (subrelstr S) let S be Subset of R; ::_thesis: for C being Clique of R holds C /\ S is Clique of (subrelstr S) let C be Clique of R; ::_thesis: C /\ S is Clique of (subrelstr S) set sS = subrelstr S; set CS = C /\ S; A1: C /\ S c= S by XBOOLE_1:17; A2: S = the carrier of (subrelstr S) by YELLOW_0:def_15; now__::_thesis:_for_a,_b_being_Element_of_(subrelstr_S)_holds_ (_not_a_in_C_/\_S_or_not_b_in_C_/\_S_or_not_a_<>_b_or_a_<=_b_or_b_<=_a_) let a, b be Element of (subrelstr S); ::_thesis: ( not a in C /\ S or not b in C /\ S or not a <> b or a <= b or b <= a ) assume A3: a in C /\ S ; ::_thesis: ( not b in C /\ S or not a <> b or a <= b or b <= a ) assume A4: b in C /\ S ; ::_thesis: ( not a <> b or a <= b or b <= a ) assume A5: a <> b ; ::_thesis: ( a <= b or b <= a ) A6: ( a in S & b in S ) by A3, A4, XBOOLE_0:def_4; A7: not S is empty by A3; not R is 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; ::_thesis: verum end; hence C /\ S is Clique of (subrelstr S) by Th6, A1, YELLOW_0:def_15; ::_thesis: verum end; theorem Th30: :: DILWORTH:30 for R being RelStr for S being Subset of R for A being StableSet of (subrelstr S) holds A is StableSet of R proof let R be RelStr ; ::_thesis: for S being Subset of R for A being StableSet of (subrelstr S) holds A is StableSet of R let S be Subset of R; ::_thesis: for A being StableSet of (subrelstr S) holds A is StableSet of R let A be StableSet of (subrelstr S); ::_thesis: A is StableSet of R set sS = subrelstr S; percases ( R is empty or not R is empty ) ; suppose R is empty ; ::_thesis: A is StableSet of R then the carrier of (subrelstr S) = {} by YELLOW_0:def_15; then A = {} R ; hence A is StableSet of R ; ::_thesis: verum end; supposeA1: not R is empty ; ::_thesis: A is StableSet of R percases ( S is empty or not S is empty ) ; suppose S is empty ; ::_thesis: A is StableSet of R then the carrier of (subrelstr S) = {} by YELLOW_0:def_15; then A = {} R ; hence A is StableSet of R ; ::_thesis: verum end; supposeA2: not S is empty ; ::_thesis: A is StableSet of R S = the carrier of (subrelstr S) by YELLOW_0:def_15; then reconsider A = A as Subset of R by XBOOLE_1:1; A is stable proof let x, y be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( x in A & y in A & x <> y implies ( not x <= y & not y <= x ) ) assume that A3: x in A and A4: y in A and A5: x <> y ; ::_thesis: ( not x <= y & not y <= x ) reconsider x9 = x, y9 = y as Element of (subrelstr S) 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; ::_thesis: verum end; hence A is StableSet of R ; ::_thesis: verum end; end; end; end; end; theorem Th31: :: DILWORTH:31 for R being RelStr for S being Subset of R for A being StableSet of R holds A /\ S is StableSet of (subrelstr S) proof let R be RelStr ; ::_thesis: for S being Subset of R for A being StableSet of R holds A /\ S is StableSet of (subrelstr S) let S be Subset of R; ::_thesis: for A being StableSet of R holds A /\ S is StableSet of (subrelstr S) let A be StableSet of R; ::_thesis: A /\ S is StableSet of (subrelstr S) set sS = subrelstr S; set AS = A /\ S; percases ( R is empty or not R is empty ) ; suppose R is empty ; ::_thesis: A /\ S is StableSet of (subrelstr S) then A /\ S = {} (subrelstr S) ; hence A /\ S is StableSet of (subrelstr S) ; ::_thesis: verum end; supposeA1: not R is empty ; ::_thesis: A /\ S is StableSet of (subrelstr S) percases ( S is empty or not S is empty ) ; suppose S is empty ; ::_thesis: A /\ S is StableSet of (subrelstr S) then A /\ S = {} (subrelstr S) ; hence A /\ S is StableSet of (subrelstr S) ; ::_thesis: verum end; supposeA2: not S is empty ; ::_thesis: A /\ S is StableSet of (subrelstr S) S = the carrier of (subrelstr S) by YELLOW_0:def_15; then reconsider AS = A /\ S as Subset of (subrelstr S) by XBOOLE_1:17; AS is stable proof let x, y be Element of (subrelstr S); :: according to DILWORTH:def_2 ::_thesis: ( x in AS & y in AS & x <> y implies ( not x <= y & not y <= x ) ) assume that A3: x in AS and A4: y in AS and A5: x <> y ; ::_thesis: ( not x <= y & not y <= x ) 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; ::_thesis: verum end; hence A /\ S is StableSet of (subrelstr S) ; ::_thesis: verum end; end; end; end; end; theorem Th32: :: DILWORTH:32 for R being RelStr for S being Subset of R for B being Subset of (subrelstr S) for x being Element of (subrelstr S) for y being Element of R st x = y & x is_maximal_in B holds y is_maximal_in B proof let R be RelStr ; ::_thesis: for S being Subset of R for B being Subset of (subrelstr S) for x being Element of (subrelstr S) for y being Element of R st x = y & x is_maximal_in B holds y is_maximal_in B let S be Subset of R; ::_thesis: for B being Subset of (subrelstr S) for x being Element of (subrelstr S) for y being Element of R st x = y & x is_maximal_in B holds y is_maximal_in B let B be Subset of (subrelstr S); ::_thesis: for x being Element of (subrelstr S) for y being Element of R st x = y & x is_maximal_in B holds y is_maximal_in B let x be Element of (subrelstr S); ::_thesis: for y being Element of R st x = y & x is_maximal_in B holds y is_maximal_in B let y be Element of R; ::_thesis: ( x = y & x is_maximal_in B implies y is_maximal_in B ) assume that A1: x = y and A2: x is_maximal_in B ; ::_thesis: y is_maximal_in B A3: x in B by A2, WAYBEL_4:55; assume not y is_maximal_in B ; ::_thesis: contradiction 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; ::_thesis: verum end; theorem Th33: :: DILWORTH:33 for R being RelStr for S being Subset of R for B being Subset of (subrelstr S) for x being Element of (subrelstr S) for y being Element of R st x = y & x is_minimal_in B holds y is_minimal_in B proof let R be RelStr ; ::_thesis: for S being Subset of R for B being Subset of (subrelstr S) for x being Element of (subrelstr S) for y being Element of R st x = y & x is_minimal_in B holds y is_minimal_in B let S be Subset of R; ::_thesis: for B being Subset of (subrelstr S) for x being Element of (subrelstr S) for y being Element of R st x = y & x is_minimal_in B holds y is_minimal_in B let B be Subset of (subrelstr S); ::_thesis: for x being Element of (subrelstr S) for y being Element of R st x = y & x is_minimal_in B holds y is_minimal_in B let x be Element of (subrelstr S); ::_thesis: for y being Element of R st x = y & x is_minimal_in B holds y is_minimal_in B let y be Element of R; ::_thesis: ( x = y & x is_minimal_in B implies y is_minimal_in B ) assume that A1: x = y and A2: x is_minimal_in B ; ::_thesis: y is_minimal_in B A3: x in B by A2, WAYBEL_4:56; assume not y is_minimal_in B ; ::_thesis: contradiction 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; ::_thesis: verum end; theorem Th34: :: DILWORTH:34 for R being transitive RelStr for A being StableSet of R for C being Clique of (subrelstr (Lower A)) for a, b being Element of R st a in A & a in C & b in C & not a = b holds b <= a proof let R be transitive RelStr ; ::_thesis: for A being StableSet of R for C being Clique of (subrelstr (Lower A)) for a, b being Element of R st a in A & a in C & b in C & not a = b holds b <= a let A be StableSet of R; ::_thesis: for C being Clique of (subrelstr (Lower A)) for a, b being Element of R st a in A & a in C & b in C & not a = b holds b <= a let C be Clique of (subrelstr (Lower A)); ::_thesis: for a, b being Element of R st a in A & a in C & b in C & not a = b holds b <= a let a, b be Element of R; ::_thesis: ( a in A & a in C & b in C & not a = b implies b <= a ) assume that A1: a in A and A2: a in C and A3: b in C ; ::_thesis: ( a = b or b <= a ) set ap = subrelstr (Lower A); reconsider a9 = a as Element of (subrelstr (Lower A)) by A2; A4: b in the carrier of (subrelstr (Lower A)) by A3; reconsider b9 = b as Element of (subrelstr (Lower A)) by A3; A5: b9 in Lower A by A4, YELLOW_0:def_15; A6: C is Clique of R by Th28; percases ( b9 in A or b9 in downarrow A ) by A5, XBOOLE_0:def_3; suppose b9 in A ; ::_thesis: ( a = b or b <= a ) hence ( a = b or b <= a ) by A1, A2, A3, A6, Th15; ::_thesis: verum end; suppose b9 in downarrow A ; ::_thesis: ( a = b or b <= a ) then consider c being Element of R such that A7: b <= c and A8: c in A by WAYBEL_0:def_15; percases ( a <> b or a = b ) ; supposeA9: a <> b ; ::_thesis: ( a = b or b <= a ) percases ( a9 <= b9 or b9 <= a9 ) by A9, A2, A3, Th6; suppose a9 <= b9 ; ::_thesis: ( a = b or b <= a ) then a <= b by YELLOW_0:59; then a <= c by A7, YELLOW_0:def_2; hence ( a = b or b <= a ) by A8, A7, A1, Def2; ::_thesis: verum end; suppose b9 <= a9 ; ::_thesis: ( a = b or b <= a ) hence ( a = b or b <= a ) by YELLOW_0:59; ::_thesis: verum end; end; end; suppose a = b ; ::_thesis: ( a = b or b <= a ) hence ( a = b or b <= a ) ; ::_thesis: verum end; end; end; end; end; theorem Th35: :: DILWORTH:35 for R being transitive RelStr for A being StableSet of R for C being Clique of (subrelstr (Upper A)) for a, b being Element of R st a in A & a in C & b in C & not a = b holds a <= b proof let R be transitive RelStr ; ::_thesis: for A being StableSet of R for C being Clique of (subrelstr (Upper A)) for a, b being Element of R st a in A & a in C & b in C & not a = b holds a <= b let A be StableSet of R; ::_thesis: for C being Clique of (subrelstr (Upper A)) for a, b being Element of R st a in A & a in C & b in C & not a = b holds a <= b let C be Clique of (subrelstr (Upper A)); ::_thesis: for a, b being Element of R st a in A & a in C & b in C & not a = b holds a <= b let a, b be Element of R; ::_thesis: ( a in A & a in C & b in C & not a = b implies a <= b ) assume that A1: a in A and A2: a in C and A3: b in C ; ::_thesis: ( a = b or a <= b ) set ap = subrelstr (Upper A); reconsider a9 = a as Element of (subrelstr (Upper A)) by A2; A4: b in the carrier of (subrelstr (Upper A)) by A3; reconsider b9 = b as Element of (subrelstr (Upper A)) by A3; A5: b9 in Upper A by A4, YELLOW_0:def_15; A6: C is Clique of R by Th28; percases ( b9 in A or b9 in uparrow A ) by A5, XBOOLE_0:def_3; suppose b9 in A ; ::_thesis: ( a = b or a <= b ) hence ( a = b or a <= b ) by A1, A2, A3, A6, Th15; ::_thesis: verum end; suppose b9 in uparrow A ; ::_thesis: ( a = b or a <= b ) then consider c being Element of R such that A7: c <= b and A8: c in A by WAYBEL_0:def_16; percases ( a <> b or a = b ) ; supposeA9: a <> b ; ::_thesis: ( a = b or a <= b ) percases ( a9 <= b9 or b9 <= a9 ) by A9, A2, A3, Th6; suppose a9 <= b9 ; ::_thesis: ( a = b or a <= b ) hence ( a = b or a <= b ) by YELLOW_0:59; ::_thesis: verum end; suppose b9 <= a9 ; ::_thesis: ( a = b or a <= b ) then b <= a by YELLOW_0:59; then c <= a by A7, YELLOW_0:def_2; hence ( a = b or a <= b ) by A8, A7, A1, Def2; ::_thesis: verum end; end; end; suppose a = b ; ::_thesis: ( a = b or a <= b ) hence ( a = b or a <= b ) ; ::_thesis: verum end; end; end; end; end; registration let R be with_finite_clique# RelStr ; let S be Subset of R; cluster subrelstr S -> with_finite_clique# ; coherence subrelstr S is with_finite_clique# proof 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 S1[ Nat] means ex c being finite Clique of (subrelstr S) st card c = R; A2: for k being Nat st S1[k] holds k <= card C proof let k be Nat; ::_thesis: ( S1[k] implies k <= card C ) assume S1[k] ; ::_thesis: k <= card C then consider c being finite Clique of (subrelstr S) such that A3: card c = k ; c is finite Clique of R by Th28; hence k <= card C by A3, A1; ::_thesis: verum end; card ({} (subrelstr S)) = 0 ; then A4: ex k being Nat st S1[k] ; consider k being Nat such that A5: S1[k] and A6: for n being Nat st S1[n] holds n <= k from NAT_1:sch_6(A2, A4); consider c being finite Clique of (subrelstr S) such that A7: card c = k by A5; for D being finite Clique of (subrelstr S) holds card D <= card c by A7, A6; hence subrelstr S is with_finite_clique# by Def3; ::_thesis: verum end; end; registration let R be with_finite_stability# RelStr ; let S be Subset of R; cluster subrelstr S -> with_finite_stability# ; coherence subrelstr S is with_finite_stability# proof 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# ; ::_thesis: contradiction defpred S1[ Nat] means ex C being finite StableSet of (subrelstr S) st ( card C = R & ex B being finite StableSet of (subrelstr S) st R < card B ); A3: S1[ 0 ] proof reconsider C = {} (subrelstr S) as finite StableSet of (subrelstr S) ; take C ; ::_thesis: ( card C = 0 & ex B being finite StableSet of (subrelstr S) st 0 < card B ) thus card C = 0 ; ::_thesis: ex B being finite StableSet of (subrelstr S) st 0 < card B hence ex B being finite StableSet of (subrelstr S) st 0 < card B by A2, Def5; ::_thesis: verum end; A4: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) 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 ; ::_thesis: S1[n + 1] 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 ; ::_thesis: ( card BB = n + 1 & ex B being finite StableSet of (subrelstr S) st n + 1 < card B ) thus card BB = n + 1 by A7; ::_thesis: ex B being finite StableSet of (subrelstr S) st n + 1 < card B consider Bb being finite StableSet of (subrelstr S) such that A8: card BB < card Bb by A2, Def5; take Bb ; ::_thesis: n + 1 < card Bb thus n + 1 < card Bb by A8, A7; ::_thesis: verum end; for n being Nat holds S1[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; ::_thesis: verum end; end; theorem Th36: :: DILWORTH:36 for R being non empty transitive antisymmetric with_finite_clique# RelStr for x being Element of R ex y being Element of R st ( y is_minimal_in [#] R & ( y = x or y < x ) ) proof let R be non empty transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: for x being Element of R ex y being Element of R st ( y is_minimal_in [#] R & ( y = x or y < x ) ) let x be Element of R; ::_thesis: ex y being Element of R st ( y is_minimal_in [#] R & ( y = x or y < x ) ) set sx = Lower {x}; set sL = subrelstr (Lower {x}); reconsider sL = subrelstr (Lower {x}) as non empty transitive antisymmetric with_finite_clique# RelStr ; consider y being set such that A1: y in minimals sL by XBOOLE_0:def_1; reconsider y = y as Element of sL by A1; A2: [#] sL = Lower {x} by YELLOW_0:def_15; then A3: y is_minimal_in Lower {x} by A1, Def9; reconsider y9 = y as Element of R by YELLOW_0:58; take y9 ; ::_thesis: ( y9 is_minimal_in [#] R & ( y9 = x or y9 < x ) ) Lower {x} c= the carrier of sL by YELLOW_0:def_15; hence y9 is_minimal_in [#] R by A3, Th33, Th24; ::_thesis: ( y9 = x or y9 < x ) percases ( y9 = x or y9 <> x ) ; suppose y9 = x ; ::_thesis: ( y9 = x or y9 < x ) hence ( y9 = x or y9 < x ) ; ::_thesis: verum end; suppose y9 <> x ; ::_thesis: ( y9 = x or 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 ( y9 = x or y9 < x ) by ORDERS_2:def_6; ::_thesis: verum end; end; end; theorem :: DILWORTH:37 for R being transitive antisymmetric with_finite_clique# RelStr holds Upper (minimals R) = [#] R proof let R be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: Upper (minimals R) = [#] R set ap = Upper (minimals R); set cR = the carrier of R; the carrier of R c= Upper (minimals R) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R or x in Upper (minimals R) ) assume A1: x in the carrier of R ; ::_thesis: x in Upper (minimals R) then reconsider x9 = x as Element of R ; A2: not R is 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; percases ( x9 = y or y < x9 ) by A4; suppose x9 = y ; ::_thesis: x in Upper (minimals R) hence x in Upper (minimals R) by A5, XBOOLE_0:def_3; ::_thesis: verum end; suppose y < x9 ; ::_thesis: x in Upper (minimals R) then y <= x9 by ORDERS_2:def_6; then x in uparrow (minimals R) by A5, WAYBEL_0:def_16; hence x in Upper (minimals R) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence Upper (minimals R) = [#] R by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th38: :: DILWORTH:38 for R being non empty transitive antisymmetric with_finite_clique# RelStr for x being Element of R ex y being Element of R st ( y is_maximal_in [#] R & ( y = x or x < y ) ) proof let R be non empty transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: for x being Element of R ex y being Element of R st ( y is_maximal_in [#] R & ( y = x or x < y ) ) let x be Element of R; ::_thesis: ex y being Element of R st ( y is_maximal_in [#] R & ( y = x or x < y ) ) set ax = Upper {x}; set sU = subrelstr (Upper {x}); reconsider sU = subrelstr (Upper {x}) as non empty transitive antisymmetric with_finite_clique# RelStr ; consider y being set such that A1: y in maximals sU by XBOOLE_0:def_1; reconsider y = y as Element of sU by A1; A2: [#] sU = Upper {x} by YELLOW_0:def_15; then A3: y is_maximal_in Upper {x} by A1, Def10; reconsider y9 = y as Element of R by YELLOW_0:58; take y9 ; ::_thesis: ( y9 is_maximal_in [#] R & ( y9 = x or x < y9 ) ) Upper {x} c= the carrier of sU by YELLOW_0:def_15; hence y9 is_maximal_in [#] R by A3, Th32, Th25; ::_thesis: ( y9 = x or x < y9 ) percases ( y9 = x or y9 <> x ) ; suppose y9 = x ; ::_thesis: ( y9 = x or x < y9 ) hence ( y9 = x or x < y9 ) ; ::_thesis: verum end; suppose y9 <> x ; ::_thesis: ( y9 = x or x < y9 ) 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 ( y9 = x or x < y9 ) by ORDERS_2:def_6; ::_thesis: verum end; end; end; theorem :: DILWORTH:39 for R being transitive antisymmetric with_finite_clique# RelStr holds Lower (maximals R) = [#] R proof let P be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: Lower (maximals P) = [#] P set ap = Lower (maximals P); set cP = the carrier of P; the carrier of P c= Lower (maximals P) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of P or x in Lower (maximals P) ) assume A1: x in the carrier of P ; ::_thesis: x in Lower (maximals P) then reconsider x9 = x as Element of P ; A2: not P is 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; percases ( x9 = y or y > x9 ) by A4; suppose x9 = y ; ::_thesis: x in Lower (maximals P) hence x in Lower (maximals P) by A5, XBOOLE_0:def_3; ::_thesis: verum end; suppose y > x9 ; ::_thesis: x in Lower (maximals P) then x9 <= y by ORDERS_2:def_6; then x in downarrow (maximals P) by A5, WAYBEL_0:def_15; hence x in Lower (maximals P) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence Lower (maximals P) = [#] P by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th40: :: DILWORTH:40 for R being transitive antisymmetric with_finite_clique# RelStr for A being StableSet of R st minimals R c= A holds A = minimals R proof let R be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: for A being StableSet of R st minimals R c= A holds A = minimals R let A be StableSet of R; ::_thesis: ( minimals R c= A implies A = minimals R ) assume A1: minimals R c= A ; ::_thesis: A = minimals R A c= minimals R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in minimals R ) assume A2: x in A ; ::_thesis: x in minimals R then A3: not R is 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; ::_thesis: verum end; hence A = minimals R by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th41: :: DILWORTH:41 for R being transitive antisymmetric with_finite_clique# RelStr for A being StableSet of R st maximals R c= A holds A = maximals R proof let R be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: for A being StableSet of R st maximals R c= A holds A = maximals R let A be StableSet of R; ::_thesis: ( maximals R c= A implies A = maximals R ) assume A1: maximals R c= A ; ::_thesis: A = maximals R A c= maximals R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in maximals R ) assume A2: x in A ; ::_thesis: x in maximals R then A3: not R is 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; ::_thesis: verum end; hence A = maximals R by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th42: :: DILWORTH:42 for R being with_finite_clique# RelStr for S being Subset of R holds clique# (subrelstr S) <= clique# R proof let R be with_finite_clique# RelStr ; ::_thesis: for S being Subset of R holds clique# (subrelstr S) <= clique# R let S be Subset of R; ::_thesis: clique# (subrelstr S) <= clique# R set s = subrelstr S; consider c being finite Clique of (subrelstr S) such that A1: card c = clique# (subrelstr S) by Def4; c is Clique of R by Th28; hence clique# (subrelstr S) <= clique# R by Def4, A1; ::_thesis: verum end; theorem :: DILWORTH:43 for R being with_finite_clique# RelStr for C being Clique of R for S being Subset of R st card C = clique# R & C c= S holds clique# (subrelstr S) = clique# R proof let R be with_finite_clique# RelStr ; ::_thesis: for C being Clique of R for S being Subset of R st card C = clique# R & C c= S holds clique# (subrelstr S) = clique# R let C be Clique of R; ::_thesis: for S being Subset of R st card C = clique# R & C c= S holds clique# (subrelstr S) = clique# R let S be Subset of R; ::_thesis: ( card C = clique# R & C c= S implies clique# (subrelstr S) = clique# R ) assume that A1: card C = clique# R and A2: C c= S ; ::_thesis: clique# (subrelstr S) = clique# R 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; ::_thesis: verum end; theorem Th44: :: DILWORTH:44 for R being with_finite_stability# RelStr for S being Subset of R holds stability# (subrelstr S) <= stability# R proof let R be with_finite_stability# RelStr ; ::_thesis: for S being Subset of R holds stability# (subrelstr S) <= stability# R let S be Subset of R; ::_thesis: stability# (subrelstr S) <= stability# 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; ::_thesis: verum end; theorem Th45: :: DILWORTH:45 for R being with_finite_stability# RelStr for A being StableSet of R for S being Subset of R st card A = stability# R & A c= S holds stability# (subrelstr S) = stability# R proof let R be with_finite_stability# RelStr ; ::_thesis: for A being StableSet of R for S being Subset of R st card A = stability# R & A c= S holds stability# (subrelstr S) = stability# R let A be StableSet of R; ::_thesis: for S being Subset of R st card A = stability# R & A c= S holds stability# (subrelstr S) = stability# R let S be Subset of R; ::_thesis: ( card A = stability# R & A c= S implies stability# (subrelstr S) = stability# R ) assume that A1: card A = stability# R and A2: A c= S ; ::_thesis: stability# (subrelstr S) = stability# R 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; ::_thesis: verum end; begin definition let R be RelStr ; let P be a_partition of the carrier of R; attrP is Clique-wise means :Def11: :: DILWORTH:def 11 for x being set st x in P holds x is Clique of R; end; :: deftheorem Def11 defines Clique-wise DILWORTH:def_11_:_ for R being RelStr for P being a_partition of the carrier of R holds ( P is Clique-wise iff for x being set st x in P holds x is Clique of R ); registration let R be RelStr ; cluster with_non-empty_elements Clique-wise for a_partition of the carrier of R; existence ex b1 being a_partition of the carrier of R st b1 is Clique-wise proof set cR = the carrier of R; percases ( R is empty or not R is empty ) ; suppose R is empty ; ::_thesis: ex b1 being a_partition of the carrier of R st b1 is Clique-wise then reconsider S = {} as a_partition of the carrier of R by EQREL_1:45; take S ; ::_thesis: S is Clique-wise thus for x being set st x in S holds x is Clique of R ; :: according to DILWORTH:def_11 ::_thesis: verum end; supposeA1: not R is empty ; ::_thesis: ex b1 being a_partition of the carrier of R st b1 is Clique-wise take S = SmallestPartition the carrier of R; ::_thesis: S is Clique-wise let z be set ; :: according to DILWORTH:def_11 ::_thesis: ( z in S implies z is Clique of R ) assume A2: z in S ; ::_thesis: z is Clique of R S = { {x} where x is Element of the carrier of R : verum } by A1, EQREL_1:37; then consider x being Element of the carrier of R such that A3: z = {x} and verum by A2; thus z is Clique of R by A3, A1, SUBSET_1:33; ::_thesis: verum end; 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 for b1 being a_partition of the carrier of R st b1 is empty holds b1 is Clique-wise proof let P be a_partition of the carrier of R; ::_thesis: ( P is empty implies P is Clique-wise ) assume P is empty ; ::_thesis: P is Clique-wise let x be set ; :: according to DILWORTH:def_11 ::_thesis: ( x in P implies x is Clique of R ) thus ( x in P implies x is Clique of R ) ; ::_thesis: verum end; end; theorem Th46: :: DILWORTH:46 for R being finite RelStr for C being Clique-partition of R holds card C >= stability# R proof let R be finite RelStr ; ::_thesis: for C being Clique-partition of R holds card C >= stability# R let C be Clique-partition of R; ::_thesis: card C >= stability# R assume A1: card C < stability# R ; ::_thesis: contradiction 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; percases ( R is empty or not R is empty ) ; suppose R is empty ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; supposeA4: not R is empty ; ::_thesis: contradiction defpred S1[ set , set ] means ( $1 in A & $2 in C & $1 in $2 ); A5: for x being set st x in A holds ex y being set st ( y in C & S1[x,y] ) proof let x be set ; ::_thesis: ( x in A implies ex y being set st ( y in C & S1[x,y] ) ) assume A6: x in A ; ::_thesis: ex y being set st ( y in C & S1[x,y] ) reconsider x9 = x as Element of R by A6; not the carrier of R is empty by A4; then x9 in the carrier of R ; 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 ; ::_thesis: ( y in C & S1[x,y] ) thus ( y in C & S1[x,y] ) by A6, A7, A8; ::_thesis: verum end; consider f being Function of A,C such that A9: for x being set st x in A holds S1[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; ::_thesis: verum end; end; end; theorem Th47: :: DILWORTH:47 for R being with_finite_stability# RelStr for A being StableSet of R for C being Clique-partition of R st card C = card A holds ex f being Function of A,C st ( f is bijective & ( for x being set st x in A holds x in f . x ) ) proof let R be with_finite_stability# RelStr ; ::_thesis: for A being StableSet of R for C being Clique-partition of R st card C = card A holds ex f being Function of A,C st ( f is bijective & ( for x being set st x in A holds x in f . x ) ) let A be StableSet of R; ::_thesis: for C being Clique-partition of R st card C = card A holds ex f being Function of A,C st ( f is bijective & ( for x being set st x in A holds x in f . x ) ) let C be Clique-partition of R; ::_thesis: ( card C = card A implies ex f being Function of A,C st ( f is bijective & ( for x being set st x in A holds x in f . x ) ) ) assume A1: card C = card A ; ::_thesis: ex f being Function of A,C st ( f is bijective & ( for x being set st x in A holds x in f . x ) ) set cR = the carrier of R; percases ( R is empty or not R is empty ) ; supposeA2: R is empty ; ::_thesis: ex f being Function of A,C st ( f is bijective & ( for x being set st x in A holds x in f . x ) ) then the carrier of R is empty ; then A3: C = {} by EQREL_1:32; set f = the Function of A,C; dom the Function of A,C = {} 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 ; ::_thesis: ( f is bijective & ( for x being set st x in A holds x in f . x ) ) thus f is bijective by A4; ::_thesis: for x being set st x in A holds x in f . x thus for x being set st x in A holds x in f . x ; ::_thesis: verum end; supposeA5: not R is empty ; ::_thesis: ex f being Function of A,C st ( f is bijective & ( for x being set st x in A holds x in f . x ) ) defpred S1[ set , set ] means ( $1 in A & $2 in C & $1 in $2 ); A6: for x being set st x in A holds ex y being set st ( y in C & S1[x,y] ) proof let x be set ; ::_thesis: ( x in A implies ex y being set st ( y in C & S1[x,y] ) ) assume A7: x in A ; ::_thesis: ex y being set st ( y in C & S1[x,y] ) then reconsider x9 = x as Element of R ; not the carrier of R is empty by A5; then x9 in the carrier of R ; 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 ; ::_thesis: ( y in C & S1[x,y] ) thus ( y in C & S1[x,y] ) by A7, A8, A9; ::_thesis: verum end; consider f being Function of A,C such that A10: for x being set st x in A holds S1[x,f . x] from FUNCT_2:sch_1(A6); take f ; ::_thesis: ( f is bijective & ( for x being set st x in A holds x in f . x ) ) A11: f is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 ) assume that A12: x1 in dom f and A13: x2 in dom f and A14: f . x1 = f . x2 ; ::_thesis: x1 = 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; ::_thesis: verum 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; ::_thesis: for x being set st x in A holds x in f . x let x be set ; ::_thesis: ( x in A implies x in f . x ) assume x in A ; ::_thesis: x in f . x hence x in f . x by A10; ::_thesis: verum end; end; end; theorem Th48: :: DILWORTH:48 for R being finite RelStr for A being StableSet of R for C being Clique-partition of R st card C = card A holds for c being set st c in C holds ex a being Element of A st c /\ A = {a} proof let R be finite RelStr ; ::_thesis: for A being StableSet of R for C being Clique-partition of R st card C = card A holds for c being set st c in C holds ex a being Element of A st c /\ A = {a} let A be StableSet of R; ::_thesis: for C being Clique-partition of R st card C = card A holds for c being set st c in C holds ex a being Element of A st c /\ A = {a} let C be Clique-partition of R; ::_thesis: ( card C = card A implies for c being set st c in C holds ex a being Element of A st c /\ A = {a} ) assume A1: card C = card A ; ::_thesis: for c being set st c in C holds ex a being Element of A st c /\ A = {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 ; ::_thesis: ( c in C implies ex a being Element of A st c /\ A = {a} ) assume A4: c in C ; ::_thesis: ex a being Element of A st c /\ A = {a} 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 ; ::_thesis: c /\ A = {a} now__::_thesis:_for_z_being_set_holds_ (_(_z_in_c_/\_A_implies_z_=_a_)_&_(_z_=_a_implies_z_in_c_/\_A_)_) let z be set ; ::_thesis: ( ( z in c /\ A implies z = a ) & ( z = a implies z in c /\ A ) ) hereby ::_thesis: ( z = a implies z in c /\ A ) assume z in c /\ A ; ::_thesis: z = 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; ::_thesis: verum end; assume z = a ; ::_thesis: z in c /\ A hence z in c /\ A by A7, A5, XBOOLE_0:def_4; ::_thesis: verum end; hence c /\ A = {a} by TARSKI:def_1; ::_thesis: verum end; theorem Th49: :: DILWORTH:49 for R being non empty transitive antisymmetric with_finite_stability# RelStr for A being StableSet of R for U being Clique-partition of (subrelstr (Upper A)) for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds ex C being Clique-partition of R st card C = stability# R proof let R be non empty transitive antisymmetric with_finite_stability# RelStr ; ::_thesis: for A being StableSet of R for U being Clique-partition of (subrelstr (Upper A)) for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds ex C being Clique-partition of R st card C = stability# R let A be StableSet of R; ::_thesis: for U being Clique-partition of (subrelstr (Upper A)) for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds ex C being Clique-partition of R st card C = stability# R let U be Clique-partition of (subrelstr (Upper A)); ::_thesis: for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds ex C being Clique-partition of R st card C = stability# R let L be Clique-partition of (subrelstr (Lower A)); ::_thesis: ( card A = stability# R & card U = stability# R & card L = stability# R implies ex C being Clique-partition of R st card C = stability# R ) assume that A1: card A = stability# R and A2: card U = stability# R and A3: card L = stability# R ; ::_thesis: ex C being Clique-partition of R st card C = stability# R A4: not A is empty by A1; set aA = Upper A; set bA = Lower A; set cR = the carrier of R; set Pa = subrelstr (Upper A); set Pb = subrelstr (Lower A); A5: Upper A = the carrier of (subrelstr (Upper A)) by YELLOW_0:def_15; A6: Lower A = the carrier of (subrelstr (Lower A)) by YELLOW_0:def_15; reconsider Pa = subrelstr (Upper A) as non empty transitive antisymmetric with_finite_stability# 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 non empty transitive antisymmetric with_finite_stability# 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 (f .\/ g); A15: dom (f .\/ g) = (dom f) \/ (dom g) by LEXBFS:def_2; A16: rng (f .\/ g) c= bool the carrier of R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f .\/ g) or x in bool the carrier of R ) assume x in rng (f .\/ g) ; ::_thesis: x in bool the carrier of R then consider a being set such that A17: a in dom (f .\/ g) and A18: (f .\/ g) . a = x by FUNCT_1:def_3; A19: (f .\/ g) . 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= the carrier of R by A5, XBOOLE_1:1; g . a in L by A17, A15, FUNCT_2:5; then g . a c= the carrier of R by A6, XBOOLE_1:1; then x c= the carrier of R by A18, A19, A20, XBOOLE_1:8; hence x in bool the carrier of R ; ::_thesis: verum end; A21: union (rng (f .\/ g)) = the carrier of R proof now__::_thesis:_for_x_being_set_holds_ (_(_x_in_union_(rng_(f_.\/_g))_implies_x_in_the_carrier_of_R_)_&_(_x_in_[#]_R_implies_x_in_union_(rng_(f_.\/_g))_)_) let x be set ; ::_thesis: ( ( x in union (rng (f .\/ g)) implies x in the carrier of R ) & ( x in [#] R implies b1 in union (rng (f .\/ g)) ) ) hereby ::_thesis: ( x in [#] R implies b1 in union (rng (f .\/ g)) ) assume x in union (rng (f .\/ g)) ; ::_thesis: x in the carrier of R then consider Y being set such that A22: x in Y and A23: Y in rng (f .\/ g) by TARSKI:def_4; consider a being set such that A24: a in dom (f .\/ g) and A25: Y = (f .\/ g) . a by A23, FUNCT_1:def_3; A26: x in (f . a) \/ (g . a) by A24, A25, A22, A15, LEXBFS:def_2; percases ( x in f . a or x in g . a ) by A26, XBOOLE_0:def_3; supposeA27: x in f . a ; ::_thesis: x in the carrier of R f . a in U by A24, A15, FUNCT_2:5; then x in Upper A by A27, A5; hence x in the carrier of R ; ::_thesis: verum end; supposeA28: x in g . a ; ::_thesis: x in the carrier of R g . a in L by A24, A15, FUNCT_2:5; then x in Lower A by A28, A6; hence x in the carrier of R ; ::_thesis: verum end; end; end; assume x in [#] R ; ::_thesis: b1 in union (rng (f .\/ g)) then A29: x in (Upper A) \/ (Lower A) by A1, Th23; percases ( x in Upper A or x in Lower A ) by A29, XBOOLE_0:def_3; suppose x in Upper A ; ::_thesis: b1 in union (rng (f .\/ g)) 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: (f .\/ g) . a in rng (f .\/ g) by A32, A15, A9, A13, FUNCT_1:3; (f .\/ g) . a = (f . a) \/ (g . a) by A32, A15, A9, A13, LEXBFS:def_2; then x in (f .\/ g) . a by A30, A33, XBOOLE_0:def_3; hence x in union (rng (f .\/ g)) by A34, TARSKI:def_4; ::_thesis: verum end; suppose x in Lower A ; ::_thesis: b1 in union (rng (f .\/ g)) 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: (f .\/ g) . a in rng (f .\/ g) by A37, A15, A9, A13, FUNCT_1:3; (f .\/ g) . a = (f . a) \/ (g . a) by A37, A15, A9, A13, LEXBFS:def_2; then x in (f .\/ g) . a by A35, A38, XBOOLE_0:def_3; hence x in union (rng (f .\/ g)) by A39, TARSKI:def_4; ::_thesis: verum end; end; end; hence union (rng (f .\/ g)) = the carrier of R by TARSKI:1; ::_thesis: verum end; A40: now__::_thesis:_for_a_being_Subset_of_the_carrier_of_R_st_a_in_rng_(f_.\/_g)_holds_ (_a_<>_{}_&_(_for_b_being_Subset_of_the_carrier_of_R_st_b_in_rng_(f_.\/_g)_&_a_<>_b_holds_ not_a_meets_b_)_) let a be Subset of the carrier of R; ::_thesis: ( a in rng (f .\/ g) implies ( a <> {} & ( for b being Subset of the carrier of R st b in rng (f .\/ g) & a <> b holds not a meets b ) ) ) assume a in rng (f .\/ g) ; ::_thesis: ( a <> {} & ( for b being Subset of the carrier of R st b in rng (f .\/ g) & a <> b holds not a meets b ) ) then consider x being set such that A41: x in dom (f .\/ g) and A42: (f .\/ g) . x = a by FUNCT_1:def_3; A43: (f .\/ g) . x = (f . x) \/ (g . x) by A41, A15, LEXBFS:def_2; set cfx = f . x; set cgx = g . x; A44: f . x in U by A41, A15, FUNCT_2:5; then reconsider cfx = f . x as Subset of Pa ; A45: g . x in L by A41, A15, FUNCT_2:5; then reconsider cgx = g . x as Subset of Pb ; cfx <> {} by A44, EQREL_1:def_4; hence a <> {} by A42, A43; ::_thesis: for b being Subset of the carrier of R st b in rng (f .\/ g) & a <> b holds not a meets b let b be Subset of the carrier of R; ::_thesis: ( b in rng (f .\/ g) & a <> b implies not a meets b ) assume b in rng (f .\/ g) ; ::_thesis: ( a <> b implies not a meets b ) then consider y being set such that A46: y in dom (f .\/ g) and A47: (f .\/ g) . y = b by FUNCT_1:def_3; A48: (f .\/ g) . y = (f . y) \/ (g . y) by A46, A15, LEXBFS:def_2; set cfy = f . y; set cgy = g . y; A49: f . y in U by A46, A15, FUNCT_2:5; then reconsider cfy = f . y as Subset of Pa ; A50: g . y in L by A46, A15, FUNCT_2:5; then reconsider cgy = g . y as Subset of Pb ; assume A51: a <> b ; ::_thesis: not a meets 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 ; ::_thesis: contradiction 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; set cgz = g . z; percases ( ( z in cfx & z in cfy ) or ( z in cfx & z in cgy ) or ( z in cgx & z in cfy ) or ( z in cgx & z in cgy ) ) by A55, A56, A42, A47, A43, A48, XBOOLE_0:def_3; suppose ( z in cfx & z in cfy ) ; ::_thesis: contradiction 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; ::_thesis: verum end; supposeA57: ( z in cfx & z in cgy ) ; ::_thesis: contradiction then A58: z in A by A5, A6, Th22; A59: z in f . z by A57, A5, A6, Th22, A8; A60: f . z in U by A57, A5, A6, Th22, FUNCT_2:5; then reconsider cfz = f . z 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: g . z in L by A57, A5, A6, Th22, FUNCT_2:5; then reconsider cgz = g . z 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; ::_thesis: verum end; supposeA64: ( z in cgx & z in cfy ) ; ::_thesis: contradiction then A65: z in A by A5, A6, Th22; A66: z in f . z by A64, A5, A6, Th22, A8; A67: f . z in U by A64, A5, A6, Th22, FUNCT_2:5; then reconsider cfz = f . z 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: g . z in L by A64, A5, A6, Th22, FUNCT_2:5; then reconsider cgz = g . z 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; ::_thesis: verum end; suppose ( z in cgx & z in cgy ) ; ::_thesis: contradiction 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; ::_thesis: verum end; end; end; A71: for x being set st x in rng (f .\/ g) holds x is Clique of R proof let c be set ; ::_thesis: ( c in rng (f .\/ g) implies c is Clique of R ) assume c in rng (f .\/ g) ; ::_thesis: c is Clique of R then consider x being set such that A72: x in dom (f .\/ g) and A73: c = (f .\/ g) . x by FUNCT_1:def_3; A74: c = (f . x) \/ (g . x) by A72, A73, A15, LEXBFS:def_2; set cf = f . x; set cg = g . x; f . x in U by A72, A15, FUNCT_2:5; then A75: f . x is Clique of Pa by Def11; then A76: f . x is Clique of R by Th28; g . x in L by A72, A15, FUNCT_2:5; then A77: g . x is Clique of Pb by Def11; then A78: g . x is Clique of R by Th28; then reconsider c9 = c as Subset of R by A74, A76, XBOOLE_1:8; now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_c9_&_b_in_c9_&_a_<>_b_&_not_a_<=_b_holds_ b_<=_a let a, b be Element of R; ::_thesis: ( a in c9 & b in c9 & a <> b & not b1 <= b2 implies b2 <= b1 ) assume that A79: a in c9 and A80: b in c9 and A81: a <> b ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) A82: x in f . x by A72, A15, A8; A83: x in g . x by A72, A15, A12; reconsider x = x as Element of R by A72, A15, A9, A13; percases ( ( a in f . x & b in f . x ) or ( a in f . x & b in g . x ) or ( a in g . x & b in f . x ) or ( a in g . x & b in g . x ) ) by A79, A80, A74, XBOOLE_0:def_3; suppose ( a in f . x & b in f . x ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) hence ( a <= b or b <= a ) by A76, A81, Th6; ::_thesis: verum end; supposeA84: ( a in f . x & b in g . x ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) 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; ::_thesis: verum end; supposeA86: ( a in g . x & b in f . x ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) 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; ::_thesis: verum end; suppose ( a in g . x & b in g . x ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) hence ( a <= b or b <= a ) by A78, A81, Th6; ::_thesis: verum end; end; end; hence c is Clique of R by Th6; ::_thesis: verum end; A88: f .\/ g is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (f .\/ g) or not x2 in dom (f .\/ g) or not (f .\/ g) . x1 = (f .\/ g) . x2 or x1 = x2 ) assume that A89: x1 in dom (f .\/ g) and A90: x2 in dom (f .\/ g) and A91: (f .\/ g) . x1 = (f .\/ g) . x2 ; ::_thesis: x1 = x2 A92: (f .\/ g) . x1 is Clique of R by A71, A89, FUNCT_1:3; A93: (f .\/ g) . 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 (f .\/ g) . x1 by A93, XBOOLE_0:def_3; A95: (f .\/ g) . 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 (f .\/ g) . x2 by A95, XBOOLE_0:def_3; hence x1 = x2 by A15, A89, A90, A91, A92, A94, Th15; ::_thesis: verum end; reconsider C = rng (f .\/ g) as Clique-partition of R by A16, A21, A40, A71, Def11, EQREL_1:def_4; take C ; ::_thesis: card C = stability# R card C = card (f .\/ g) by A88, PRE_POLY:19 .= card A by A15, A9, A13, CARD_1:62 ; hence card C = stability# R by A1; ::_thesis: verum end; definition let R be RelStr ; let P be a_partition of the carrier of R; attrP is StableSet-wise means :Def12: :: DILWORTH:def 12 for x being set st x in P holds x is StableSet of R; end; :: deftheorem Def12 defines StableSet-wise DILWORTH:def_12_:_ for R being RelStr for P being a_partition of the carrier of R holds ( P is StableSet-wise iff for x being set st x in P holds x is StableSet of R ); registration let R be RelStr ; cluster with_non-empty_elements StableSet-wise for a_partition of the carrier of R; existence ex b1 being a_partition of the carrier of R st b1 is StableSet-wise proof set cR = the carrier of R; percases ( R is empty or not R is empty ) ; suppose R is empty ; ::_thesis: ex b1 being a_partition of the carrier of R st b1 is StableSet-wise then reconsider S = {} as a_partition of the carrier of R by EQREL_1:45; take S ; ::_thesis: S is StableSet-wise let x be set ; :: according to DILWORTH:def_12 ::_thesis: ( x in S implies x is StableSet of R ) thus ( x in S implies x is StableSet of R ) ; ::_thesis: verum end; supposeA1: not R is empty ; ::_thesis: ex b1 being a_partition of the carrier of R st b1 is StableSet-wise then reconsider RR = R as non empty RelStr ; take S = SmallestPartition the carrier of R; ::_thesis: S is StableSet-wise let z be set ; :: according to DILWORTH:def_12 ::_thesis: ( z in S implies z is StableSet of R ) assume A2: z in S ; ::_thesis: z is StableSet of R S = { {x} where x is Element of the carrier of R : verum } 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; ::_thesis: verum end; 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 for b1 being a_partition of the carrier of R holds b1 is StableSet-wise proof let P be a_partition of the carrier of R; ::_thesis: P is StableSet-wise let x be set ; :: according to DILWORTH:def_12 ::_thesis: ( x in P implies x is StableSet of R ) thus ( x in P implies x is StableSet of R ) ; ::_thesis: verum end; end; theorem :: DILWORTH:50 for R being finite RelStr for C being Coloring of R holds card C >= clique# R proof let R be finite RelStr ; ::_thesis: for C being Coloring of R holds card C >= clique# R let C be Coloring of R; ::_thesis: card C >= clique# R assume A1: card C < clique# R ; ::_thesis: contradiction 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; percases ( R is empty or not R is empty ) ; suppose R is empty ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; supposeA4: not R is empty ; ::_thesis: contradiction defpred S1[ set , set ] means ( $1 in A & $2 in C & $1 in $2 ); A5: for x being set st x in A holds ex y being set st ( y in C & S1[x,y] ) proof let x be set ; ::_thesis: ( x in A implies ex y being set st ( y in C & S1[x,y] ) ) assume A6: x in A ; ::_thesis: ex y being set st ( y in C & S1[x,y] ) reconsider x9 = x as Element of R by A6; not the carrier of R is empty by A4; then x9 in the carrier of R ; 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 ; ::_thesis: ( y in C & S1[x,y] ) thus ( y in C & S1[x,y] ) by A6, A7, A8; ::_thesis: verum end; consider f being Function of A,C such that A9: for x being set st x in A holds S1[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; ::_thesis: verum end; end; end; begin theorem Th51: :: DILWORTH:51 for R being finite transitive antisymmetric RelStr ex C being Clique-partition of R st card C = stability# R proof defpred S1[ Nat] means for P being finite transitive antisymmetric RelStr st card P = $1 holds 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 S1[k] ) holds S1[n] proof let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds S1[k] ) implies S1[n] ) assume A2: for k being Nat st k < n holds S1[k] ; ::_thesis: S1[n] let P be finite transitive antisymmetric RelStr ; ::_thesis: ( card P = n implies ex C being Clique-partition of P st card C = stability# P ) assume A3: card P = n ; ::_thesis: ex C being Clique-partition of P st card C = stability# P set wP = stability# P; percases ( n = 0 or n > 0 ) ; supposeA4: n = 0 ; ::_thesis: ex C being Clique-partition of P st card C = stability# P then P is empty by A3; then reconsider C = {} as Clique-partition of P by EQREL_1:45; take C ; ::_thesis: card C = stability# P P is empty by A3, A4; hence card C = stability# P by A3, A4; ::_thesis: verum end; supposeA5: n > 0 ; ::_thesis: ex C being Clique-partition of P st card C = stability# P percases ( ex A being StableSet of P st ( card A = stability# P & A <> minimals P & A <> maximals P ) or for A being StableSet of P holds ( not card A = stability# P or A = minimals P or A = maximals P ) ) ; suppose ex A being StableSet of P st ( card A = stability# P & A <> minimals P & A <> maximals P ) ; ::_thesis: ex C being Clique-partition of P st card C = stability# 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; set bA = Lower A; set cP = the carrier of P; set Pa = subrelstr (Upper A); set Pb = subrelstr (Lower A); reconsider PP = P as non empty finite transitive antisymmetric RelStr by A5, A3; A9: Upper A = the carrier of (subrelstr (Upper A)) by YELLOW_0:def_15; A10: Lower A = the carrier of (subrelstr (Lower A)) by YELLOW_0:def_15; not minimals PP c= Upper A by A7, Th40, Th26; then consider mi being set such that A11: mi in minimals P and A12: not mi in Upper A by TARSKI:def_3; not maximals PP c= Lower A by A8, Th41, Th27; then consider ma being set such that A13: ma in maximals P and A14: not ma in Lower A by TARSKI:def_3; reconsider Pa = subrelstr (Upper A) as finite transitive antisymmetric RelStr ; mi in the carrier of P by A11; then Upper A c< the carrier of P 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 = stability# P by A6, Th45, XBOOLE_1:7; reconsider Pb = subrelstr (Lower A) as finite transitive antisymmetric RelStr ; ma in the carrier of P by A13; then Lower A c< the carrier of P 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 = stability# P 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 ; ::_thesis: card C = stability# P thus card C = stability# P by A18; ::_thesis: verum end; supposeA19: for A being StableSet of P holds ( not card A = stability# P or A = minimals P or A = maximals P ) ; ::_thesis: ex C being Clique-partition of P st card C = stability# P consider S being StableSet of P such that A20: card S = stability# P by Def6; reconsider PP = P as non empty finite transitive antisymmetric RelStr by A5, A3; set cR = the carrier of PP; set a = the Element of minimals P; A21: the Element of minimals P in minimals PP ; then reconsider a = the Element of minimals P 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 = the carrier of P \ {a,b}; A25: the carrier of P = ( the carrier of P \ {a,b}) \/ {a,b} by XBOOLE_1:45; A26: the carrier of P \ {a,b} misses {a,b} by XBOOLE_1:79; then A27: the carrier of P \ ( the carrier of P \ {a,b}) = {a,b} by A25, XBOOLE_1:88; reconsider cP9 = the carrier of P \ {a,b} as Subset of the carrier of PP ; set P9 = subrelstr cP9; A28: cP9 = the carrier of (subrelstr cP9) by YELLOW_0:def_15; A29: card cP9 = card (subrelstr cP9) by YELLOW_0:def_15; card cP9 = (card the carrier of P) - (card {a,b}) by CARD_2:44; then consider C being Clique-partition of (subrelstr cP9) such that A30: card C = stability# (subrelstr cP9) by A2, A3, A29, XREAL_1:44; A31: not {a,b} in C proof assume A32: {a,b} in C ; ::_thesis: contradiction a in {a,b} by TARSKI:def_2; hence contradiction by A26, A28, A32, ZFMISC_1:49; ::_thesis: verum end; set wP = stability# PP; set wP1 = (stability# PP) - 1; 0 + 1 <= stability# PP by NAT_1:13; then (0 + 1) - 1 <= (stability# PP) - 1 by XREAL_1:9; then (stability# PP) - 1 in NAT by INT_1:3; then reconsider wP1 = (stability# PP) - 1 as Nat ; set S9 = S /\ cP9; S /\ the carrier of P = S by XBOOLE_1:28; then A33: S /\ cP9 = S \ {a,b} by XBOOLE_1:49; A34: {a,b} = {a} \/ {b} by ENUMSET1:1; reconsider S9 = S /\ cP9 as StableSet of (subrelstr cP9) by Th31; A35: card S9 = wP1 proof percases ( S = minimals P or S = maximals PP ) by A19, A20; supposeA36: S = minimals P ; ::_thesis: card S9 = wP1 S9 = S \ {a} proof percases ( a = b or a <> b ) ; suppose a = b ; ::_thesis: S9 = S \ {a} hence S9 = S \ {a} by A33, ENUMSET1:29; ::_thesis: verum end; supposeA37: a <> b ; ::_thesis: S9 = S \ {a} now__::_thesis:_not_b_in_minimals_PP assume b in minimals PP ; ::_thesis: contradiction then b is_minimal_in [#] PP by Def9; hence contradiction by A37, A23, WAYBEL_4:56; ::_thesis: verum end; hence S9 = S \ {a} by A33, A34, A36, Th1; ::_thesis: verum end; end; end; hence card S9 = (card S) - (card {a}) by A36, EULER_1:4 .= wP1 by A20, CARD_1:30 ; ::_thesis: verum end; supposeA38: S = maximals PP ; ::_thesis: card S9 = wP1 A39: S9 = S \ {b} proof percases ( a = b or a <> b ) ; suppose a = b ; ::_thesis: S9 = S \ {b} hence S9 = S \ {b} by A33, ENUMSET1:29; ::_thesis: verum end; supposeA40: a <> b ; ::_thesis: S9 = S \ {b} now__::_thesis:_not_a_in_maximals_PP assume a in maximals PP ; ::_thesis: contradiction then a is_maximal_in [#] PP by Def10; hence contradiction by A40, A23, WAYBEL_4:55; ::_thesis: verum end; hence S9 = S \ {b} by A33, A34, A38, Th1; ::_thesis: verum end; 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 ; ::_thesis: verum end; end; end; for T being StableSet of (subrelstr cP9) holds card T <= card S9 proof let T be StableSet of (subrelstr cP9); ::_thesis: card T <= card S9 assume card T > card S9 ; ::_thesis: contradiction then card T >= (card S9) + 1 by NAT_1:13; then consider V being StableSet of (subrelstr cP9) 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; ::_thesis: verum end; then A42: (stability# (subrelstr cP9)) + 1 = ((stability# PP) - 1) + 1 by A35, Def6 .= stability# PP ; set CC = C \/ {{a,b}}; cP9 <> the carrier of P by A27, XBOOLE_1:37; then A43: cP9 c< the carrier of P by XBOOLE_0:def_8; now__::_thesis:_for_x_being_set_st_x_in_C_\/_{{a,b}}_holds_ x_is_Clique_of_P let x be set ; ::_thesis: ( x in C \/ {{a,b}} implies b1 is Clique of P ) assume A44: x in C \/ {{a,b}} ; ::_thesis: b1 is Clique of P percases ( x in C or x in {{a,b}} ) by A44, XBOOLE_0:def_3; suppose x in C ; ::_thesis: b1 is Clique of P then x is Clique of (subrelstr cP9) by Def11; hence x is Clique of P by Th28; ::_thesis: verum end; suppose x in {{a,b}} ; ::_thesis: b1 is Clique of P then A45: x = {a,b} by TARSKI:def_1; percases ( a = b or a <> b ) ; suppose a = b ; ::_thesis: b1 is Clique of P then x = {a} by A45, ENUMSET1:29; hence x is Clique of P ; ::_thesis: verum end; suppose a <> b ; ::_thesis: b1 is Clique of P then a <= b by A23, ORDERS_2:def_6; hence x is Clique of P by A45, Th8; ::_thesis: verum end; end; end; end; end; then reconsider CC = C \/ {{a,b}} as Clique-partition of P by A27, A28, Th4, Def11, A43; take CC ; ::_thesis: card CC = stability# P thus card CC = stability# P by A30, A42, A31, CARD_2:41; ::_thesis: verum end; end; end; end; end; A46: for n being Nat holds S1[n] from NAT_1:sch_4(A1); let R be finite transitive antisymmetric RelStr ; ::_thesis: ex C being Clique-partition of R st card C = stability# R card R = card R ; hence ex C being Clique-partition of R st card C = stability# R by A46; ::_thesis: verum end; definition let R be non empty with_finite_stability# RelStr ; let C be Subset of R; attrC is strong-chain means :Def13: :: DILWORTH:def 13 for S being non empty finite Subset of R ex P being Clique-partition of (subrelstr S) st ( card P <= stability# R & ex c being set st ( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds C /\ d = {} ) ) ); end; :: deftheorem Def13 defines strong-chain DILWORTH:def_13_:_ for R being non empty with_finite_stability# RelStr for C being Subset of R holds ( C is strong-chain iff for S being non empty finite Subset of R ex P being Clique-partition of (subrelstr S) st ( card P <= stability# R & ex c being set st ( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds C /\ d = {} ) ) ) ); registration let R be non empty with_finite_stability# RelStr ; cluster strong-chain -> clique for Element of bool the carrier of R; coherence for b1 being Subset of R st b1 is strong-chain holds b1 is clique proof let C be Subset of R; ::_thesis: ( C is strong-chain implies C is clique ) assume A1: C is strong-chain ; ::_thesis: C is clique now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_C_&_b_in_C_&_a_<>_b_&_not_a_<=_b_holds_ b_<=_a let a, b be Element of R; ::_thesis: ( a in C & b in C & a <> b & not a <= b implies b <= a ) assume that A2: a in C and A3: b in C and A4: a <> b ; ::_thesis: ( a <= b or b <= a ) set S = {a,b}; reconsider S = {a,b} as non empty finite 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; ::_thesis: verum end; hence C is clique by Th6; ::_thesis: verum end; end; registration let R be non empty transitive antisymmetric with_finite_stability# RelStr ; cluster1 -element -> strong-chain for Element of bool the carrier of R; coherence for b1 being Subset of R st b1 is 1 -element holds b1 is strong-chain proof let C be Subset of R; ::_thesis: ( C is 1 -element implies C is strong-chain ) assume C is 1 -element ; ::_thesis: C is strong-chain then consider x being set such that A1: C = {x} by ZFMISC_1:131; let S be non empty finite Subset of R; :: according to DILWORTH:def_13 ::_thesis: 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 = {} ) ) ) 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 ; ::_thesis: ( 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 = {} ) ) ) thus card P <= stability# R by A2, Th44; ::_thesis: 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 = {} ) ) percases ( x in S or not x in S ) ; suppose x in S ; ::_thesis: 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 = {} ) ) 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 ; ::_thesis: ( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds C /\ d = {} ) ) thus c in P by A5; ::_thesis: ( S /\ C c= c & ( for d being set st d in P & d <> c holds C /\ d = {} ) ) thus S /\ C c= c ::_thesis: for d being set st d in P & d <> c holds C /\ d = {} proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in S /\ C or a in c ) assume a in S /\ C ; ::_thesis: a in c then a in C by XBOOLE_0:def_4; hence a in c by A4, A1, TARSKI:def_1; ::_thesis: verum end; let d be set ; ::_thesis: ( d in P & d <> c implies C /\ d = {} ) assume that A6: d in P and A7: d <> c ; ::_thesis: C /\ d = {} assume C /\ d <> {} ; ::_thesis: contradiction then consider a being set such that A8: a in C /\ d by XBOOLE_0:def_1; reconsider d = d, c = 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; ::_thesis: verum end; supposeA9: not x in S ; ::_thesis: 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 = {} ) ) set c = the Element of P; take the Element of P ; ::_thesis: ( the Element of P in P & S /\ C c= the Element of P & ( for d being set st d in P & d <> the Element of P holds C /\ d = {} ) ) thus the Element of P in P ; ::_thesis: ( S /\ C c= the Element of P & ( for d being set st d in P & d <> the Element of P holds C /\ d = {} ) ) C misses S by A9, A1, ZFMISC_1:50; then S /\ C = {} by XBOOLE_0:def_7; hence S /\ C c= the Element of P by XBOOLE_1:2; ::_thesis: for d being set st d in P & d <> the Element of P holds C /\ d = {} let d be set ; ::_thesis: ( d in P & d <> the Element of P implies C /\ d = {} ) assume that A10: d in P and d <> the Element of P ; ::_thesis: C /\ d = {} 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; ::_thesis: verum end; end; end; end; theorem Th52: :: DILWORTH:52 for R being non empty transitive antisymmetric with_finite_stability# RelStr ex S being non empty Subset of R st ( S is strong-chain & ( for D being Subset of R holds ( not D is strong-chain or not S c< D ) ) ) proof let R be non empty transitive antisymmetric with_finite_stability# RelStr ; ::_thesis: ex S being non empty Subset of R st ( S is strong-chain & ( for D being Subset of R holds ( not D is strong-chain or not S c< D ) ) ) set E = { C where C is Subset of R : C is strong-chain } ; set x = the Element of R; A1: { the Element of R} in { C where C is Subset of R : C is strong-chain } ; now__::_thesis:_for_Z_being_set_st_Z_c=__{__C_where_C_is_Subset_of_R_:_C_is_strong-chain__}__&_Z_is_c=-linear_holds_ ex_Y_being_set_st_ (_Y_in__{__C_where_C_is_Subset_of_R_:_C_is_strong-chain__}__&_(_for_X1_being_set_st_X1_in_Z_holds_ X1_c=_Y_)_) let Z be set ; ::_thesis: ( Z c= { C where C is Subset of R : C is strong-chain } & Z is c=-linear implies ex Y being set st ( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds X1 c= Y ) ) ) assume that A2: Z c= { C where C is Subset of R : C is strong-chain } and A3: Z is c=-linear ; ::_thesis: ex Y being set st ( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds X1 c= Y ) ) set Y = union Z; take Y = union Z; ::_thesis: ( Y in { C where C is Subset of R : C is strong-chain } & ( for X1 being set st X1 in Z holds X1 c= Y ) ) now__::_thesis:_for_B_being_set_st_B_in_Z_holds_ B_c=_the_carrier_of_R let B be set ; ::_thesis: ( B in Z implies B c= the carrier of R ) assume B in Z ; ::_thesis: B c= the carrier of R then B in { C where C is Subset of R : C is strong-chain } by A2; then ex C being Subset of R st ( C = B & C is strong-chain ) ; hence B c= the carrier of R ; ::_thesis: verum end; then reconsider Y9 = Y as Subset of R by ZFMISC_1:76; Y9 is strong-chain proof let S be non empty finite Subset of R; :: according to DILWORTH:def_13 ::_thesis: ex P being Clique-partition of (subrelstr S) st ( card P <= stability# R & ex c being set st ( c in P & S /\ Y9 c= c & ( for d being set st d in P & d <> c holds Y9 /\ d = {} ) ) ) set F = S /\ Y; percases ( S /\ Y is empty or not S /\ Y is empty ) ; supposeA4: S /\ Y is empty ; ::_thesis: ex P being Clique-partition of (subrelstr S) st ( card P <= stability# R & ex c being set st ( c in P & S /\ Y9 c= c & ( for d being set st d in P & d <> c holds Y9 /\ d = {} ) ) ) consider p being Clique-partition of (subrelstr S) such that A5: card p = stability# (subrelstr S) by Th51; take p ; ::_thesis: ( card p <= stability# R & ex c being set st ( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds Y9 /\ d = {} ) ) ) thus card p <= stability# R by Th44, A5; ::_thesis: ex c being set st ( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds Y9 /\ d = {} ) ) set c = the Element of p; take the Element of p ; ::_thesis: ( the Element of p in p & S /\ Y9 c= the Element of p & ( for d being set st d in p & d <> the Element of p holds Y9 /\ d = {} ) ) thus the Element of p in p ; ::_thesis: ( S /\ Y9 c= the Element of p & ( for d being set st d in p & d <> the Element of p holds Y9 /\ d = {} ) ) thus S /\ Y9 c= the Element of p by A4, XBOOLE_1:2; ::_thesis: for d being set st d in p & d <> the Element of p holds Y9 /\ d = {} let d be set ; ::_thesis: ( d in p & d <> the Element of p implies Y9 /\ d = {} ) assume that A6: d in p and d <> the Element of p ; ::_thesis: Y9 /\ d = {} 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, XBOOLE_1:26; ::_thesis: verum end; supposeA7: not S /\ Y is empty ; ::_thesis: ex P being Clique-partition of (subrelstr S) st ( card P <= stability# R & ex c being set st ( c in P & S /\ Y9 c= c & ( for d being set st d in P & d <> c holds Y9 /\ d = {} ) ) ) then A8: not Z is empty by ZFMISC_1:2; defpred S1[ set , set ] means ( $1 in S /\ Y & $2 in Z & $1 in $2 ); A9: for x being set st x in S /\ Y holds ex y being set st ( y in Z & S1[x,y] ) proof let x be set ; ::_thesis: ( x in S /\ Y implies ex y being set st ( y in Z & S1[x,y] ) ) assume A10: x in S /\ Y ; ::_thesis: ex y being set st ( y in Z & S1[x,y] ) 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 ; ::_thesis: ( y in Z & S1[x,y] ) thus ( y in Z & S1[x,y] ) by A12, A10, A11; ::_thesis: verum end; consider f being Function of (S /\ Y),Z such that A13: for x being set st x in S /\ Y holds S1[x,f . x] from FUNCT_2:sch_1(A9); set rf = rng f; ( rng f c= Z & Z is c=-linear implies rng f is c=-linear ) ; then consider m being set such that A14: m in rng f and A15: for C being set st C in rng f holds C c= m by A3, A7, A8, FINSET_1:12, RELAT_1:def_19; rng f c= Z by RELAT_1:def_19; then m in Z by A14; then m in { C where C is Subset of R : C is strong-chain } by A2; then consider C being Subset of R such that A16: m = C and A17: C is strong-chain ; A18: S /\ Y c= C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S /\ Y or x in C ) assume A19: x in S /\ Y ; ::_thesis: x in C 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; ::_thesis: verum 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 ; ::_thesis: ( card p <= stability# R & ex c being set st ( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds Y9 /\ d = {} ) ) ) thus card p <= stability# R by A21; ::_thesis: ex c being set st ( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds Y9 /\ d = {} ) ) 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 ; ::_thesis: ( c in p & S /\ Y9 c= c & ( for d being set st d in p & d <> c holds Y9 /\ d = {} ) ) thus c in p by A23; ::_thesis: ( S /\ Y9 c= c & ( for d being set st d in p & d <> c holds Y9 /\ d = {} ) ) thus S /\ Y9 c= c ::_thesis: for d being set st d in p & d <> c holds Y9 /\ d = {} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S /\ Y9 or x in c ) assume x in S /\ Y9 ; ::_thesis: x in c 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; ::_thesis: verum end; let d be set ; ::_thesis: ( d in p & d <> c implies Y9 /\ d = {} ) assume that A26: d in p and A27: d <> c ; ::_thesis: Y9 /\ d = {} assume Y9 /\ d <> {} ; ::_thesis: contradiction 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 S /\ Y 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; ::_thesis: verum end; end; end; hence Y in { C where C is Subset of R : C is strong-chain } ; ::_thesis: for X1 being set st X1 in Z holds X1 c= Y let X1 be set ; ::_thesis: ( X1 in Z implies X1 c= Y ) assume A31: X1 in Z ; ::_thesis: X1 c= Y thus X1 c= Y by A31, ZFMISC_1:74; ::_thesis: verum end; then consider Y being set such that A32: Y in { C where C is Subset of R : C is strong-chain } and A33: for Z being set st Z in { C where C is Subset of R : C is strong-chain } & 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 ; ::_thesis: ( S is strong-chain & ( for D being Subset of R holds ( not D is strong-chain or not S c< D ) ) ) thus S is strong-chain by A35; ::_thesis: for D being Subset of R holds ( not D is strong-chain or not S c< D ) let D be Subset of R; ::_thesis: ( not D is strong-chain or not S c< D ) assume that A36: D is strong-chain and A37: S c< D ; ::_thesis: contradiction A38: D in { C where C is Subset of R : C is strong-chain } by A36; ( D <> S & S c= D ) by A37, XBOOLE_0:def_8; hence contradiction by A34, A38, A33; ::_thesis: verum end; theorem :: DILWORTH:53 for R being transitive antisymmetric with_finite_stability# RelStr ex C being Clique-partition of R st card C = stability# R proof let R be transitive antisymmetric with_finite_stability# RelStr ; ::_thesis: ex C being Clique-partition of R st card C = stability# R percases ( R is finite or R is infinite ) ; suppose R is finite ; ::_thesis: ex C being Clique-partition of R st card C = stability# R hence ex C being Clique-partition of R st card C = stability# R by Th51; ::_thesis: verum end; supposeA1: R is infinite ; ::_thesis: ex C being Clique-partition of R st card C = stability# R defpred S1[ Nat] means for P being non empty transitive antisymmetric with_finite_stability# RelStr st stability# P = $1 holds ex C being Clique-partition of P st card C = stability# P; A2: S1[ 0 ] ; A3: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] let P be non empty transitive antisymmetric with_finite_stability# RelStr ; ::_thesis: ( stability# P = k + 1 implies ex C being Clique-partition of P st card C = stability# P ) assume A5: stability# P = k + 1 ; ::_thesis: ex C being Clique-partition of P st card C = stability# P consider C being non empty Subset of P such that A6: C is strong-chain and A7: for D being Subset of P holds ( not D is strong-chain or not C c< D ) by Th52; set cP = the carrier of P; percases ( C = the carrier of P or C <> the carrier of P ) ; supposeA8: C = the carrier of P ; ::_thesis: ex C being Clique-partition of P st card C = stability# P 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 ; ::_thesis: card Cp = stability# P A9: the carrier of P = [#] P ; thus card Cp = 1 by CARD_1:30 .= stability# P by A9, A6, A8, Th20 ; ::_thesis: verum end; suppose C <> the carrier of P ; ::_thesis: ex C being Clique-partition of P st card C = stability# P then A10: C c< the carrier of P by XBOOLE_0:def_8; set cP9 = the carrier of P \ C; A11: the carrier of P \ ( the carrier of P \ C) = the carrier of P /\ C by XBOOLE_1:48 .= C by XBOOLE_1:28 ; reconsider cP9 = the carrier of P \ C as Subset of P ; cP9 <> {} by A10, XBOOLE_1:105; then reconsider P9 = subrelstr cP9 as non empty transitive antisymmetric with_finite_stability# 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 ; ::_thesis: contradiction consider A being finite StableSet of P9 such that A16: card A = stability# P9 by Def6; reconsider A9 = A as non empty finite StableSet of P by A16, Th30; defpred S2[ set , set , set ] means for c being set holds ( not c in $2 or not $1 /\ $3 c= c or ex d being set st ( d in $2 & d <> c & $3 /\ d <> {} ) ); defpred S3[ finite Subset of P, set ] means for p being Clique-partition of (subrelstr $1) st card p <= stability# P holds S2[$1,p,$2]; defpred S4[ set , set ] means ex S being non empty finite Subset of P st ( $2 = S & $1 in $2 & S3[S,C \/ {$1}] ); A17: for x being set st x in A holds ex y being set st S4[x,y] proof let a be set ; ::_thesis: ( a in A implies ex y being set st S4[a,y] ) assume A18: a in A ; ::_thesis: ex y being set st S4[a,y] A c= the carrier of P by A12, XBOOLE_1:1; then {a} c= the carrier of P by A18, ZFMISC_1:31; then reconsider Ca = C \/ {a} as Subset of P by XBOOLE_1:8; now__::_thesis:_not_Ca_is_strong-chain assume A19: Ca is strong-chain ; ::_thesis: contradiction 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; ::_thesis: verum end; then consider S being non empty finite Subset of P such that A22: S3[S,Ca] by Def13; take S ; ::_thesis: S4[a,S] take S ; ::_thesis: ( S = S & a in S & S3[S,C \/ {a}] ) thus S = S ; ::_thesis: ( a in S & S3[S,C \/ {a}] ) now__::_thesis:_a_in_S assume A23: not a in S ; ::_thesis: contradiction A24: S /\ C c= S /\ Ca proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S /\ C or x in S /\ Ca ) assume x in S /\ C ; ::_thesis: x in S /\ Ca 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; ::_thesis: verum end; S /\ Ca c= S /\ C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S /\ Ca or x in S /\ C ) assume A25: x in S /\ Ca ; ::_thesis: x in S /\ C 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; ::_thesis: verum 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 S2[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 ; ::_thesis: ( d in p & d <> c implies Ca /\ d = {} ) assume that A33: d in p and A34: d <> c ; ::_thesis: Ca /\ d = {} now__::_thesis:_not_Ca_/\_d_<>_{} assume Ca /\ d <> {} ; ::_thesis: contradiction 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; percases ( x in C or x in {a} ) by A36, XBOOLE_0:def_3; suppose x in C ; ::_thesis: contradiction then x in C /\ d by A37, XBOOLE_0:def_4; hence contradiction by A33, A34, A32; ::_thesis: verum end; suppose x in {a} ; ::_thesis: contradiction 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; ::_thesis: verum end; end; end; hence Ca /\ d = {} ; ::_thesis: verum end; hence contradiction by A30, A31, A28, A27, A22; ::_thesis: verum end; hence a in S ; ::_thesis: S3[S,C \/ {a}] thus S3[S,C \/ {a}] by A22; ::_thesis: verum end; consider f being Function such that A38: dom f = A and A39: for x being set st x in A holds S4[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 ; ::_thesis: ( x in rng f implies x is finite ) assume x in rng f ; ::_thesis: x is finite 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 non empty finite Subset of P such that A44: f . a = S and ( a in f . a & S3[S,C \/ {a}] ) by A38, A42, A39; thus x is finite by A44, A43; ::_thesis: verum end; A45: union (rng f) c= the carrier of P proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng f) or x in the carrier of P ) assume x in union (rng f) ; ::_thesis: x in the carrier of P 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 non empty finite Subset of P such that A50: f . a = S and ( a in f . a & S3[S,C \/ {a}] ) by A38, A48, A39; thus x in the carrier of P by A46, A49, A50; ::_thesis: verum end; A51: A9 c= union (rng f) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A9 or x in union (rng f) ) assume A52: x in A9 ; ::_thesis: x in union (rng f) then consider S being non empty finite Subset of P such that f . x = S and A53: x in f . x and S3[S,C \/ {x}] by A39; f . x in rng f by A52, A38, FUNCT_1:3; hence x in union (rng f) by A53, TARSKI:def_4; ::_thesis: verum end; then reconsider SS = union (rng f) as non empty finite Subset of P by A41, A40, A45, FINSET_1:7; set SSp = subrelstr SS; A54: SS = the carrier of (subrelstr SS) by YELLOW_0:def_15; consider p being Clique-partition of (subrelstr SS) such that A55: card p <= stability# P and A56: not S2[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 = c as Element of p by A57; A9 = A9 /\ SS by A51, XBOOLE_1:28; then reconsider A = A9 as non empty finite StableSet of (subrelstr SS) by Th31; A60: stability# (subrelstr SS) >= card A by Def6; card p >= stability# (subrelstr SS) 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 non empty finite Subset of P such that A63: f . a = S and A64: a in f . a and A65: S3[S,C \/ {a}] by A39; deffunc H1( set ) -> Element of bool the carrier of P = $1 /\ S; defpred S5[ set ] means $1 meets S; set Sp = { H1(e) where e is Element of p : S5[e] } ; A66: S c= SS proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in SS ) assume A67: x in S ; ::_thesis: x in SS S in rng f by A63, A38, FUNCT_1:3; hence x in SS by A67, TARSKI:def_4; ::_thesis: verum end; then reconsider Sp = { H1(e) where e is Element of p : S5[e] } 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 ; ::_thesis: ( x in Sp implies x is Clique of (subrelstr S) ) assume x in Sp ; ::_thesis: x is Clique of (subrelstr S) then consider e being Element of p such that A68: x = e /\ S and e meets S ; e is Clique of (subrelstr SS) by Def11; then e is Clique of P by Th28; hence x is Clique of (subrelstr S) by A68, Th29; ::_thesis: verum end; then reconsider Sp = Sp as Clique-partition of (subrelstr S) by Def11, YELLOW_0:def_15; A69: Sp = { H1(e) where e is Element of p : S5[e] } ; A70: card Sp <= card p from DILWORTH:sch_1(A69); set cc = c /\ S; c meets S by A62, A63, A64, XBOOLE_0:3; then A71: c /\ S in Sp ; S /\ (C \/ {a}) c= c /\ S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S /\ (C \/ {a}) or x in c /\ S ) assume A72: x in S /\ (C \/ {a}) ; ::_thesis: x in c /\ S then A73: x in S by XBOOLE_0:def_4; A74: x in C \/ {a} by A72, XBOOLE_0:def_4; percases ( x in C or x in {a} ) by A74, XBOOLE_0:def_3; suppose x in C ; ::_thesis: x in c /\ S then x in SS /\ C by A73, A66, XBOOLE_0:def_4; hence x in c /\ S by A73, A58, XBOOLE_0:def_4; ::_thesis: verum end; suppose x in {a} ; ::_thesis: x in c /\ S then x = a by TARSKI:def_1; hence x in c /\ S by A62, A63, A64, XBOOLE_0:def_4; ::_thesis: verum end; end; end; then consider d being set such that A75: d in Sp and A76: d <> c /\ S 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; ::_thesis: verum 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 percases ( A /\ C = {} or A /\ C <> {} ) ; supposeA84: A /\ C = {} ; ::_thesis: stability# P9 = k A c= cP9 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in cP9 ) assume A85: x in A ; ::_thesis: x in cP9 then not x in C by A84, XBOOLE_0:def_4; hence x in cP9 by A85, XBOOLE_0:def_5; ::_thesis: verum end; hence stability# P9 = k by A5, A14, A82, Th45; ::_thesis: verum end; suppose A /\ C <> {} ; ::_thesis: stability# P9 = k 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 = (A \ {x}) \/ {x} by XBOOLE_1:45; x in {x} by TARSKI:def_1; then not x in A \ {x} by XBOOLE_0:def_5; then A90: card A = (card (A \ {x})) + 1 by A89, CARD_2:41; A91: A \ {x} c= A by XBOOLE_1:36; A \ {x} c= cP9 proof let xx be set ; :: according to TARSKI:def_3 ::_thesis: ( not xx in A \ {x} or xx in cP9 ) assume A92: xx in A \ {x} ; ::_thesis: xx in cP9 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; ::_thesis: verum end; then A94: A \ {x} c= A /\ cP9 by A91, XBOOLE_1:19; A /\ cP9 c= A \ {x} proof let xx be set ; :: according to TARSKI:def_3 ::_thesis: ( not xx in A /\ cP9 or xx in A \ {x} ) assume A95: xx in A /\ cP9 ; ::_thesis: xx in A \ {x} 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 A \ {x} by A96, XBOOLE_0:def_5; ::_thesis: verum end; then A \ {x} = A /\ cP9 by A94, XBOOLE_0:def_10; then reconsider A9 = A \ {x} as StableSet of P9 by Th31; stability# P9 >= card A9 by Def6; hence stability# P9 = k by A90, A82, A5, A81, XXREAL_0:1; ::_thesis: verum end; end; end; then consider Cp9 being Clique-partition of P9 such that A97: card Cp9 = stability# P9 by A4; set Cp = Cp9 \/ {( the carrier of P \ cP9)}; A98: Cp9 is finite by A97; cP9 <> the carrier of P by A11, XBOOLE_1:37; then A99: cP9 c< the carrier of P by XBOOLE_0:def_8; then reconsider Cp = Cp9 \/ {( the carrier of P \ cP9)} as a_partition of the carrier of P by A12, Th4; now__::_thesis:_for_x_being_set_st_x_in_Cp_holds_ x_is_Clique_of_P let x be set ; ::_thesis: ( x in Cp implies b1 is Clique of P ) assume A100: x in Cp ; ::_thesis: b1 is Clique of P percases ( x in Cp9 or x in {( the carrier of P \ cP9)} ) by A100, XBOOLE_0:def_3; suppose x in Cp9 ; ::_thesis: b1 is Clique of P then x is Clique of P9 by Def11; hence x is Clique of P by Th28; ::_thesis: verum end; suppose x in {( the carrier of P \ cP9)} ; ::_thesis: b1 is Clique of P hence x is Clique of P by A6, A11, TARSKI:def_1; ::_thesis: verum end; end; end; then reconsider Cp = Cp as Clique-partition of P by Def11; take Cp ; ::_thesis: card Cp = stability# P not the carrier of P \ cP9 in Cp9 proof assume the carrier of P \ cP9 in Cp9 ; ::_thesis: contradiction then the carrier of P c= cP9 \/ cP9 by A12, XBOOLE_1:44; hence contradiction by A99, XBOOLE_1:60; ::_thesis: verum end; hence card Cp = stability# P by A5, A83, A97, A98, CARD_2:41; ::_thesis: verum end; end; end; for k being Nat holds S1[k] from NAT_1:sch_2(A2, A3); hence ex C being Clique-partition of R st card C = stability# R by A1; ::_thesis: verum end; end; end; theorem :: DILWORTH:54 for R being transitive antisymmetric with_finite_clique# RelStr ex A being Coloring of R st card A = clique# R proof let R be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: ex A being Coloring of R st card A = clique# R defpred S1[ Nat] means for P being transitive antisymmetric with_finite_clique# RelStr st clique# P = $1 holds ex A being Coloring of P st card A = clique# P; A1: S1[ 0 ] proof let P be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: ( clique# P = 0 implies ex A being Coloring of P st card A = clique# P ) assume A2: clique# P = 0 ; ::_thesis: ex A being Coloring of P st card A = clique# P then P is empty ; then reconsider C = {} as Coloring of P by EQREL_1:45; take C ; ::_thesis: card C = clique# P thus card C = clique# P by A2; ::_thesis: verum end; A3: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: S1[n] ; ::_thesis: S1[n + 1] let P be transitive antisymmetric with_finite_clique# RelStr ; ::_thesis: ( clique# P = n + 1 implies ex A being Coloring of P st card A = clique# P ) assume A5: clique# P = n + 1 ; ::_thesis: ex A being Coloring of P st card A = clique# P then A6: not P is empty ; reconsider PP = P as non empty transitive antisymmetric with_finite_clique# RelStr by A5; set M = maximals PP; set cP = the carrier of P; set cPM = the carrier of P \ (maximals PP); reconsider cPM = the carrier of P \ (maximals PP) as Subset of P ; set PM = subrelstr cPM; A7: cPM = the carrier of (subrelstr cPM) by YELLOW_0:def_15; reconsider PM = subrelstr cPM as transitive antisymmetric with_finite_clique# RelStr ; consider Ca being finite Clique of PM such that A8: card Ca = clique# PM by Def4; A9: Ca is Clique of P by Th28; consider C being finite Clique of P such that A10: card C = n + 1 by A5, Def4; A11: C <> {} by A10; set cC = C /\ cPM; reconsider cC = C /\ cPM as finite Clique of PM by Th29; consider m being Element of P such that A12: m in C and A13: m is_maximal_wrt C, the InternalRel of P by A6, A11, BAGORDER:6; A14: m is_maximal_in C by A13, WAYBEL_4:def_24; A15: C /\ (maximals PP) = {m} proof thus C /\ (maximals PP) c= {m} :: according to XBOOLE_0:def_10 ::_thesis: {m} c= C /\ (maximals PP) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in C /\ (maximals PP) or a in {m} ) assume A16: a in C /\ (maximals PP) ; ::_thesis: a in {m} then A17: a in C by XBOOLE_0:def_4; A18: a in maximals PP by A16, XBOOLE_0:def_4; reconsider a9 = a as Element of P by A16; A19: a9 is_maximal_in [#] P by A18, Def10; now__::_thesis:_not_a_<>_m assume A20: a <> m ; ::_thesis: contradiction 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; ::_thesis: verum end; hence a in {m} by TARSKI:def_1; ::_thesis: verum end; thus {m} c= C /\ (maximals PP) ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {m} or a in C /\ (maximals PP) ) assume a in {m} ; ::_thesis: a in C /\ (maximals PP) then A21: a = m by TARSKI:def_1; now__::_thesis:_a_in_maximals_PP assume A22: not a in maximals PP ; ::_thesis: contradiction consider y being Element of P such that A23: y is_maximal_in [#] P and A24: ( m = y or m < y ) by A6, Th38; set Cm = C \/ {y}; now__::_thesis:_C_\/_{y}_is_finite_Clique_of_P percases ( m = y or m <> y ) ; suppose m = y ; ::_thesis: C \/ {y} is finite Clique of P hence C \/ {y} is finite Clique of P by A12, ZFMISC_1:40; ::_thesis: verum end; suppose m <> y ; ::_thesis: C \/ {y} is finite Clique of P then m <= y by A24, ORDERS_2:def_6; hence C \/ {y} is finite Clique of P by A14, Th11; ::_thesis: verum end; end; end; then reconsider Cm = C \/ {y} as finite Clique of P ; not y in C by A21, A22, A23, Def10, A24, A14, WAYBEL_4:55; then card Cm = (card C) + 1 by CARD_2:41; then (n + 1) + 1 <= (n + 1) + 0 by A10, A5, Def4; hence contradiction by XREAL_1:6; ::_thesis: verum end; hence a in C /\ (maximals PP) by A21, A12, XBOOLE_0:def_4; ::_thesis: verum end; end; A25: cC = (C /\ the carrier of P) \ (C /\ (maximals PP)) by XBOOLE_1:50; C /\ the carrier of P = C by XBOOLE_1:28; then A26: card cC = (card C) - (card {m}) by A12, A15, A25, EULER_1:4 .= (n + 1) - 1 by A10, CARD_1:30 .= n ; A27: clique# PM >= card cC by Def4; A28: clique# PM <= clique# P by Th42; now__::_thesis:_not_clique#_PM_=_n_+_1 assume A29: clique# PM = n + 1 ; ::_thesis: contradiction then A30: Ca <> {} by A8; A31: not PM is empty by A29; then consider x being Element of PM such that A32: x in Ca and A33: x is_maximal_wrt Ca, the InternalRel of PM by A30, BAGORDER:6; A34: x is_maximal_in Ca by A33, WAYBEL_4:def_24; reconsider x9 = x as Element of P by A31, YELLOW_0:58; consider y being Element of P such that A35: y is_maximal_in [#] P and A36: ( x9 = y or x9 < y ) by Th38; set Cb = Ca \/ {y}; now__::_thesis:_Ca_\/_{y}_is_finite_Clique_of_P percases ( x9 = y or x9 <> y ) ; suppose x9 = y ; ::_thesis: Ca \/ {y} is finite Clique of P hence Ca \/ {y} is finite Clique of P by A32, A9, ZFMISC_1:40; ::_thesis: verum end; suppose x9 <> y ; ::_thesis: Ca \/ {y} is finite Clique of P then x9 <= y by A36, ORDERS_2:def_6; hence Ca \/ {y} is finite Clique of P by A34, Th32, A9, Th11; ::_thesis: verum end; end; end; then reconsider Cb = Ca \/ {y} as finite Clique of P ; y in maximals PP by A35, Def10; then not y in Ca by A7, XBOOLE_0:def_5; then A37: card Cb = (n + 1) + 1 by A8, A29, CARD_2:41; card Cb <= n + 1 by A5, Def4; then n + 1 <= n + 0 by A37, XREAL_1:6; hence contradiction by XREAL_1:6; ::_thesis: verum end; then clique# PM < n + 1 by A5, A28, XXREAL_0:1; then clique# PM <= n by NAT_1:13; then clique# PM = n by A26, A27, XXREAL_0:1; then consider Aa being Coloring of PM such that A38: card Aa = n by A4; reconsider Ab = Aa as finite set by A38; set A = Aa \/ {(maximals PP)}; A39: the carrier of P = cPM \/ (maximals PP) by XBOOLE_1:45; {(maximals PP)} is a_partition of maximals PP by EQREL_1:39; then A40: Aa \/ {(maximals PP)} is a_partition of the carrier of P by A39, A7, Th3, XBOOLE_1:79; now__::_thesis:_for_x_being_set_st_x_in_Aa_\/_{(maximals_PP)}_holds_ x_is_StableSet_of_P let x be set ; ::_thesis: ( x in Aa \/ {(maximals PP)} implies b1 is StableSet of P ) assume A41: x in Aa \/ {(maximals PP)} ; ::_thesis: b1 is StableSet of P percases ( x in Aa or x in {(maximals PP)} ) by A41, XBOOLE_0:def_3; suppose x in Aa ; ::_thesis: b1 is StableSet of P then x is StableSet of PM by Def12; hence x is StableSet of P by Th30; ::_thesis: verum end; suppose x in {(maximals PP)} ; ::_thesis: b1 is StableSet of P hence x is StableSet of P by TARSKI:def_1; ::_thesis: verum end; end; end; then reconsider A = Aa \/ {(maximals PP)} as Coloring of P by A40, Def12; take A ; ::_thesis: card A = clique# P not maximals PP in Ab by A7, XBOOLE_1:38; hence card A = clique# P by A5, A38, CARD_2:41; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A3); hence ex A being Coloring of R st card A = clique# R ; ::_thesis: verum end; begin theorem Th55: :: DILWORTH:55 for R being finite transitive antisymmetric RelStr for r, s being Nat holds ( not card R = (r * s) + 1 or ex C being Clique of R st card C >= r + 1 or ex A being StableSet of R st card A >= s + 1 ) proof let R be finite transitive antisymmetric RelStr ; ::_thesis: for r, s being Nat holds ( not card R = (r * s) + 1 or ex C being Clique of R st card C >= r + 1 or ex A being StableSet of R st card A >= s + 1 ) let r, s be Nat; ::_thesis: ( not card R = (r * s) + 1 or ex C being Clique of R st card C >= r + 1 or ex A being StableSet of R st card A >= s + 1 ) assume 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 ; ::_thesis: contradiction 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 (canFS p) = card p by UPROOTS:3; A8: dom (canFS p) = Seg (len (canFS p)) by FINSEQ_1:def_3; set f = canFS p; A9: rng (canFS p) = p by FUNCT_2:def_3; then reconsider f = canFS p as FinSequence of bool the carrier of R by FINSEQ_1:def_4; now__::_thesis:_for_d,_e_being_Nat_st_d_in_dom_f_&_e_in_dom_f_&_d_<>_e_holds_ f_._d_misses_f_._e let d, e be Nat; ::_thesis: ( d in dom f & e in dom f & d <> e implies f . d misses f . e ) assume that A10: d in dom f and A11: e in dom f and A12: d <> e ; ::_thesis: f . d misses f . 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 the carrier of R 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; ::_thesis: verum 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 = (stability# R) |-> n9 as Element of (stability# R) -tuples_on NAT ; A16: Sum h = (stability# R) * r by RVSUM_1:80; dom f = dom (Card f) by CARD_3:def_2; then len (Card f) = stability# R by A7, A4, FINSEQ_3:29; then reconsider Cf = Card f as Element of (stability# R) -tuples_on NAT by FINSEQ_2:92; A17: h is Element of (stability# R) -tuples_on REAL by FINSEQ_2:109; A18: Cf is Element of (stability# R) -tuples_on REAL by FINSEQ_2:109; now__::_thesis:_for_j_being_Nat_st_j_in_Seg_(stability#_R)_holds_ Cf_._j_<=_h_._j let j be Nat; ::_thesis: ( j in Seg (stability# R) implies Cf . j <= h . j ) assume A19: j in Seg (stability# R) ; ::_thesis: Cf . j <= h . j 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; ::_thesis: verum end; then A22: Sum Cf <= Sum h by A17, A18, RVSUM_1:82; (stability# R) * 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; ::_thesis: verum end; theorem :: DILWORTH:56 for f being real-valued FinSequence for n being Nat st card f = (n ^2) + 1 & f is one-to-one holds ex g being real-valued FinSubsequence st ( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) ) proof let f be real-valued FinSequence; ::_thesis: for n being Nat st card f = (n ^2) + 1 & f is one-to-one holds ex g being real-valued FinSubsequence st ( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) ) let n be Nat; ::_thesis: ( card f = (n ^2) + 1 & f is one-to-one implies ex g being real-valued FinSubsequence st ( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) ) ) assume that A1: card f = (n ^2) + 1 and A2: f is one-to-one ; ::_thesis: ex g being real-valued FinSubsequence st ( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) ) set cP = f; defpred S1[ set , set ] means ex i, j being Nat ex r, s being real number st ( $1 = [i,r] & $2 = [j,s] & i < j & r < s ); consider iP being Relation of f,f such that A3: for x, y being set holds ( [x,y] in iP iff ( x in f & y in f & S1[x,y] ) ) from RELSET_1:sch_1(); set P = RelStr(# f,iP #); A4: dom f = Seg (len f) by FINSEQ_1:def_3; A5: RelStr(# f,iP #) is antisymmetric proof let x, y be set ; :: according to RELAT_2:def_4,ORDERS_2:def_4 ::_thesis: ( not x in the carrier of RelStr(# f,iP #) or not y in the carrier of RelStr(# f,iP #) or not [x,y] in the InternalRel of RelStr(# f,iP #) or not [y,x] in the InternalRel of RelStr(# f,iP #) or x = y ) assume that x in the carrier of RelStr(# f,iP #) and y in the carrier of RelStr(# f,iP #) and A6: [x,y] in the InternalRel of RelStr(# f,iP #) and A7: [y,x] in the InternalRel of RelStr(# f,iP #) ; ::_thesis: x = y consider i, j being Nat, r, s being real number such that A8: x = [i,r] and A9: y = [j,s] and A10: ( i < j & r < s ) by A6, A3; consider j1, i1 being Nat, s1, r1 being real number such that A11: y = [j1,s1] and A12: x = [i1,r1] and A13: ( j1 < i1 & s1 < r1 ) by A7, A3; ( i = i1 & j = j1 ) by A8, A9, A11, A12, XTUPLE_0:1; hence x = y by A10, A13; ::_thesis: verum end; RelStr(# f,iP #) is transitive proof let x, y, z be set ; :: according to RELAT_2:def_8,ORDERS_2:def_3 ::_thesis: ( not x in the carrier of RelStr(# f,iP #) or not y in the carrier of RelStr(# f,iP #) or not z in the carrier of RelStr(# f,iP #) or not [x,y] in the InternalRel of RelStr(# f,iP #) or not [y,z] in the InternalRel of RelStr(# f,iP #) or [x,z] in the InternalRel of RelStr(# f,iP #) ) assume that A14: x in the carrier of RelStr(# f,iP #) and y in the carrier of RelStr(# f,iP #) and A15: z in the carrier of RelStr(# f,iP #) and A16: [x,y] in the InternalRel of RelStr(# f,iP #) and A17: [y,z] in the InternalRel of RelStr(# f,iP #) ; ::_thesis: [x,z] in the InternalRel of RelStr(# f,iP #) consider ix, jy being Nat, rx, sy being real number such that A18: x = [ix,rx] and A19: y = [jy,sy] and A20: ( ix < jy & rx < sy ) by A16, A3; consider iy, jz being Nat, ry, sz being real number such that A21: y = [iy,ry] and A22: z = [jz,sz] and A23: ( iy < jz & ry < sz ) by A17, A3; ( jy = iy & sy = ry ) by A19, A21, XTUPLE_0:1; then ( ix < jz & rx < sz ) by A20, A23, XXREAL_0:2; hence [x,z] in the InternalRel of RelStr(# f,iP #) by A18, A22, A14, A15, A3; ::_thesis: verum end; then reconsider P = RelStr(# f,iP #) as finite transitive antisymmetric RelStr by A5; A24: card P = card f ; percases ( ex C being Clique of P st card C >= n + 1 or ex A being StableSet of P st card A >= n + 1 ) by A24, A1, Th55; suppose ex C being Clique of P st card C >= n + 1 ; ::_thesis: ex g being real-valued FinSubsequence st ( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) ) then consider C being Clique of P such that A25: card C >= n + 1 ; set g = C; reconsider g = C as Subset of f ; reconsider g = g as Function ; dom g c= Seg (len f) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom g or x in Seg (len f) ) assume x in dom g ; ::_thesis: x in Seg (len f) 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 x in Seg (len f) by FINSEQ_1:def_3; ::_thesis: verum end; then reconsider g = g as FinSubsequence by FINSEQ_1:def_12; reconsider g = g as real-valued FinSubsequence ; take g ; ::_thesis: ( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) ) thus g c= f ; ::_thesis: ( card g >= n + 1 & ( g is increasing or g is decreasing ) ) thus card g >= n + 1 by A25; ::_thesis: ( g is increasing or g is decreasing ) g is increasing proof let e1, e2 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: ( not e1 in dom g or not e2 in dom g or e2 <= e1 or not g . e2 <= g . e1 ) assume that A27: e1 in dom g and A28: e2 in dom g and A29: e1 < e2 ; ::_thesis: not g . e2 <= g . e1 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; percases ( p1 <= p2 or p2 <= p1 ) by A30, A31, A32, Th6; suppose p1 <= p2 ; ::_thesis: not g . e2 <= g . e1 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 < j & r < s ) by A3; ( j = e2 & s = g . e2 ) by A34, XTUPLE_0:1; hence g . e1 < g . e2 by A35, A33, XTUPLE_0:1; ::_thesis: verum end; suppose p2 <= p1 ; ::_thesis: not g . e2 <= g . e1 then [p2,p1] in iP by ORDERS_2:def_5; then consider i, j being Nat, r, s being real number such that A36: p2 = [i,r] and A37: p1 = [j,s] and A38: ( i < j & r < s ) by A3; ( i = e2 & j = e1 ) by A36, A37, XTUPLE_0:1; hence g . e1 < g . e2 by A29, A38; ::_thesis: verum end; end; end; hence ( g is increasing or g is decreasing ) ; ::_thesis: verum end; suppose ex A being StableSet of P st card A >= n + 1 ; ::_thesis: ex g being real-valued FinSubsequence st ( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) ) then consider A being StableSet of P such that A39: card A >= n + 1 ; set g = A; reconsider g = A as Subset of f ; reconsider g = g as Function ; A40: dom g c= Seg (len f) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom g or x in Seg (len f) ) assume x in dom g ; ::_thesis: x in Seg (len f) 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 x in Seg (len f) by FINSEQ_1:def_3; ::_thesis: verum end; then reconsider g = g as FinSubsequence by FINSEQ_1:def_12; reconsider g = g as real-valued FinSubsequence ; take g ; ::_thesis: ( g c= f & card g >= n + 1 & ( g is increasing or g is decreasing ) ) thus g c= f ; ::_thesis: ( card g >= n + 1 & ( g is increasing or g is decreasing ) ) thus card g >= n + 1 by A39; ::_thesis: ( g is increasing or g is decreasing ) g is decreasing proof let e1, e2 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: ( not e1 in dom g or not e2 in dom g or e2 <= e1 or not g . e1 <= g . e2 ) assume that A42: e1 in dom g and A43: e2 in dom g and A44: e1 < e2 ; ::_thesis: not g . e1 <= g . 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] ) ; percases ( g . e1 < g . e2 or g . e1 > g . e2 ) by A48, XXREAL_0:1; suppose g . e1 < g . e2 ; ::_thesis: not 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; ::_thesis: verum end; suppose g . e1 > g . e2 ; ::_thesis: not g . e1 <= g . e2 hence not g . e1 <= g . e2 ; ::_thesis: verum end; end; end; hence ( g is increasing or g is decreasing ) ; ::_thesis: verum end; end; end;