:: MYCIELSK semantic presentation begin begin theorem :: MYCIELSK:1 for x, y, z being real number st 0 <= x holds x * (y -' z) = (x * y) -' (x * z) proof let x, y, z be real number ; ::_thesis: ( 0 <= x implies x * (y -' z) = (x * y) -' (x * z) ) assume A1: x >= 0 ; ::_thesis: x * (y -' z) = (x * y) -' (x * z) percases ( y - z >= 0 or y - z < 0 ) ; supposeA2: y - z >= 0 ; ::_thesis: x * (y -' z) = (x * y) -' (x * z) A3: x * (y - z) >= 0 by A1, A2; thus x * (y -' z) = x * (y - z) by A2, XREAL_0:def_2 .= (x * y) - (x * z) .= (x * y) -' (x * z) by A3, XREAL_0:def_2 ; ::_thesis: verum end; supposeA4: y - z < 0 ; ::_thesis: x * (y -' z) = (x * y) -' (x * z) percases ( x = 0 or x > 0 ) by A1; supposeA5: x = 0 ; ::_thesis: x * (y -' z) = (x * y) -' (x * z) thus x * (y -' z) = (x * y) -' (x * z) by A5, XREAL_1:232; ::_thesis: verum end; supposeA6: x > 0 ; ::_thesis: x * (y -' z) = (x * y) -' (x * z) x * (y - z) < 0 by A4, A6; then A7: (x * y) - (x * z) < 0 ; thus x * (y -' z) = x * 0 by A4, XREAL_0:def_2 .= (x * y) -' (x * z) by A7, XREAL_0:def_2 ; ::_thesis: verum end; end; end; end; end; theorem Th2: :: MYCIELSK:2 for x, y, z being Nat holds ( x in y \ z iff ( z <= x & x < y ) ) proof let x, y, z be Nat; ::_thesis: ( x in y \ z iff ( z <= x & x < y ) ) hereby ::_thesis: ( z <= x & x < y implies x in y \ z ) assume A1: x in y \ z ; ::_thesis: ( z <= x & x < y ) not x in z by A1, XBOOLE_0:def_5; hence z <= x by NAT_1:44; ::_thesis: x < y thus x < y by A1, NAT_1:44; ::_thesis: verum end; assume ( z <= x & x < y ) ; ::_thesis: x in y \ z then ( x in y & not x in z ) by NAT_1:44; hence x in y \ z by XBOOLE_0:def_5; ::_thesis: verum end; theorem Th3: :: MYCIELSK:3 for A, B, C, D, E, X being set st ( X c= A or X c= B or X c= C or X c= D or X c= E ) holds X c= (((A \/ B) \/ C) \/ D) \/ E proof let A, B, C, D, E, X be set ; ::_thesis: ( ( X c= A or X c= B or X c= C or X c= D or X c= E ) implies X c= (((A \/ B) \/ C) \/ D) \/ E ) assume A1: ( X c= A or X c= B or X c= C or X c= D or X c= E ) ; ::_thesis: X c= (((A \/ B) \/ C) \/ D) \/ E percases ( X c= A or X c= B or X c= C or X c= D or X c= E ) by A1; suppose X c= A ; ::_thesis: X c= (((A \/ B) \/ C) \/ D) \/ E then X c= A \/ B by XBOOLE_1:10; then X c= (A \/ B) \/ C by XBOOLE_1:10; then X c= ((A \/ B) \/ C) \/ D by XBOOLE_1:10; hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; ::_thesis: verum end; suppose X c= B ; ::_thesis: X c= (((A \/ B) \/ C) \/ D) \/ E then X c= A \/ B by XBOOLE_1:10; then X c= (A \/ B) \/ C by XBOOLE_1:10; then X c= ((A \/ B) \/ C) \/ D by XBOOLE_1:10; hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; ::_thesis: verum end; suppose X c= C ; ::_thesis: X c= (((A \/ B) \/ C) \/ D) \/ E then X c= (A \/ B) \/ C by XBOOLE_1:10; then X c= ((A \/ B) \/ C) \/ D by XBOOLE_1:10; hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; ::_thesis: verum end; suppose X c= D ; ::_thesis: X c= (((A \/ B) \/ C) \/ D) \/ E then X c= ((A \/ B) \/ C) \/ D by XBOOLE_1:10; hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; ::_thesis: verum end; suppose X c= E ; ::_thesis: X c= (((A \/ B) \/ C) \/ D) \/ E hence X c= (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_1:10; ::_thesis: verum end; end; end; theorem Th4: :: MYCIELSK:4 for A, B, C, D, E, x being set holds ( x in (((A \/ B) \/ C) \/ D) \/ E iff ( x in A or x in B or x in C or x in D or x in E ) ) proof let A, B, C, D, E, x be set ; ::_thesis: ( x in (((A \/ B) \/ C) \/ D) \/ E iff ( x in A or x in B or x in C or x in D or x in E ) ) hereby ::_thesis: ( ( x in A or x in B or x in C or x in D or x in E ) implies x in (((A \/ B) \/ C) \/ D) \/ E ) assume x in (((A \/ B) \/ C) \/ D) \/ E ; ::_thesis: ( x in A or x in B or x in C or x in D or x in E ) then ( x in ((A \/ B) \/ C) \/ D or x in E ) by XBOOLE_0:def_3; then ( x in (A \/ B) \/ C or x in D or x in E ) by XBOOLE_0:def_3; then ( x in A \/ B or x in C or x in D or x in E ) by XBOOLE_0:def_3; hence ( x in A or x in B or x in C or x in D or x in E ) by XBOOLE_0:def_3; ::_thesis: verum end; assume A1: ( x in A or x in B or x in C or x in D or x in E ) ; ::_thesis: x in (((A \/ B) \/ C) \/ D) \/ E percases ( x in A or x in B or x in C or x in D or x in E ) by A1; suppose x in A ; ::_thesis: x in (((A \/ B) \/ C) \/ D) \/ E then x in A \/ B by XBOOLE_0:def_3; then x in (A \/ B) \/ C by XBOOLE_0:def_3; then x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def_3; hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def_3; ::_thesis: verum end; suppose x in B ; ::_thesis: x in (((A \/ B) \/ C) \/ D) \/ E then x in A \/ B by XBOOLE_0:def_3; then x in (A \/ B) \/ C by XBOOLE_0:def_3; then x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def_3; hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def_3; ::_thesis: verum end; suppose x in C ; ::_thesis: x in (((A \/ B) \/ C) \/ D) \/ E then x in (A \/ B) \/ C by XBOOLE_0:def_3; then x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def_3; hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def_3; ::_thesis: verum end; suppose x in D ; ::_thesis: x in (((A \/ B) \/ C) \/ D) \/ E then x in ((A \/ B) \/ C) \/ D by XBOOLE_0:def_3; hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def_3; ::_thesis: verum end; suppose x in E ; ::_thesis: x in (((A \/ B) \/ C) \/ D) \/ E hence x in (((A \/ B) \/ C) \/ D) \/ E by XBOOLE_0:def_3; ::_thesis: verum end; end; end; theorem Th5: :: MYCIELSK:5 for R being symmetric RelStr for x, y being set st x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R holds [y,x] in the InternalRel of R proof let R be symmetric RelStr ; ::_thesis: for x, y being set st x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R holds [y,x] in the InternalRel of R let x, y be set ; ::_thesis: ( x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R implies [y,x] in the InternalRel of R ) set cR = the carrier of R; set iR = the InternalRel of R; assume that A1: x in the carrier of R and A2: y in the carrier of R and A3: [x,y] in the InternalRel of R ; ::_thesis: [y,x] in the InternalRel of R the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def_3; hence [y,x] in the InternalRel of R by A1, A2, A3, RELAT_2:def_3; ::_thesis: verum end; theorem Th6: :: MYCIELSK:6 for R being symmetric RelStr for x, y being Element of R st x <= y holds y <= x proof let R be symmetric RelStr ; ::_thesis: for x, y being Element of R st x <= y holds y <= x let x, y be Element of R; ::_thesis: ( x <= y implies y <= x ) assume A1: x <= y ; ::_thesis: y <= x set cR = the carrier of R; set iR = the InternalRel of R; A2: the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def_3; A3: [x,y] in the InternalRel of R by A1, ORDERS_2:def_5; then ( x in the carrier of R & y in the carrier of R ) by ZFMISC_1:87; then [y,x] in the InternalRel of R by A2, A3, RELAT_2:def_3; hence y <= x by ORDERS_2:def_5; ::_thesis: verum end; begin theorem Th7: :: MYCIELSK:7 for X being set for P being a_partition of X holds card P c= card X proof let X be set ; ::_thesis: for P being a_partition of X holds card P c= card X let P be a_partition of X; ::_thesis: card P c= card X defpred S1[ set , set ] means $2 = choose $1; A1: for e being set st e in P holds ex u being set st S1[e,u] ; consider f being Function such that A2: dom f = P and A3: for e being set st e in P holds S1[e,f . e] from CLASSES1:sch_1(A1); A4: 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 A5: x1 in dom f and A6: x2 in dom f and A7: f . x1 = f . x2 ; ::_thesis: x1 = x2 A8: x1 <> {} by A2, A5, EQREL_1:def_4; A9: x2 <> {} by A2, A6, EQREL_1:def_4; ( f . x1 = choose x1 & f . x2 = choose x2 ) by A5, A6, A2, A3; then x1 meets x2 by A7, A8, A9, XBOOLE_0:3; hence x1 = x2 by A5, A6, A2, EQREL_1:def_4; ::_thesis: verum end; rng f c= X proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in X ) assume y in rng f ; ::_thesis: y in X then consider x being set such that A10: x in dom f and A11: y = f . x by FUNCT_1:def_3; A12: f . x = choose x by A2, A3, A10; x <> {} by A2, A10, EQREL_1:def_4; then f . x in x by A12; hence y in X by A10, A2, A11; ::_thesis: verum end; hence card P c= card X by A2, A4, CARD_1:10; ::_thesis: verum end; definition let X be set ; let P be a_partition of X; let S be Subset of X; funcP | S -> a_partition of S equals :: MYCIELSK:def 1 { (x /\ S) where x is Element of P : x meets S } ; coherence { (x /\ S) where x is Element of P : x meets S } is a_partition of S proof set D = { (x /\ S) where x is Element of P : x meets S } ; A1: { (x /\ S) where x is Element of P : x meets S } c= bool S proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (x /\ S) where x is Element of P : x meets S } or a in bool S ) assume a in { (x /\ S) where x is Element of P : x meets S } ; ::_thesis: a in bool S then consider x being Element of P such that A2: a = x /\ S and x meets S ; a c= S by A2, XBOOLE_1:17; hence a in bool S ; ::_thesis: verum end; A3: union { (x /\ S) where x is Element of P : x meets S } = S proof thus union { (x /\ S) where x is Element of P : x meets S } c= S :: according to XBOOLE_0:def_10 ::_thesis: S c= union { (x /\ S) where x is Element of P : x meets S } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (x /\ S) where x is Element of P : x meets S } or x in S ) assume x in union { (x /\ S) where x is Element of P : x meets S } ; ::_thesis: x in S then consider Y being set such that A4: x in Y and A5: Y in { (x /\ S) where x is Element of P : x meets S } by TARSKI:def_4; thus x in S by A4, A1, A5; ::_thesis: verum end; thus S c= union { (x /\ S) where x is Element of P : x meets S } ::_thesis: verum proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in S or s in union { (x /\ S) where x is Element of P : x meets S } ) assume A6: s in S ; ::_thesis: s in union { (x /\ S) where x is Element of P : x meets S } then s in X ; then s in union P by EQREL_1:def_4; then consider p being set such that A7: s in p and A8: p in P by TARSKI:def_4; p meets S by A7, A6, XBOOLE_0:3; then A9: p /\ S in { (x /\ S) where x is Element of P : x meets S } by A8; s in p /\ S by A7, A6, XBOOLE_0:def_4; hence s in union { (x /\ S) where x is Element of P : x meets S } by A9, TARSKI:def_4; ::_thesis: verum end; end; now__::_thesis:_for_A_being_Subset_of_S_st_A_in__{__(x_/\_S)_where_x_is_Element_of_P_:_x_meets_S__}__holds_ (_A_<>_{}_&_(_for_B_being_Subset_of_S_holds_ (_not_B_in__{__(x_/\_S)_where_x_is_Element_of_P_:_x_meets_S__}__or_A_=_B_or_A_misses_B_)_)_) let A be Subset of S; ::_thesis: ( A in { (x /\ S) where x is Element of P : x meets S } implies ( A <> {} & ( for B being Subset of S holds ( not B in { (x /\ S) where x is Element of P : x meets S } or b2 = b3 or b2 misses b3 ) ) ) ) assume A in { (x /\ S) where x is Element of P : x meets S } ; ::_thesis: ( A <> {} & ( for B being Subset of S holds ( not B in { (x /\ S) where x is Element of P : x meets S } or b2 = b3 or b2 misses b3 ) ) ) then consider x being Element of P such that A10: A = x /\ S and A11: x meets S ; consider z being set such that A12: z in x and A13: z in S by A11, XBOOLE_0:3; reconsider Xp1 = X as non empty set by A13; reconsider Pp1 = P as a_partition of Xp1 ; thus A <> {} by A12, A13, A10, XBOOLE_0:def_4; ::_thesis: for B being Subset of S holds ( not B in { (x /\ S) where x is Element of P : x meets S } or b2 = b3 or b2 misses b3 ) let B be Subset of S; ::_thesis: ( not B in { (x /\ S) where x is Element of P : x meets S } or b1 = b2 or b1 misses b2 ) assume B in { (x /\ S) where x is Element of P : x meets S } ; ::_thesis: ( b1 = b2 or b1 misses b2 ) then consider y being Element of P such that A14: B = y /\ S and y meets S ; A15: ( x in Pp1 & y in Pp1 ) ; percases ( x = y or x misses y ) by A15, EQREL_1:def_4; suppose x = y ; ::_thesis: ( b1 = b2 or b1 misses b2 ) hence ( A = B or A misses B ) by A10, A14; ::_thesis: verum end; suppose x misses y ; ::_thesis: ( b1 = b2 or b1 misses b2 ) hence ( A = B or A misses B ) by A10, A14, XBOOLE_1:76; ::_thesis: verum end; end; end; hence { (x /\ S) where x is Element of P : x meets S } is a_partition of S by A1, A3, EQREL_1:def_4; ::_thesis: verum end; end; :: deftheorem defines | MYCIELSK:def_1_:_ for X being set for P being a_partition of X for S being Subset of X holds P | S = { (x /\ S) where x is Element of P : x meets S } ; registration let X be set ; cluster finite V89() for a_partition of X; existence ex b1 being a_partition of X st b1 is finite proof percases ( X = {} or X <> {} ) ; suppose X = {} ; ::_thesis: ex b1 being a_partition of X st b1 is finite hence ex b1 being a_partition of X st b1 is finite by EQREL_1:45; ::_thesis: verum end; suppose X <> {} ; ::_thesis: ex b1 being a_partition of X st b1 is finite then {X} is a_partition of X by EQREL_1:39; hence ex b1 being a_partition of X st b1 is finite ; ::_thesis: verum end; end; end; end; registration let X be set ; let P be finite a_partition of X; let S be Subset of X; clusterP | S -> finite ; coherence P | S is finite proof defpred S1[ set , set ] means P = X /\ S; A1: for e being set st e in P holds ex u being set st S1[e,u] ; consider f being Function such that A2: dom f = P and A3: for e being set st e in P holds S1[e,f . e] from CLASSES1:sch_1(A1); A4: rng f is finite by A2, FINSET_1:8; P | S c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P | S or x in rng f ) assume x in P | S ; ::_thesis: x in rng f then consider xx being Element of P such that A5: x = xx /\ S and A6: xx meets S ; consider y being set such that y in xx and A7: y in S by A6, XBOOLE_0:3; reconsider Xp1 = X as non empty set by A7; A8: P is a_partition of Xp1 ; then x = f . xx by A3, A5; hence x in rng f by A8, A2, FUNCT_1:def_3; ::_thesis: verum end; hence P | S is finite by A4; ::_thesis: verum end; end; theorem Th8: :: MYCIELSK:8 for X being set for P being finite a_partition of X for S being Subset of X holds card (P | S) <= card P proof let X be set ; ::_thesis: for P being finite a_partition of X for S being Subset of X holds card (P | S) <= card P let P be finite a_partition of X; ::_thesis: for S being Subset of X holds card (P | S) <= card P let S be Subset of X; ::_thesis: card (P | S) <= card P percases ( X = {} or X <> {} ) ; supposeA1: X = {} ; ::_thesis: card (P | S) <= card P then A2: P = {} by EQREL_1:32; S = {} by A1; hence card (P | S) <= card P by A2, EQREL_1:32; ::_thesis: verum end; suppose X <> {} ; ::_thesis: card (P | S) <= card P then reconsider Pp1 = P as non empty finite set ; defpred S1[ set ] means $1 meets S; deffunc H1( set ) -> Element of bool X = $1 /\ S; A3: P | S = { H1(x) where x is Element of Pp1 : S1[x] } ; card (P | S) <= card Pp1 from DILWORTH:sch_1(A3); hence card (P | S) <= card P ; ::_thesis: verum end; end; end; theorem Th9: :: MYCIELSK:9 for X being set for P being finite a_partition of X for S being Subset of X holds ( ( for p being set st p in P holds p meets S ) iff card (P | S) = card P ) proof let X be set ; ::_thesis: for P being finite a_partition of X for S being Subset of X holds ( ( for p being set st p in P holds p meets S ) iff card (P | S) = card P ) let P be finite a_partition of X; ::_thesis: for S being Subset of X holds ( ( for p being set st p in P holds p meets S ) iff card (P | S) = card P ) let S be Subset of X; ::_thesis: ( ( for p being set st p in P holds p meets S ) iff card (P | S) = card P ) percases ( X = {} or X <> {} ) ; supposeA1: X = {} ; ::_thesis: ( ( for p being set st p in P holds p meets S ) iff card (P | S) = card P ) hereby ::_thesis: ( card (P | S) = card P implies for p being set st p in P holds p meets S ) assume for p being set st p in P holds p meets S ; ::_thesis: card (P | S) = card P S = {} by A1; hence card (P | S) = {} by CARD_1:27, EQREL_1:32 .= card P by A1, CARD_1:27, EQREL_1:32 ; ::_thesis: verum end; thus ( card (P | S) = card P implies for p being set st p in P holds p meets S ) by A1, EQREL_1:32; ::_thesis: verum end; supposeA2: X <> {} ; ::_thesis: ( ( for p being set st p in P holds p meets S ) iff card (P | S) = card P ) set PS = P | S; reconsider Pp1 = P as non empty finite set by A2; hereby ::_thesis: ( card (P | S) = card P implies for p being set st p in P holds p meets S ) assume A3: for p being set st p in P holds p meets S ; ::_thesis: card (P | S) = card P set p = the Element of P; the Element of P in Pp1 ; then the Element of P meets S by A3; then the Element of P /\ S in P | S ; then reconsider PSp1 = P | S as non empty finite set ; defpred S1[ set , set ] means ( $1 in P & $2 = $1 /\ S ); A4: for x being set st x in P holds ex y being set st ( y in PSp1 & S1[x,y] ) proof let x be set ; ::_thesis: ( x in P implies ex y being set st ( y in PSp1 & S1[x,y] ) ) assume A5: x in P ; ::_thesis: ex y being set st ( y in PSp1 & S1[x,y] ) take x /\ S ; ::_thesis: ( x /\ S in PSp1 & S1[x,x /\ S] ) x meets S by A5, A3; hence ( x /\ S in PSp1 & S1[x,x /\ S] ) by A5; ::_thesis: verum end; consider f being Function of P,PSp1 such that A6: for x being set st x in P holds S1[x,f . x] from FUNCT_2:sch_1(A4); now__::_thesis:_for_x1,_x2_being_set_st_x1_in_P_&_x2_in_P_&_f_._x1_=_f_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in P & x2 in P & f . x1 = f . x2 implies x1 = x2 ) assume that A7: x1 in P and A8: x2 in P and A9: f . x1 = f . x2 ; ::_thesis: x1 = x2 A10: f . x1 = x1 /\ S by A7, A6; A11: f . x2 = x2 /\ S by A8, A6; x1 meets S by A7, A3; then f . x1 in P | S by A10, A7; then f . x1 <> {} by EQREL_1:def_4; then consider x being set such that A12: x in f . x1 by XBOOLE_0:def_1; ( x in x1 & x in x2 ) by A12, A9, A10, A11, XBOOLE_0:def_4; then x1 meets x2 by XBOOLE_0:3; hence x1 = x2 by A7, A8, EQREL_1:def_4; ::_thesis: verum end; then A13: f is one-to-one by FUNCT_2:19; rng f = PSp1 proof thus rng f c= PSp1 :: according to XBOOLE_0:def_10 ::_thesis: PSp1 c= rng f proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in PSp1 ) assume y in rng f ; ::_thesis: y in PSp1 then consider x being set such that A14: x in P and A15: f . x = y by FUNCT_2:11; x meets S by A3, A14; then x /\ S in P | S by A14; hence y in PSp1 by A15, A14, A6; ::_thesis: verum end; thus PSp1 c= rng f ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in PSp1 or y in rng f ) assume y in PSp1 ; ::_thesis: y in rng f then consider p being Element of P such that A16: y = p /\ S and p meets S ; A17: p in Pp1 ; then f . p = p /\ S by A6; hence y in rng f by A16, A17, FUNCT_2:4; ::_thesis: verum end; end; then f is onto by FUNCT_2:def_3; hence card (P | S) = card P by A13, EULER_1:11; ::_thesis: verum end; assume A18: card (P | S) = card P ; ::_thesis: for p being set st p in P holds p meets S defpred S1[ set , set ] means ( $1 in P | S & $2 in Pp1 & $1 = $2 /\ S ); A19: for x being set st x in P | S holds ex y being set st ( y in Pp1 & S1[x,y] ) proof let x be set ; ::_thesis: ( x in P | S implies ex y being set st ( y in Pp1 & S1[x,y] ) ) assume A20: x in P | S ; ::_thesis: ex y being set st ( y in Pp1 & S1[x,y] ) then consider p being Element of P such that A21: x = p /\ S and p meets S ; take p ; ::_thesis: ( p in Pp1 & S1[x,p] ) thus ( p in Pp1 & S1[x,p] ) by A20, A21; ::_thesis: verum end; consider f being Function of (P | S),Pp1 such that A22: for x being set st x in P | S holds S1[x,f . x] from FUNCT_2:sch_1(A19); A23: 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 A24: x1 in dom f and A25: x2 in dom f and A26: f . x1 = f . x2 ; ::_thesis: x1 = x2 x1 = (f . x1) /\ S by A24, A22; hence x1 = x2 by A26, A25, A22; ::_thesis: verum end; A27: rng f = P by A18, A23, FINSEQ_4:63; let p be set ; ::_thesis: ( p in P implies p meets S ) assume p in P ; ::_thesis: p meets S then consider ps being set such that A28: ps in dom f and A29: p = f . ps by A27, FUNCT_1:def_3; A30: dom f = P | S by FUNCT_2:def_1; A31: ps = p /\ S by A29, A28, A22; not ps is empty by A28, A30, EQREL_1:def_4; then ex x being set st x in ps by XBOOLE_0:def_1; hence p meets S by A31, XBOOLE_0:4; ::_thesis: verum end; end; end; theorem Th10: :: MYCIELSK:10 for R being RelStr for C being Coloring of R for S being Subset of R holds C | S is Coloring of (subrelstr S) proof let R be RelStr ; ::_thesis: for C being Coloring of R for S being Subset of R holds C | S is Coloring of (subrelstr S) let C be Coloring of R; ::_thesis: for S being Subset of R holds C | S is Coloring of (subrelstr S) let S be Subset of R; ::_thesis: C | S is Coloring of (subrelstr S) set sS = subrelstr S; A1: the carrier of (subrelstr S) = S by YELLOW_0:def_15; now__::_thesis:_for_x_being_set_st_x_in_C_|_S_holds_ x_is_StableSet_of_(subrelstr_S) let x be set ; ::_thesis: ( x in C | S implies x is StableSet of (subrelstr S) ) assume x in C | S ; ::_thesis: x is StableSet of (subrelstr S) then consider c being Element of C such that A2: x = c /\ S and A3: c meets S ; consider z being set such that z in c and A4: z in S by A3, XBOOLE_0:3; A5: not subrelstr S is empty by A4, YELLOW_0:def_15; A6: not R is empty by A4; reconsider Rp1 = R as non empty RelStr by A4; reconsider xp1 = x as Subset of (subrelstr S) by A1, A2, XBOOLE_1:17; xp1 is stable proof let a, b be Element of (subrelstr S); :: according to DILWORTH:def_2 ::_thesis: ( not a in xp1 or not b in xp1 or a = b or ( not a <= b & not b <= a ) ) assume that A7: a in xp1 and A8: b in xp1 and A9: a <> b ; ::_thesis: ( not a <= b & not b <= a ) A10: ( a in c & b in c ) by A7, A8, A2, XBOOLE_0:def_4; reconsider ap1 = a, bp1 = b as Element of R by A5, A6, YELLOW_0:58; A11: C is Coloring of Rp1 ; then c in C ; then reconsider cp1 = c as Subset of R ; A12: cp1 is stable by A11, DILWORTH:def_12; assume ( a <= b or b <= a ) ; ::_thesis: contradiction then ( ap1 <= bp1 or bp1 <= ap1 ) by YELLOW_0:59; hence contradiction by A9, A10, A12, DILWORTH:def_2; ::_thesis: verum end; hence x is StableSet of (subrelstr S) ; ::_thesis: verum end; hence C | S is Coloring of (subrelstr S) by A1, DILWORTH:def_12; ::_thesis: verum end; begin definition let R be RelStr ; attrR is with_finite_chromatic# means :Def2: :: MYCIELSK:def 2 ex C being Coloring of R st C is finite ; end; :: deftheorem Def2 defines with_finite_chromatic# MYCIELSK:def_2_:_ for R being RelStr holds ( R is with_finite_chromatic# iff ex C being Coloring of R st C is finite ); registration cluster with_finite_chromatic# for RelStr ; existence ex b1 being RelStr st b1 is with_finite_chromatic# proof take R = the empty RelStr ; ::_thesis: R is with_finite_chromatic# reconsider S = {} as a_partition of the carrier of R by EQREL_1:45; take S ; :: according to MYCIELSK:def_2 ::_thesis: S is finite thus S is finite ; ::_thesis: verum end; end; registration cluster finite -> with_finite_chromatic# for RelStr ; coherence for b1 being RelStr st b1 is finite holds b1 is with_finite_chromatic# proof let R be RelStr ; ::_thesis: ( R is finite implies R is with_finite_chromatic# ) set cR = the carrier of R; assume A1: R is finite ; ::_thesis: R is with_finite_chromatic# percases ( R is empty or not R is empty ) ; suppose R is empty ; ::_thesis: R is with_finite_chromatic# then reconsider S = {} as a_partition of the carrier of R by EQREL_1:45; for x being set st x in S holds x is StableSet of R ; then reconsider S = S as Coloring of R by DILWORTH:def_12; take S ; :: according to MYCIELSK:def_2 ::_thesis: S is finite thus S is finite ; ::_thesis: verum end; supposeA2: not R is empty ; ::_thesis: R is with_finite_chromatic# reconsider cRp1 = the carrier of R as non empty finite set by A2, A1; set S = SmallestPartition the carrier of R; deffunc H1( set ) -> set = {c1}; defpred S1[ set ] means verum; A3: SmallestPartition the carrier of R = { H1(x) where x is Element of cRp1 : S1[x] } by EQREL_1:37; A4: { H1(x) where x is Element of cRp1 : S1[x] } is finite from PRE_CIRC:sch_1(); now__::_thesis:_for_z_being_set_st_z_in_SmallestPartition_the_carrier_of_R_holds_ z_is_StableSet_of_R let z be set ; ::_thesis: ( z in SmallestPartition the carrier of R implies z is StableSet of R ) assume z in SmallestPartition the carrier of R ; ::_thesis: z is StableSet of R then ex x being Element of the carrier of R st z = {x} by A3; hence z is StableSet of R by A2, SUBSET_1:33; ::_thesis: verum end; then reconsider S = SmallestPartition the carrier of R as Coloring of R by DILWORTH:def_12; take S ; :: according to MYCIELSK:def_2 ::_thesis: S is finite thus S is finite by A4; ::_thesis: verum end; end; end; end; registration let R be with_finite_chromatic# RelStr ; cluster finite V89() StableSet-wise for a_partition of the carrier of R; existence ex b1 being Coloring of R st b1 is finite by Def2; end; registration let R be with_finite_chromatic# RelStr ; let S be Subset of R; cluster subrelstr S -> with_finite_chromatic# ; coherence subrelstr S is with_finite_chromatic# proof set sS = subrelstr S; consider C being Coloring of R such that A1: C is finite by Def2; A2: the carrier of (subrelstr S) = S by YELLOW_0:def_15; reconsider CS = C | S as a_partition of S ; for x being set st x in CS holds x is StableSet of (subrelstr S) proof let x be set ; ::_thesis: ( x in CS implies x is StableSet of (subrelstr S) ) assume x in CS ; ::_thesis: x is StableSet of (subrelstr S) then consider X being Element of C such that A3: x = X /\ S and A4: X meets S ; ex y being set st ( y in X & y in S ) by A4, XBOOLE_0:3; then X is StableSet of R by DILWORTH:def_12; hence x is StableSet of (subrelstr S) by A3, DILWORTH:31; ::_thesis: verum end; then CS is Coloring of (subrelstr S) by A2, DILWORTH:def_12; hence subrelstr S is with_finite_chromatic# by A1, Def2; ::_thesis: verum end; end; definition let R be with_finite_chromatic# RelStr ; func chromatic# R -> Nat means :Def3: :: MYCIELSK:def 3 ( ex C being finite Coloring of R st card C = it & ( for C being finite Coloring of R holds it <= card C ) ); existence ex b1 being Nat st ( ex C being finite Coloring of R st card C = b1 & ( for C being finite Coloring of R holds b1 <= card C ) ) proof defpred S1[ Nat] means ex C being finite Coloring of R st card C = $1; consider C being Coloring of R such that A1: C is finite by Def2; card C = card C ; then A2: ex k being Nat st S1[k] by A1; consider n being Nat such that A3: S1[n] and A4: for k being Nat st S1[k] holds n <= k from NAT_1:sch_5(A2); take n ; ::_thesis: ( ex C being finite Coloring of R st card C = n & ( for C being finite Coloring of R holds n <= card C ) ) thus ex C being finite Coloring of R st card C = n by A3; ::_thesis: for C being finite Coloring of R holds n <= card C let C be finite Coloring of R; ::_thesis: n <= card C thus n <= card C by A4; ::_thesis: verum end; uniqueness for b1, b2 being Nat st ex C being finite Coloring of R st card C = b1 & ( for C being finite Coloring of R holds b1 <= card C ) & ex C being finite Coloring of R st card C = b2 & ( for C being finite Coloring of R holds b2 <= card C ) holds b1 = b2 proof let it1, it2 be Nat; ::_thesis: ( ex C being finite Coloring of R st card C = it1 & ( for C being finite Coloring of R holds it1 <= card C ) & ex C being finite Coloring of R st card C = it2 & ( for C being finite Coloring of R holds it2 <= card C ) implies it1 = it2 ) assume that A5: ex C being finite Coloring of R st card C = it1 and A6: for C being finite Coloring of R holds it1 <= card C and A7: ex C being finite Coloring of R st card C = it2 and A8: for C being finite Coloring of R holds it2 <= card C ; ::_thesis: it1 = it2 consider C1 being finite Coloring of R such that A9: card C1 = it1 by A5; consider C2 being finite Coloring of R such that A10: card C2 = it2 by A7; ( it1 <= card C2 & it2 <= card C1 ) by A6, A8; hence it1 = it2 by A9, A10, XXREAL_0:1; ::_thesis: verum end; end; :: deftheorem Def3 defines chromatic# MYCIELSK:def_3_:_ for R being with_finite_chromatic# RelStr for b2 being Nat holds ( b2 = chromatic# R iff ( ex C being finite Coloring of R st card C = b2 & ( for C being finite Coloring of R holds b2 <= card C ) ) ); registration let R be empty RelStr ; cluster chromatic# R -> empty ; coherence chromatic# R is empty proof consider C being finite Coloring of R such that A1: card C = chromatic# R by Def3; C is empty by EQREL_1:32; hence chromatic# R is empty by A1; ::_thesis: verum end; end; registration let R be non empty with_finite_chromatic# RelStr ; cluster chromatic# R -> positive ; coherence chromatic# R is positive proof ex C being finite Coloring of R st card C = chromatic# R by Def3; hence chromatic# R is positive ; ::_thesis: verum end; end; definition let R be RelStr ; attrR is with_finite_cliquecover# means :Def4: :: MYCIELSK:def 4 ex C being Clique-partition of R st C is finite ; end; :: deftheorem Def4 defines with_finite_cliquecover# MYCIELSK:def_4_:_ for R being RelStr holds ( R is with_finite_cliquecover# iff ex C being Clique-partition of R st C is finite ); registration cluster with_finite_cliquecover# for RelStr ; existence ex b1 being RelStr st b1 is with_finite_cliquecover# proof take R = the empty RelStr ; ::_thesis: R is with_finite_cliquecover# reconsider S = {} as a_partition of the carrier of R by EQREL_1:45; reconsider S = S as Clique-partition of R ; take S ; :: according to MYCIELSK:def_4 ::_thesis: S is finite thus S is finite ; ::_thesis: verum end; end; registration cluster finite -> with_finite_cliquecover# for RelStr ; coherence for b1 being RelStr st b1 is finite holds b1 is with_finite_cliquecover# proof let R be RelStr ; ::_thesis: ( R is finite implies R is with_finite_cliquecover# ) set cR = the carrier of R; assume A1: R is finite ; ::_thesis: R is with_finite_cliquecover# percases ( R is empty or not R is empty ) ; suppose R is empty ; ::_thesis: R is with_finite_cliquecover# then reconsider S = {} as a_partition of the carrier of R by EQREL_1:45; for x being set st x in S holds x is Clique of R ; then reconsider S = S as Clique-partition of R by DILWORTH:def_11; take S ; :: according to MYCIELSK:def_4 ::_thesis: S is finite thus S is finite ; ::_thesis: verum end; supposeA2: not R is empty ; ::_thesis: R is with_finite_cliquecover# reconsider cRp1 = the carrier of R as non empty finite set by A2, A1; set S = SmallestPartition the carrier of R; deffunc H1( set ) -> set = {c1}; defpred S1[ set ] means verum; A3: SmallestPartition the carrier of R = { H1(x) where x is Element of cRp1 : S1[x] } by EQREL_1:37; A4: { H1(x) where x is Element of cRp1 : S1[x] } is finite from PRE_CIRC:sch_1(); now__::_thesis:_for_z_being_set_st_z_in_SmallestPartition_the_carrier_of_R_holds_ z_is_Clique_of_R let z be set ; ::_thesis: ( z in SmallestPartition the carrier of R implies z is Clique of R ) assume A5: z in SmallestPartition the carrier of R ; ::_thesis: z is Clique of R ex x being Element of the carrier of R st z = {x} by A5, A3; hence z is Clique of R by A2, SUBSET_1:33; ::_thesis: verum end; then reconsider S = SmallestPartition the carrier of R as Clique-partition of R by DILWORTH:def_11; take S ; :: according to MYCIELSK:def_4 ::_thesis: S is finite thus S is finite by A4; ::_thesis: verum end; end; end; end; registration let R be with_finite_cliquecover# RelStr ; cluster finite V89() Clique-wise for a_partition of the carrier of R; existence ex b1 being Clique-partition of R st b1 is finite by Def4; end; registration let R be with_finite_cliquecover# RelStr ; let S be Subset of R; cluster subrelstr S -> with_finite_cliquecover# ; coherence subrelstr S is with_finite_cliquecover# proof set sS = subrelstr S; consider C being Clique-partition of R such that A1: C is finite by Def4; A2: the carrier of (subrelstr S) = S by YELLOW_0:def_15; reconsider CS = C | S as a_partition of S ; for x being set st x in CS holds x is Clique of (subrelstr S) proof let x be set ; ::_thesis: ( x in CS implies x is Clique of (subrelstr S) ) assume x in CS ; ::_thesis: x is Clique of (subrelstr S) then consider X being Element of C such that A3: x = X /\ S and A4: X meets S ; ex y being set st ( y in X & y in S ) by A4, XBOOLE_0:3; then X is Clique of R by DILWORTH:def_11; hence x is Clique of (subrelstr S) by A3, DILWORTH:29; ::_thesis: verum end; then CS is Clique-partition of (subrelstr S) by A2, DILWORTH:def_11; hence subrelstr S is with_finite_cliquecover# by A1, Def4; ::_thesis: verum end; end; definition let R be with_finite_cliquecover# RelStr ; func cliquecover# R -> Nat means :Def5: :: MYCIELSK:def 5 ( ex C being finite Clique-partition of R st card C = it & ( for C being finite Clique-partition of R holds it <= card C ) ); existence ex b1 being Nat st ( ex C being finite Clique-partition of R st card C = b1 & ( for C being finite Clique-partition of R holds b1 <= card C ) ) proof defpred S1[ Nat] means ex C being finite Clique-partition of R st card C = $1; consider C being Clique-partition of R such that A1: C is finite by Def4; card C = card C ; then A2: ex k being Nat st S1[k] by A1; consider n being Nat such that A3: S1[n] and A4: for k being Nat st S1[k] holds n <= k from NAT_1:sch_5(A2); take n ; ::_thesis: ( ex C being finite Clique-partition of R st card C = n & ( for C being finite Clique-partition of R holds n <= card C ) ) thus ex C being finite Clique-partition of R st card C = n by A3; ::_thesis: for C being finite Clique-partition of R holds n <= card C let C be finite Clique-partition of R; ::_thesis: n <= card C thus n <= card C by A4; ::_thesis: verum end; uniqueness for b1, b2 being Nat st ex C being finite Clique-partition of R st card C = b1 & ( for C being finite Clique-partition of R holds b1 <= card C ) & ex C being finite Clique-partition of R st card C = b2 & ( for C being finite Clique-partition of R holds b2 <= card C ) holds b1 = b2 proof let it1, it2 be Nat; ::_thesis: ( ex C being finite Clique-partition of R st card C = it1 & ( for C being finite Clique-partition of R holds it1 <= card C ) & ex C being finite Clique-partition of R st card C = it2 & ( for C being finite Clique-partition of R holds it2 <= card C ) implies it1 = it2 ) assume that A5: ex C being finite Clique-partition of R st card C = it1 and A6: for C being finite Clique-partition of R holds it1 <= card C and A7: ex C being finite Clique-partition of R st card C = it2 and A8: for C being finite Clique-partition of R holds it2 <= card C ; ::_thesis: it1 = it2 consider C1 being finite Clique-partition of R such that A9: card C1 = it1 by A5; consider C2 being finite Clique-partition of R such that A10: card C2 = it2 by A7; ( it1 <= card C2 & it2 <= card C1 ) by A6, A8; hence it1 = it2 by A9, A10, XXREAL_0:1; ::_thesis: verum end; end; :: deftheorem Def5 defines cliquecover# MYCIELSK:def_5_:_ for R being with_finite_cliquecover# RelStr for b2 being Nat holds ( b2 = cliquecover# R iff ( ex C being finite Clique-partition of R st card C = b2 & ( for C being finite Clique-partition of R holds b2 <= card C ) ) ); registration let R be empty RelStr ; cluster cliquecover# R -> empty ; coherence cliquecover# R is empty proof consider C being finite Clique-partition of R such that A1: card C = cliquecover# R by Def5; C is empty by EQREL_1:32; hence cliquecover# R is empty by A1; ::_thesis: verum end; end; registration let R be non empty with_finite_cliquecover# RelStr ; cluster cliquecover# R -> positive ; coherence cliquecover# R is positive proof consider C being finite Clique-partition of R such that A1: card C = cliquecover# R by Def5; thus cliquecover# R is positive by A1; ::_thesis: verum end; end; theorem Th11: :: MYCIELSK:11 for R being finite RelStr holds clique# R <= card the carrier of R proof let R be finite RelStr ; ::_thesis: clique# R <= card the carrier of R consider C being finite Clique of R such that A1: card C = clique# R by DILWORTH:def_4; card C c= card the carrier of R by CARD_1:11; hence clique# R <= card the carrier of R by A1, NAT_1:39; ::_thesis: verum end; theorem :: MYCIELSK:12 for R being finite RelStr holds stability# R <= card the carrier of R proof let R be finite RelStr ; ::_thesis: stability# R <= card the carrier of R consider C being finite StableSet of R such that A1: card C = stability# R by DILWORTH:def_6; card C c= card the carrier of R by CARD_1:11; hence stability# R <= card the carrier of R by A1, NAT_1:39; ::_thesis: verum end; theorem Th13: :: MYCIELSK:13 for R being finite RelStr holds chromatic# R <= card the carrier of R proof let R be finite RelStr ; ::_thesis: chromatic# R <= card the carrier of R consider C being finite Coloring of R such that A1: card C = chromatic# R by Def3; card C c= card the carrier of R by Th7; hence chromatic# R <= card the carrier of R by A1, NAT_1:39; ::_thesis: verum end; theorem :: MYCIELSK:14 for R being finite RelStr holds cliquecover# R <= card the carrier of R proof let R be finite RelStr ; ::_thesis: cliquecover# R <= card the carrier of R consider C being finite Clique-partition of R such that A1: card C = cliquecover# R by Def5; card C c= card the carrier of R by Th7; hence cliquecover# R <= card the carrier of R by A1, NAT_1:39; ::_thesis: verum end; theorem Th15: :: MYCIELSK:15 for R being with_finite_clique# with_finite_chromatic# RelStr holds clique# R <= chromatic# R proof let P be with_finite_clique# with_finite_chromatic# RelStr ; ::_thesis: clique# P <= chromatic# P assume A1: clique# P > chromatic# P ; ::_thesis: contradiction consider A being Clique of P such that A2: card A = clique# P by DILWORTH:def_4; consider C being finite Coloring of P such that A3: card C = chromatic# P by Def3; ( card (card C) = card C & card (card A) = card A ) ; then A4: card C in card A by A3, A1, A2, NAT_1:41; set cP = the carrier of P; percases ( P is empty or not P is empty ) ; suppose P is empty ; ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; supposeA5: not P is empty ; ::_thesis: contradiction 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 xp1 = x as Element of P ; not the carrier of P is empty by A5; then xp1 in the carrier of P ; then x 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); consider x, y being set such that A11: x in A and A12: y in A and A13: x <> y and A14: f . x = f . y by A5, A4, FINSEQ_4:65; f . x in C by A11, FUNCT_2:5; then A15: f . x is StableSet of P by DILWORTH:def_12; ( x in f . x & y in f . x ) by A14, A11, A12, A10; hence contradiction by A15, A11, A12, A13, DILWORTH:15; ::_thesis: verum end; end; end; theorem :: MYCIELSK:16 for R being with_finite_stability# with_finite_cliquecover# RelStr holds stability# R <= cliquecover# R proof let R be with_finite_stability# with_finite_cliquecover# RelStr ; ::_thesis: stability# R <= cliquecover# R assume A1: stability# R > cliquecover# R ; ::_thesis: contradiction consider A being StableSet of R such that A2: card A = stability# R by DILWORTH:def_6; consider C being finite Clique-partition of R such that A3: card C = cliquecover# R by Def5; ( card (card C) = card C & card (card A) = card A ) ; then A4: card C in card A by A3, 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; supposeA5: not R is empty ; ::_thesis: contradiction 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] ) reconsider xp1 = x as Element of R by A7; not the carrier of R is empty by A5; then xp1 in the carrier of R ; then x 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); consider x, y being set such that A11: x in A and A12: y in A and A13: x <> y and A14: f . x = f . y by A5, A4, FINSEQ_4:65; f . x in C by A11, FUNCT_2:5; then A15: f . x is Clique of R by DILWORTH:def_11; ( x in f . x & y in f . x ) by A14, A11, A12, A10; hence contradiction by A15, A11, A12, A13, DILWORTH:15; ::_thesis: verum end; end; end; begin theorem Th17: :: MYCIELSK:17 for R being RelStr for x, y being Element of R for a, b being Element of (ComplRelStr R) st x = a & y = b & x <= y holds not a <= b proof let R be RelStr ; ::_thesis: for x, y being Element of R for a, b being Element of (ComplRelStr R) st x = a & y = b & x <= y holds not a <= b let x, y be Element of R; ::_thesis: for a, b being Element of (ComplRelStr R) st x = a & y = b & x <= y holds not a <= b let a, b be Element of (ComplRelStr R); ::_thesis: ( x = a & y = b & x <= y implies not a <= b ) assume that A1: x = a and A2: y = b ; ::_thesis: ( not x <= y or not a <= b ) set cR = the carrier of R; set iR = the InternalRel of R; set CR = ComplRelStr R; set iCR = the InternalRel of (ComplRelStr R); A3: the InternalRel of (ComplRelStr R) = ( the InternalRel of R `) \ (id the carrier of R) by NECKLACE:def_8; assume x <= y ; ::_thesis: not a <= b then [x,y] in the InternalRel of R by ORDERS_2:def_5; then not [x,y] in the InternalRel of R ` by XBOOLE_0:def_5; then not [x,y] in the InternalRel of (ComplRelStr R) by A3, XBOOLE_0:def_5; hence not a <= b by A1, A2, ORDERS_2:def_5; ::_thesis: verum end; theorem Th18: :: MYCIELSK:18 for R being RelStr for x, y being Element of R for a, b being Element of (ComplRelStr R) st x = a & y = b & x <> y & x in the carrier of R & not a <= b holds x <= y proof let R be RelStr ; ::_thesis: for x, y being Element of R for a, b being Element of (ComplRelStr R) st x = a & y = b & x <> y & x in the carrier of R & not a <= b holds x <= y let x, y be Element of R; ::_thesis: for a, b being Element of (ComplRelStr R) st x = a & y = b & x <> y & x in the carrier of R & not a <= b holds x <= y let a, b be Element of (ComplRelStr R); ::_thesis: ( x = a & y = b & x <> y & x in the carrier of R & not a <= b implies x <= y ) assume that A1: x = a and A2: y = b and A3: x <> y and A4: x in the carrier of R ; ::_thesis: ( a <= b or x <= y ) set cR = the carrier of R; set iR = the InternalRel of R; set CR = ComplRelStr R; set iCR = the InternalRel of (ComplRelStr R); A5: the InternalRel of (ComplRelStr R) = ( the InternalRel of R `) \ (id the carrier of R) by NECKLACE:def_8; A6: [x,y] in [: the carrier of R, the carrier of R:] by A4, ZFMISC_1:def_2; assume not a <= b ; ::_thesis: x <= y then A7: not [x,y] in the InternalRel of (ComplRelStr R) by A1, A2, ORDERS_2:def_5; not [x,y] in id the carrier of R by A3, RELAT_1:def_10; then not [x,y] in the InternalRel of R ` by A5, A7, XBOOLE_0:def_5; then [x,y] in the InternalRel of R by A6, XBOOLE_0:def_5; hence x <= y by ORDERS_2:def_5; ::_thesis: verum end; registration let R be finite RelStr ; cluster ComplRelStr R -> finite ; coherence ComplRelStr R is finite proof the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def_8; hence ComplRelStr R is finite ; ::_thesis: verum end; end; theorem Th19: :: MYCIELSK:19 for R being symmetric RelStr for C being Clique of R holds C is StableSet of (ComplRelStr R) proof let R be symmetric RelStr ; ::_thesis: for C being Clique of R holds C is StableSet of (ComplRelStr R) let C be Clique of R; ::_thesis: C is StableSet of (ComplRelStr R) now__::_thesis:_for_x,_y_being_Element_of_(ComplRelStr_R)_st_x_in_C_&_y_in_C_&_x_<>_y_holds_ (_not_x_<=_y_&_not_y_<=_x_) let x, y be Element of (ComplRelStr R); ::_thesis: ( x in C & y in C & x <> y implies ( not x <= y & not y <= x ) ) assume that A1: x in C and A2: y in C and A3: x <> y ; ::_thesis: ( not x <= y & not y <= x ) reconsider a = x, b = y as Element of R by NECKLACE:def_8; ( a <= b or b <= a ) by A1, A2, A3, DILWORTH:6; then ( a <= b & b <= a ) by Th6; hence ( not x <= y & not y <= x ) by Th17; ::_thesis: verum end; hence C is StableSet of (ComplRelStr R) by DILWORTH:def_2, NECKLACE:def_8; ::_thesis: verum end; theorem Th20: :: MYCIELSK:20 for R being symmetric RelStr for C being Clique of (ComplRelStr R) holds C is StableSet of R proof let R be symmetric RelStr ; ::_thesis: for C being Clique of (ComplRelStr R) holds C is StableSet of R let C be Clique of (ComplRelStr R); ::_thesis: C is StableSet of R now__::_thesis:_for_x,_y_being_Element_of_R_st_x_in_C_&_y_in_C_&_x_<>_y_holds_ (_not_x_<=_y_&_not_y_<=_x_) let x, y be Element of R; ::_thesis: ( x in C & y in C & x <> y implies ( not x <= y & not y <= x ) ) assume that A1: x in C and A2: y in C and A3: x <> y ; ::_thesis: ( not x <= y & not y <= x ) reconsider a = x, b = y as Element of (ComplRelStr R) by NECKLACE:def_8; ( a <= b or b <= a ) by A1, A2, A3, DILWORTH:6; then ( a <= b & b <= a ) by Th6; hence ( not x <= y & not y <= x ) by Th17; ::_thesis: verum end; hence C is StableSet of R by DILWORTH:def_2, NECKLACE:def_8; ::_thesis: verum end; theorem Th21: :: MYCIELSK:21 for R being RelStr for C being StableSet of R holds C is Clique of (ComplRelStr R) proof let R be RelStr ; ::_thesis: for C being StableSet of R holds C is Clique of (ComplRelStr R) let C be StableSet of R; ::_thesis: C is Clique of (ComplRelStr R) set CR = ComplRelStr R; A1: C is Subset of (ComplRelStr R) by NECKLACE:def_8; now__::_thesis:_for_a,_b_being_Element_of_(ComplRelStr_R)_st_a_in_C_&_b_in_C_&_a_<>_b_&_not_a_<=_b_holds_ b_<=_a let a, b be Element of (ComplRelStr 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 ap1 = a, bp1 = b as Element of R by NECKLACE:def_8; ( not ap1 <= bp1 & not bp1 <= ap1 ) by A2, A3, A4, DILWORTH:def_2; hence ( a <= b or b <= a ) by A2, A4, Th18; ::_thesis: verum end; hence C is Clique of (ComplRelStr R) by A1, DILWORTH:6; ::_thesis: verum end; theorem Th22: :: MYCIELSK:22 for R being RelStr for C being StableSet of (ComplRelStr R) holds C is Clique of R proof let R be RelStr ; ::_thesis: for C being StableSet of (ComplRelStr R) holds C is Clique of R let C be StableSet of (ComplRelStr R); ::_thesis: C is Clique of R A1: the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def_8; 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 ap1 = a, bp1 = b as Element of (ComplRelStr R) by NECKLACE:def_8; ( not ap1 <= bp1 & not bp1 <= ap1 ) by A2, A3, A4, DILWORTH:def_2; hence ( a <= b or b <= a ) by A4, A2, A1, Th18; ::_thesis: verum end; hence C is Clique of R by DILWORTH:6, NECKLACE:def_8; ::_thesis: verum end; registration let R be with_finite_clique# RelStr ; cluster ComplRelStr R -> with_finite_stability# ; coherence ComplRelStr R is with_finite_stability# proof set CR = ComplRelStr R; consider C being finite Clique of R such that A1: for D being finite Clique of R holds card D <= card C by DILWORTH:def_3; assume not ComplRelStr R is with_finite_stability# ; ::_thesis: contradiction then A2: for A being finite StableSet of (ComplRelStr R) ex B being finite StableSet of (ComplRelStr R) st card B > card A by DILWORTH:def_5; defpred S1[ Nat] means ex S being finite StableSet of (ComplRelStr R) st card S > R; consider B being finite StableSet of (ComplRelStr R) such that A3: card B > card ({} (ComplRelStr R)) by A2; A4: S1[ 0 ] by A3; A5: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then consider S being finite StableSet of (ComplRelStr R) such that A6: card S > n ; consider T being finite StableSet of (ComplRelStr R) such that A7: card T > card S by A2; card S >= n + 1 by A6, NAT_1:13; then card T > n + 1 by A7, XXREAL_0:2; hence S1[n + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A4, A5); then consider S being finite StableSet of (ComplRelStr R) such that A8: card S > card C ; S is Clique of R by Th22; hence contradiction by A1, A8; ::_thesis: verum end; end; registration let R be symmetric with_finite_stability# RelStr ; cluster ComplRelStr R -> with_finite_clique# ; coherence ComplRelStr R is with_finite_clique# proof set CR = ComplRelStr R; consider C being finite StableSet of R such that A1: for D being finite StableSet of R holds card D <= card C by DILWORTH:def_5; assume not ComplRelStr R is with_finite_clique# ; ::_thesis: contradiction then A2: for C being finite Clique of (ComplRelStr R) ex D being finite Clique of (ComplRelStr R) st card D > card C by DILWORTH:def_3; defpred S1[ Nat] means ex S being finite Clique of (ComplRelStr R) st card S > R; consider B being finite Clique of (ComplRelStr R) such that A3: card B > card ({} (ComplRelStr R)) by A2; A4: S1[ 0 ] by A3; A5: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then consider S being finite Clique of (ComplRelStr R) such that A6: card S > n ; consider T being finite Clique of (ComplRelStr R) such that A7: card T > card S by A2; card S >= n + 1 by A6, NAT_1:13; then card T > n + 1 by A7, XXREAL_0:2; hence S1[n + 1] ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A4, A5); then consider S being finite Clique of (ComplRelStr R) such that A8: card S > card C ; S is StableSet of R by Th20; hence contradiction by A1, A8; ::_thesis: verum end; end; theorem Th23: :: MYCIELSK:23 for R being symmetric with_finite_clique# RelStr holds clique# R = stability# (ComplRelStr R) proof let R be symmetric with_finite_clique# RelStr ; ::_thesis: clique# R = stability# (ComplRelStr R) set k = stability# (ComplRelStr R); consider A being finite StableSet of (ComplRelStr R) such that A1: card A = stability# (ComplRelStr R) by DILWORTH:def_6; A is Clique of R by Th22; then A2: ex C being finite Clique of R st card C = stability# (ComplRelStr R) by A1; now__::_thesis:_for_T_being_finite_Clique_of_R_holds_card_T_<=_stability#_(ComplRelStr_R) let T be finite Clique of R; ::_thesis: card T <= stability# (ComplRelStr R) T is StableSet of (ComplRelStr R) by Th19; hence card T <= stability# (ComplRelStr R) by DILWORTH:def_6; ::_thesis: verum end; hence clique# R = stability# (ComplRelStr R) by A2, DILWORTH:def_4; ::_thesis: verum end; theorem :: MYCIELSK:24 for R being symmetric with_finite_stability# RelStr holds stability# R = clique# (ComplRelStr R) proof let R be symmetric with_finite_stability# RelStr ; ::_thesis: stability# R = clique# (ComplRelStr R) set CR = ComplRelStr R; set k = clique# (ComplRelStr R); consider A being finite Clique of (ComplRelStr R) such that A1: card A = clique# (ComplRelStr R) by DILWORTH:def_4; A is StableSet of R by Th20; then A2: ex C being finite StableSet of R st card C = clique# (ComplRelStr R) by A1; now__::_thesis:_for_T_being_finite_StableSet_of_R_holds_card_T_<=_clique#_(ComplRelStr_R) let T be finite StableSet of R; ::_thesis: card T <= clique# (ComplRelStr R) T is Clique of (ComplRelStr R) by Th21; hence card T <= clique# (ComplRelStr R) by DILWORTH:def_4; ::_thesis: verum end; hence stability# R = clique# (ComplRelStr R) by A2, DILWORTH:def_6; ::_thesis: verum end; theorem Th25: :: MYCIELSK:25 for R being RelStr for C being Coloring of R holds C is Clique-partition of (ComplRelStr R) proof let R be RelStr ; ::_thesis: for C being Coloring of R holds C is Clique-partition of (ComplRelStr R) let C be Coloring of R; ::_thesis: C is Clique-partition of (ComplRelStr R) A1: the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def_8; now__::_thesis:_for_x_being_set_st_x_in_C_holds_ x_is_Clique_of_(ComplRelStr_R) let x be set ; ::_thesis: ( x in C implies x is Clique of (ComplRelStr R) ) assume x in C ; ::_thesis: x is Clique of (ComplRelStr R) then x is StableSet of R by DILWORTH:def_12; hence x is Clique of (ComplRelStr R) by Th21; ::_thesis: verum end; hence C is Clique-partition of (ComplRelStr R) by A1, DILWORTH:def_11; ::_thesis: verum end; theorem Th26: :: MYCIELSK:26 for R being symmetric RelStr for C being Clique-partition of (ComplRelStr R) holds C is Coloring of R proof let R be symmetric RelStr ; ::_thesis: for C being Clique-partition of (ComplRelStr R) holds C is Coloring of R let C be Clique-partition of (ComplRelStr R); ::_thesis: C is Coloring of R set CR = ComplRelStr R; A1: the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def_8; now__::_thesis:_for_x_being_set_st_x_in_C_holds_ x_is_StableSet_of_R let x be set ; ::_thesis: ( x in C implies x is StableSet of R ) assume x in C ; ::_thesis: x is StableSet of R then x is Clique of (ComplRelStr R) by DILWORTH:def_11; hence x is StableSet of R by Th20; ::_thesis: verum end; hence C is Coloring of R by A1, DILWORTH:def_12; ::_thesis: verum end; theorem Th27: :: MYCIELSK:27 for R being symmetric RelStr for C being Clique-partition of R holds C is Coloring of (ComplRelStr R) proof let R be symmetric RelStr ; ::_thesis: for C being Clique-partition of R holds C is Coloring of (ComplRelStr R) let C be Clique-partition of R; ::_thesis: C is Coloring of (ComplRelStr R) set CR = ComplRelStr R; A1: the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def_8; now__::_thesis:_for_x_being_set_st_x_in_C_holds_ x_is_StableSet_of_(ComplRelStr_R) let x be set ; ::_thesis: ( x in C implies x is StableSet of (ComplRelStr R) ) assume x in C ; ::_thesis: x is StableSet of (ComplRelStr R) then x is Clique of R by DILWORTH:def_11; hence x is StableSet of (ComplRelStr R) by Th19; ::_thesis: verum end; hence C is Coloring of (ComplRelStr R) by A1, DILWORTH:def_12; ::_thesis: verum end; theorem Th28: :: MYCIELSK:28 for R being RelStr for C being Coloring of (ComplRelStr R) holds C is Clique-partition of R proof let R be RelStr ; ::_thesis: for C being Coloring of (ComplRelStr R) holds C is Clique-partition of R let C be Coloring of (ComplRelStr R); ::_thesis: C is Clique-partition of R set CR = ComplRelStr R; A1: the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def_8; now__::_thesis:_for_x_being_set_st_x_in_C_holds_ x_is_Clique_of_R let x be set ; ::_thesis: ( x in C implies x is Clique of R ) assume x in C ; ::_thesis: x is Clique of R then x is StableSet of (ComplRelStr R) by DILWORTH:def_12; hence x is Clique of R by Th22; ::_thesis: verum end; hence C is Clique-partition of R by A1, DILWORTH:def_11; ::_thesis: verum end; registration let R be with_finite_chromatic# RelStr ; cluster ComplRelStr R -> with_finite_cliquecover# ; coherence ComplRelStr R is with_finite_cliquecover# proof consider C being Coloring of R such that A1: C is finite by Def2; C is Clique-partition of (ComplRelStr R) by Th25; hence ComplRelStr R is with_finite_cliquecover# by A1, Def4; ::_thesis: verum end; end; registration let R be symmetric with_finite_cliquecover# RelStr ; cluster ComplRelStr R -> with_finite_chromatic# ; coherence ComplRelStr R is with_finite_chromatic# proof consider C being Clique-partition of R such that A1: C is finite by Def4; C is Coloring of (ComplRelStr R) by Th27; hence ComplRelStr R is with_finite_chromatic# by A1, Def2; ::_thesis: verum end; end; theorem Th29: :: MYCIELSK:29 for R being symmetric with_finite_chromatic# RelStr holds chromatic# R = cliquecover# (ComplRelStr R) proof let R be symmetric with_finite_chromatic# RelStr ; ::_thesis: chromatic# R = cliquecover# (ComplRelStr R) set CR = ComplRelStr R; set k = cliquecover# (ComplRelStr R); consider C being finite Clique-partition of (ComplRelStr R) such that A1: card C = cliquecover# (ComplRelStr R) by Def5; C is Coloring of R by Th26; then A2: ex C being finite Coloring of R st card C = cliquecover# (ComplRelStr R) by A1; now__::_thesis:_for_C_being_finite_Coloring_of_R_holds_not_cliquecover#_(ComplRelStr_R)_>_card_C let C be finite Coloring of R; ::_thesis: not cliquecover# (ComplRelStr R) > card C assume A3: cliquecover# (ComplRelStr R) > card C ; ::_thesis: contradiction C is Clique-partition of (ComplRelStr R) by Th25; hence contradiction by A3, Def5; ::_thesis: verum end; hence chromatic# R = cliquecover# (ComplRelStr R) by A2, Def3; ::_thesis: verum end; theorem :: MYCIELSK:30 for R being symmetric with_finite_cliquecover# RelStr holds cliquecover# R = chromatic# (ComplRelStr R) proof let R be symmetric with_finite_cliquecover# RelStr ; ::_thesis: cliquecover# R = chromatic# (ComplRelStr R) set CR = ComplRelStr R; set k = chromatic# (ComplRelStr R); consider C being finite Coloring of (ComplRelStr R) such that A1: card C = chromatic# (ComplRelStr R) by Def3; C is Clique-partition of R by Th28; then A2: ex C being finite Clique-partition of R st card C = chromatic# (ComplRelStr R) by A1; now__::_thesis:_for_C_being_finite_Clique-partition_of_R_holds_not_chromatic#_(ComplRelStr_R)_>_card_C let C be finite Clique-partition of R; ::_thesis: not chromatic# (ComplRelStr R) > card C assume A3: chromatic# (ComplRelStr R) > card C ; ::_thesis: contradiction C is Coloring of (ComplRelStr R) by Th27; hence contradiction by A3, Def3; ::_thesis: verum end; hence cliquecover# R = chromatic# (ComplRelStr R) by A2, Def5; ::_thesis: verum end; begin definition let R be RelStr ; let v be Element of R; func Adjacent v -> Subset of R means :Def6: :: MYCIELSK:def 6 for x being Element of R holds ( x in it iff ( x < v or v < x ) ); existence ex b1 being Subset of R st for x being Element of R holds ( x in b1 iff ( x < v or v < x ) ) proof set D = { x where x is Element of R : ( x < v or v < x ) } ; set cR = the carrier of R; set iR = the InternalRel of R; { x where x is Element of R : ( x < v or v < x ) } c= the carrier of R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { x where x is Element of R : ( x < v or v < x ) } or x in the carrier of R ) assume x in { x where x is Element of R : ( x < v or v < x ) } ; ::_thesis: x in the carrier of R then consider a being Element of R such that A1: x = a and A2: ( a < v or v < a ) ; percases ( a < v or v < a ) by A2; suppose a < v ; ::_thesis: x in the carrier of R then a <= v by ORDERS_2:def_6; then [a,v] in the InternalRel of R by ORDERS_2:def_5; then [a,v] in [: the carrier of R, the carrier of R:] ; hence x in the carrier of R by A1, ZFMISC_1:87; ::_thesis: verum end; suppose v < a ; ::_thesis: x in the carrier of R then v <= a by ORDERS_2:def_6; then [v,a] in the InternalRel of R by ORDERS_2:def_5; then [v,a] in [: the carrier of R, the carrier of R:] ; hence x in the carrier of R by A1, ZFMISC_1:87; ::_thesis: verum end; end; end; then reconsider D = { x where x is Element of R : ( x < v or v < x ) } as Subset of R ; take D ; ::_thesis: for x being Element of R holds ( x in D iff ( x < v or v < x ) ) let x be Element of R; ::_thesis: ( x in D iff ( x < v or v < x ) ) hereby ::_thesis: ( ( x < v or v < x ) implies x in D ) assume x in D ; ::_thesis: ( x < v or v < x ) then consider a being Element of R such that A3: x = a and A4: ( a < v or v < a ) ; thus ( x < v or v < x ) by A3, A4; ::_thesis: verum end; assume ( x < v or v < x ) ; ::_thesis: x in D hence x in D ; ::_thesis: verum end; uniqueness for b1, b2 being Subset of R st ( for x being Element of R holds ( x in b1 iff ( x < v or v < x ) ) ) & ( for x being Element of R holds ( x in b2 iff ( x < v or v < x ) ) ) holds b1 = b2 proof let it1, it2 be Subset of R; ::_thesis: ( ( for x being Element of R holds ( x in it1 iff ( x < v or v < x ) ) ) & ( for x being Element of R holds ( x in it2 iff ( x < v or v < x ) ) ) implies it1 = it2 ) assume that A5: for x being Element of R holds ( x in it1 iff ( x < v or v < x ) ) and A6: for x being Element of R holds ( x in it2 iff ( x < v or v < x ) ) ; ::_thesis: it1 = it2 hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: it2 c= it1 let x be set ; ::_thesis: ( x in it1 implies x in it2 ) assume A7: x in it1 ; ::_thesis: x in it2 then reconsider xp1 = x as Element of R ; ( xp1 < v or v < xp1 ) by A5, A7; hence x in it2 by A6; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in it2 or x in it1 ) assume A8: x in it2 ; ::_thesis: x in it1 then reconsider xp1 = x as Element of R ; ( xp1 < v or v < xp1 ) by A6, A8; hence x in it1 by A5; ::_thesis: verum end; end; :: deftheorem Def6 defines Adjacent MYCIELSK:def_6_:_ for R being RelStr for v being Element of R for b3 being Subset of R holds ( b3 = Adjacent v iff for x being Element of R holds ( x in b3 iff ( x < v or v < x ) ) ); theorem Th31: :: MYCIELSK:31 for R being with_finite_chromatic# RelStr for C being finite Coloring of R for c being set st c in C & card C = chromatic# R holds ex v being Element of R st ( v in c & ( for d being Element of C st d <> c holds ex w being Element of R st ( w in Adjacent v & w in d ) ) ) proof let R be with_finite_chromatic# RelStr ; ::_thesis: for C being finite Coloring of R for c being set st c in C & card C = chromatic# R holds ex v being Element of R st ( v in c & ( for d being Element of C st d <> c holds ex w being Element of R st ( w in Adjacent v & w in d ) ) ) let C be finite Coloring of R; ::_thesis: for c being set st c in C & card C = chromatic# R holds ex v being Element of R st ( v in c & ( for d being Element of C st d <> c holds ex w being Element of R st ( w in Adjacent v & w in d ) ) ) let c be set ; ::_thesis: ( c in C & card C = chromatic# R implies ex v being Element of R st ( v in c & ( for d being Element of C st d <> c holds ex w being Element of R st ( w in Adjacent v & w in d ) ) ) ) assume that A1: c in C and A2: card C = chromatic# R ; ::_thesis: ex v being Element of R st ( v in c & ( for d being Element of C st d <> c holds ex w being Element of R st ( w in Adjacent v & w in d ) ) ) assume A3: for v being Element of R holds ( not v in c or ex d being Element of C st ( d <> c & ( for w being Element of R holds ( not w in Adjacent v or not w in d ) ) ) ) ; ::_thesis: contradiction set cR = the carrier of R; A4: union C = the carrier of R by EQREL_1:def_4; reconsider c = c as Subset of the carrier of R by A1; A5: c <> {} by A1, EQREL_1:def_4; set Cc = C \ {c}; A6: c in {c} by TARSKI:def_1; percases ( C \ {c} is empty or not C \ {c} is empty ) ; supposeA7: C \ {c} is empty ; ::_thesis: contradiction consider v being set such that A8: v in c by A5, XBOOLE_0:def_1; reconsider v = v as Element of R by A8; consider d being Element of C such that A9: d <> c and for w being Element of R holds ( not w in Adjacent v or not w in d ) by A8, A3; 0 = (card C) - (card {c}) by A1, A7, CARD_1:27, EULER_1:4; then 0 + 1 = ((card C) - 1) + 1 by CARD_1:30; then consider x being set such that A10: C = {x} by CARD_2:42; ( c = x & d = x ) by A1, A10, TARSKI:def_1; hence contradiction by A9; ::_thesis: verum end; suppose not C \ {c} is empty ; ::_thesis: contradiction then reconsider Cc = C \ {c} as non empty set ; defpred S1[ set , set ] means for vv being Element of the carrier of R st $1 = vv holds ( $2 <> c & $2 in C & ( for w being Element of R holds ( not w in Adjacent vv or not w in $2 ) ) ); A11: for e being set st e in c holds ex u being set st S1[e,u] proof let v be set ; ::_thesis: ( v in c implies ex u being set st S1[v,u] ) assume A12: v in c ; ::_thesis: ex u being set st S1[v,u] reconsider vv = v as Element of the carrier of R by A12; consider d being Element of C such that A13: d <> c and A14: for w being Element of R holds ( not w in Adjacent vv or not w in d ) by A12, A3; take d ; ::_thesis: S1[v,d] thus S1[v,d] by A13, A14, A1; ::_thesis: verum end; consider r being Function such that A15: dom r = c and A16: for e being set st e in c holds S1[e,r . e] from CLASSES1:sch_1(A11); defpred S2[ set ] means verum; deffunc H1( set ) -> set = $1 \/ (r " {$1}); reconsider Cc = Cc as non empty finite set ; set D = { H1(d) where d is Element of Cc : S2[d] } ; consider d being set such that A17: d in Cc by XBOOLE_0:def_1; A18: d \/ (r " {d}) in { H1(d) where d is Element of Cc : S2[d] } by A17; A19: { H1(d) where d is Element of Cc : S2[d] } c= bool the carrier of R proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H1(d) where d is Element of Cc : S2[d] } or x in bool the carrier of R ) assume x in { H1(d) where d is Element of Cc : S2[d] } ; ::_thesis: x in bool the carrier of R then consider d being Element of Cc such that A20: x = d \/ (r " {d}) ; A21: r " {d} c= c by A15, RELAT_1:132; A22: r " {d} c= the carrier of R by A21, XBOOLE_1:1; d in C by XBOOLE_0:def_5; then x c= the carrier of R by A20, A22, XBOOLE_1:8; hence x in bool the carrier of R ; ::_thesis: verum end; A23: union { H1(d) where d is Element of Cc : S2[d] } = the carrier of R proof thus union { H1(d) where d is Element of Cc : S2[d] } c= the carrier of R :: according to XBOOLE_0:def_10 ::_thesis: the carrier of R c= union { H1(d) where d is Element of Cc : S2[d] } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { H1(d) where d is Element of Cc : S2[d] } or x in the carrier of R ) assume x in union { H1(d) where d is Element of Cc : S2[d] } ; ::_thesis: x in the carrier of R then consider Y being set such that A24: x in Y and A25: Y in { H1(d) where d is Element of Cc : S2[d] } by TARSKI:def_4; thus x in the carrier of R by A24, A25, A19; ::_thesis: verum end; thus the carrier of R c= union { H1(d) where d is Element of Cc : S2[d] } ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R or x in union { H1(d) where d is Element of Cc : S2[d] } ) assume A26: x in the carrier of R ; ::_thesis: x in union { H1(d) where d is Element of Cc : S2[d] } then consider d being set such that A27: x in d and A28: d in C by A4, TARSKI:def_4; reconsider xp1 = x as Element of the carrier of R by A26; percases ( d = c or d <> c ) ; supposeA29: d = c ; ::_thesis: x in union { H1(d) where d is Element of Cc : S2[d] } then r . xp1 <> c by A27, A16; then A30: not r . xp1 in {c} by TARSKI:def_1; r . xp1 in C by A27, A29, A16; then A31: r . xp1 in Cc by A30, XBOOLE_0:def_5; r . xp1 in {(r . xp1)} by TARSKI:def_1; then x in r " {(r . xp1)} by A27, A29, A15, FUNCT_1:def_7; then A32: x in (r . xp1) \/ (r " {(r . xp1)}) by XBOOLE_0:def_3; (r . xp1) \/ (r " {(r . xp1)}) in { H1(d) where d is Element of Cc : S2[d] } by A31; hence x in union { H1(d) where d is Element of Cc : S2[d] } by A32, TARSKI:def_4; ::_thesis: verum end; suppose d <> c ; ::_thesis: x in union { H1(d) where d is Element of Cc : S2[d] } then not d in {c} by TARSKI:def_1; then d in Cc by A28, XBOOLE_0:def_5; then A33: d \/ (r " {d}) in { H1(d) where d is Element of Cc : S2[d] } ; x in d \/ (r " {d}) by A27, XBOOLE_0:def_3; hence x in union { H1(d) where d is Element of Cc : S2[d] } by A33, TARSKI:def_4; ::_thesis: verum end; end; end; end; A34: for A being Subset of the carrier of R st A in { H1(d) where d is Element of Cc : S2[d] } holds ( A <> {} & ( for B being Subset of the carrier of R holds ( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B ) ) ) proof let A be Subset of the carrier of R; ::_thesis: ( A in { H1(d) where d is Element of Cc : S2[d] } implies ( A <> {} & ( for B being Subset of the carrier of R holds ( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B ) ) ) ) assume A in { H1(d) where d is Element of Cc : S2[d] } ; ::_thesis: ( A <> {} & ( for B being Subset of the carrier of R holds ( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B ) ) ) then consider da being Element of Cc such that A35: A = da \/ (r " {da}) ; A36: da in C by XBOOLE_0:def_5; then not da is empty by EQREL_1:def_4; hence A <> {} by A35; ::_thesis: for B being Subset of the carrier of R holds ( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B ) let B be Subset of the carrier of R; ::_thesis: ( not B in { H1(d) where d is Element of Cc : S2[d] } or A = B or A misses B ) assume B in { H1(d) where d is Element of Cc : S2[d] } ; ::_thesis: ( A = B or A misses B ) then consider db being Element of Cc such that A37: B = db \/ (r " {db}) ; A38: db in C by XBOOLE_0:def_5; percases ( da = db or da <> db ) ; suppose da = db ; ::_thesis: ( A = B or A misses B ) hence ( A = B or A misses B ) by A35, A37; ::_thesis: verum end; supposeA39: da <> db ; ::_thesis: ( A = B or A misses B ) then A40: da misses db by A36, A38, EQREL_1:def_4; A41: r " {da} misses r " {db} by A39, FUNCT_1:71, ZFMISC_1:11; assume A <> B ; ::_thesis: A misses B assume A meets B ; ::_thesis: contradiction then consider x being set such that A42: x in A and A43: x in B by XBOOLE_0:3; percases ( ( x in da & x in db ) or ( x in da & x in r " {db} ) or ( x in r " {da} & x in db ) or ( x in r " {da} & x in r " {db} ) ) by A42, A43, A35, A37, XBOOLE_0:def_3; suppose ( x in da & x in db ) ; ::_thesis: contradiction hence contradiction by A40, XBOOLE_0:3; ::_thesis: verum end; supposethat A44: x in da and A45: x in r " {db} ; ::_thesis: contradiction A46: da <> c by A6, XBOOLE_0:def_5; r " {db} c= c by A15, RELAT_1:132; then da meets c by A44, A45, XBOOLE_0:3; hence contradiction by A46, A36, A1, EQREL_1:def_4; ::_thesis: verum end; supposethat A47: x in r " {da} and A48: x in db ; ::_thesis: contradiction A49: db <> c by A6, XBOOLE_0:def_5; r " {da} c= c by A15, RELAT_1:132; then db meets c by A47, A48, XBOOLE_0:3; hence contradiction by A49, A38, A1, EQREL_1:def_4; ::_thesis: verum end; suppose ( x in r " {da} & x in r " {db} ) ; ::_thesis: contradiction hence contradiction by A41, XBOOLE_0:3; ::_thesis: verum end; end; end; end; end; reconsider D = { H1(d) where d is Element of Cc : S2[d] } as a_partition of the carrier of R by A19, A23, A34, EQREL_1:def_4; now__::_thesis:_for_x_being_set_st_x_in_D_holds_ x_is_StableSet_of_R let x be set ; ::_thesis: ( x in D implies x is StableSet of R ) assume A50: x in D ; ::_thesis: x is StableSet of R then reconsider S = x as Subset of R ; consider d being Element of Cc such that A51: x = d \/ (r " {d}) by A50; A52: r " {d} c= c by A15, RELAT_1:132; A53: d in C by XBOOLE_0:def_5; A54: d is StableSet of R by A53, DILWORTH:def_12; A55: c is StableSet of R by A1, DILWORTH:def_12; S is stable proof let a, b be Element of R; :: according to DILWORTH:def_2 ::_thesis: ( not a in S or not b in S or a = b or ( not a <= b & not b <= a ) ) assume that A56: a in S and A57: b in S and A58: a <> b ; ::_thesis: ( not a <= b & not b <= a ) percases ( ( a in d & b in d ) or ( a in d & b in r " {d} ) or ( a in r " {d} & b in d ) or ( a in r " {d} & b in r " {d} ) ) by A56, A57, A51, XBOOLE_0:def_3; suppose ( a in d & b in d ) ; ::_thesis: ( not a <= b & not b <= a ) hence ( not a <= b & not b <= a ) by A54, A58, DILWORTH:def_2; ::_thesis: verum end; supposethat A59: a in d and A60: b in r " {d} ; ::_thesis: ( not a <= b & not b <= a ) r . b in {d} by A60, FUNCT_1:def_7; then r . b = d by TARSKI:def_1; then not a in Adjacent b by A59, A52, A60, A16; then ( not a < b & not b < a ) by Def6; hence ( not a <= b & not b <= a ) by A58, ORDERS_2:def_6; ::_thesis: verum end; supposethat A61: a in r " {d} and A62: b in d ; ::_thesis: ( not a <= b & not b <= a ) r . a in {d} by A61, FUNCT_1:def_7; then r . a = d by TARSKI:def_1; then not b in Adjacent a by A62, A52, A61, A16; then ( not a < b & not b < a ) by Def6; hence ( not a <= b & not b <= a ) by A58, ORDERS_2:def_6; ::_thesis: verum end; suppose ( a in r " {d} & b in r " {d} ) ; ::_thesis: ( not a <= b & not b <= a ) hence ( not a <= b & not b <= a ) by A52, A55, A58, DILWORTH:def_2; ::_thesis: verum end; end; end; hence x is StableSet of R ; ::_thesis: verum end; then reconsider D = D as Coloring of R by DILWORTH:def_12; card Cc = (card C) - (card {c}) by A1, EULER_1:4; then (card Cc) + 1 = ((card C) - 1) + 1 by CARD_1:30; then A63: card Cc < card C by NAT_1:13; deffunc H2( set ) -> set = $1 \/ (r " {$1}); consider s being Function such that A64: dom s = Cc and A65: for x being set st x in Cc holds s . x = H2(x) from FUNCT_1:sch_3(); A66: rng s c= D proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s or y in D ) assume y in rng s ; ::_thesis: y in D then consider d being set such that A67: d in dom s and A68: y = s . d by FUNCT_1:def_3; y = d \/ (r " {d}) by A64, A65, A67, A68; hence y in D by A67, A64; ::_thesis: verum end; then reconsider s = s as Function of Cc,D by A64, FUNCT_2:2; A69: s is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom s or not x2 in dom s or not s . x1 = s . x2 or x1 = x2 ) assume that A70: x1 in dom s and A71: x2 in dom s and A72: s . x1 = s . x2 ; ::_thesis: x1 = x2 A73: s . x1 = x1 \/ (r " {x1}) by A70, A65; A74: s . x2 = x2 \/ (r " {x2}) by A71, A65; thus x1 c= x2 :: according to XBOOLE_0:def_10 ::_thesis: x2 c= x1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in x1 or x in x2 ) assume A75: x in x1 ; ::_thesis: x in x2 then A76: x in s . x1 by A73, XBOOLE_0:def_3; percases ( x in x2 or x in r " {x2} ) by A76, A72, A74, XBOOLE_0:def_3; suppose x in x2 ; ::_thesis: x in x2 hence x in x2 ; ::_thesis: verum end; supposeA77: x in r " {x2} ; ::_thesis: x in x2 A78: r " {x2} c= dom r by RELAT_1:132; A79: x1 in C by A70, XBOOLE_0:def_5; then reconsider x1 = x1 as Subset of the carrier of R ; x1 meets c by A78, A77, A15, A75, XBOOLE_0:3; then x1 = c by A79, A1, EQREL_1:def_4; hence x in x2 by A6, A70, XBOOLE_0:def_5; ::_thesis: verum end; end; end; thus x2 c= x1 ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in x2 or x in x1 ) assume A80: x in x2 ; ::_thesis: x in x1 then A81: x in s . x2 by A74, XBOOLE_0:def_3; percases ( x in x1 or x in r " {x1} ) by A81, A72, A73, XBOOLE_0:def_3; suppose x in x1 ; ::_thesis: x in x1 hence x in x1 ; ::_thesis: verum end; supposeA82: x in r " {x1} ; ::_thesis: x in x1 A83: r " {x1} c= dom r by RELAT_1:132; A84: x2 in C by A71, XBOOLE_0:def_5; then reconsider x2 = x2 as Subset of the carrier of R ; x2 meets c by A83, A82, A15, A80, XBOOLE_0:3; then x2 = c by A84, A1, EQREL_1:def_4; hence x in x1 by A6, A71, XBOOLE_0:def_5; ::_thesis: verum end; end; end; end; D c= rng s proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in rng s ) assume x in D ; ::_thesis: x in rng s then consider d being Element of Cc such that A85: x = d \/ (r " {d}) ; s . d = d \/ (r " {d}) by A65; hence x in rng s by A85, A64, FUNCT_1:def_3; ::_thesis: verum end; then D = rng s by A66, XBOOLE_0:def_10; then s is onto by FUNCT_2:def_3; then A86: card Cc = card D by A69, A18, EULER_1:11; then D is finite ; hence contradiction by A63, A86, A2, Def3; ::_thesis: verum end; end; end; begin definition let n be Nat; mode NatRelStr of n -> strict RelStr means :Def7: :: MYCIELSK:def 7 the carrier of it = n; existence ex b1 being strict RelStr st the carrier of b1 = n proof reconsider I = {} as Relation of n,n by RELSET_1:12; take RelStr(# n,I #) ; ::_thesis: the carrier of RelStr(# n,I #) = n thus the carrier of RelStr(# n,I #) = n ; ::_thesis: verum end; end; :: deftheorem Def7 defines NatRelStr MYCIELSK:def_7_:_ for n being Nat for b2 being strict RelStr holds ( b2 is NatRelStr of n iff the carrier of b2 = n ); registration cluster -> empty for NatRelStr of 0 ; coherence for b1 being NatRelStr of 0 holds b1 is empty by Def7; end; registration let n be non empty Nat; cluster -> non empty for NatRelStr of n; coherence for b1 being NatRelStr of n holds not b1 is empty by Def7; end; registration let n be Nat; cluster -> finite for NatRelStr of n; coherence for b1 being NatRelStr of n holds b1 is finite by Def7; cluster strict irreflexive for NatRelStr of n; existence ex b1 being NatRelStr of n st b1 is irreflexive proof reconsider I = {} as Relation of n,n by RELSET_1:12; set R = RelStr(# n,I #); reconsider R = RelStr(# n,I #) as NatRelStr of n by Def7; R is irreflexive proof let x be set ; :: according to NECKLACE:def_5 ::_thesis: ( not x in the carrier of R or not [x,x] in the InternalRel of R ) assume x in the carrier of R ; ::_thesis: not [x,x] in the InternalRel of R thus not [x,x] in the InternalRel of R ; ::_thesis: verum end; hence ex b1 being NatRelStr of n st b1 is irreflexive ; ::_thesis: verum end; end; definition let n be Nat; func CompleteRelStr n -> NatRelStr of n means :Def8: :: MYCIELSK:def 8 the InternalRel of it = [:n,n:] \ (id n); existence ex b1 being NatRelStr of n st the InternalRel of b1 = [:n,n:] \ (id n) proof [:n,n:] c= [:n,n:] ; then reconsider f = [:n,n:] as Relation of n ; reconsider R = RelStr(# n,(f \ (id n)) #) as NatRelStr of n by Def7; take R ; ::_thesis: the InternalRel of R = [:n,n:] \ (id n) thus the InternalRel of R = [:n,n:] \ (id n) ; ::_thesis: verum end; uniqueness for b1, b2 being NatRelStr of n st the InternalRel of b1 = [:n,n:] \ (id n) & the InternalRel of b2 = [:n,n:] \ (id n) holds b1 = b2 proof let C1, C2 be NatRelStr of n; ::_thesis: ( the InternalRel of C1 = [:n,n:] \ (id n) & the InternalRel of C2 = [:n,n:] \ (id n) implies C1 = C2 ) ( the carrier of C1 = n & the carrier of C2 = n ) by Def7; hence ( the InternalRel of C1 = [:n,n:] \ (id n) & the InternalRel of C2 = [:n,n:] \ (id n) implies C1 = C2 ) ; ::_thesis: verum end; end; :: deftheorem Def8 defines CompleteRelStr MYCIELSK:def_8_:_ for n being Nat for b2 being NatRelStr of n holds ( b2 = CompleteRelStr n iff the InternalRel of b2 = [:n,n:] \ (id n) ); theorem Th32: :: MYCIELSK:32 for n being Nat for x, y being set st x in n & y in n holds ( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y ) proof let n be Nat; ::_thesis: for x, y being set st x in n & y in n holds ( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y ) let x, y be set ; ::_thesis: ( x in n & y in n implies ( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y ) ) assume A1: ( x in n & y in n ) ; ::_thesis: ( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y ) hereby ::_thesis: ( x <> y implies [x,y] in the InternalRel of (CompleteRelStr n) ) assume [x,y] in the InternalRel of (CompleteRelStr n) ; ::_thesis: x <> y then [x,y] in [:n,n:] \ (id n) by Def8; then not [x,y] in id n by XBOOLE_0:def_5; hence x <> y by A1, RELAT_1:def_10; ::_thesis: verum end; assume x <> y ; ::_thesis: [x,y] in the InternalRel of (CompleteRelStr n) then ( [x,y] in [:n,n:] & not [x,y] in id n ) by A1, RELAT_1:def_10, ZFMISC_1:87; then [x,y] in [:n,n:] \ (id n) by XBOOLE_0:def_5; hence [x,y] in the InternalRel of (CompleteRelStr n) by Def8; ::_thesis: verum end; registration let n be Nat; cluster CompleteRelStr n -> symmetric irreflexive ; coherence ( CompleteRelStr n is irreflexive & CompleteRelStr n is symmetric ) proof set R = CompleteRelStr n; set cR = the carrier of (CompleteRelStr n); set iR = the InternalRel of (CompleteRelStr n); A1: the carrier of (CompleteRelStr n) = n by Def7; thus CompleteRelStr n is irreflexive ::_thesis: CompleteRelStr n is symmetric proof let x be set ; :: according to NECKLACE:def_5 ::_thesis: ( not x in the carrier of (CompleteRelStr n) or not [x,x] in the InternalRel of (CompleteRelStr n) ) assume x in the carrier of (CompleteRelStr n) ; ::_thesis: not [x,x] in the InternalRel of (CompleteRelStr n) hence not [x,x] in the InternalRel of (CompleteRelStr n) by A1, Th32; ::_thesis: verum end; thus CompleteRelStr n is symmetric ::_thesis: verum proof let x, y be set ; :: according to RELAT_2:def_3,NECKLACE:def_3 ::_thesis: ( not x in the carrier of (CompleteRelStr n) or not y in the carrier of (CompleteRelStr n) or not [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) ) assume ( x in the carrier of (CompleteRelStr n) & y in the carrier of (CompleteRelStr n) ) ; ::_thesis: ( not [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) ) then A2: ( x in n & y in n ) by Def7; assume [x,y] in the InternalRel of (CompleteRelStr n) ; ::_thesis: [y,x] in the InternalRel of (CompleteRelStr n) hence [y,x] in the InternalRel of (CompleteRelStr n) by A2, Th32; ::_thesis: verum end; end; end; registration let n be Nat; cluster [#] (CompleteRelStr n) -> clique ; coherence [#] (CompleteRelStr n) is connected proof set R = CompleteRelStr n; set iR = the InternalRel of (CompleteRelStr n); let x, y be set ; :: according to RELAT_2:def_6,DILWORTH:def_1 ::_thesis: ( not x in [#] (CompleteRelStr n) or not y in [#] (CompleteRelStr n) or x = y or [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) ) assume ( x in [#] (CompleteRelStr n) & y in [#] (CompleteRelStr n) ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) ) then A1: ( x in n & y in n ) by Def7; assume x <> y ; ::_thesis: ( [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) ) hence ( [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) ) by A1, Th32; ::_thesis: verum end; end; theorem Th33: :: MYCIELSK:33 for n being Nat holds clique# (CompleteRelStr n) = n proof let n be Nat; ::_thesis: clique# (CompleteRelStr n) = n set R = CompleteRelStr n; A1: card (card n) = card n ; [#] (CompleteRelStr n) = n by Def7; then A2: ex C being finite Clique of (CompleteRelStr n) st card C = n by A1, CARD_1:40; for T being finite Clique of (CompleteRelStr n) holds card T <= n proof let T be finite Clique of (CompleteRelStr n); ::_thesis: card T <= n card n = n by A1, CARD_1:40; then A3: card the carrier of (CompleteRelStr n) = n by Def7; A4: card T <= clique# (CompleteRelStr n) by DILWORTH:def_4; clique# (CompleteRelStr n) <= n by A3, Th11; hence card T <= n by A4, XXREAL_0:2; ::_thesis: verum end; hence clique# (CompleteRelStr n) = n by A2, DILWORTH:def_4; ::_thesis: verum end; theorem :: MYCIELSK:34 for n being non empty Nat holds stability# (CompleteRelStr n) = 1 proof let n be non empty Nat; ::_thesis: stability# (CompleteRelStr n) = 1 set R = CompleteRelStr n; [#] (CompleteRelStr n) is Clique of (CompleteRelStr n) ; hence stability# (CompleteRelStr n) = 1 by DILWORTH:20; ::_thesis: verum end; theorem Th35: :: MYCIELSK:35 for n being Nat holds chromatic# (CompleteRelStr n) = n proof let n be Nat; ::_thesis: chromatic# (CompleteRelStr n) = n set R = CompleteRelStr n; clique# (CompleteRelStr n) = n by Th33; then A1: n <= chromatic# (CompleteRelStr n) by Th15; A2: chromatic# (CompleteRelStr n) <= card the carrier of (CompleteRelStr n) by Th13; card (card n) = card n ; then card n = n by CARD_1:40; then card the carrier of (CompleteRelStr n) = n by Def7; hence chromatic# (CompleteRelStr n) = n by A1, A2, XXREAL_0:1; ::_thesis: verum end; theorem :: MYCIELSK:36 for n being non empty Nat holds cliquecover# (CompleteRelStr n) = 1 proof let n be non empty Nat; ::_thesis: cliquecover# (CompleteRelStr n) = 1 set R = CompleteRelStr n; set cR = the carrier of (CompleteRelStr n); reconsider C = { the carrier of (CompleteRelStr n)} as a_partition of the carrier of (CompleteRelStr n) by EQREL_1:39; A1: now__::_thesis:_for_x_being_set_st_x_in_C_holds_ x_is_Clique_of_(CompleteRelStr_n) let x be set ; ::_thesis: ( x in C implies x is Clique of (CompleteRelStr n) ) assume x in C ; ::_thesis: x is Clique of (CompleteRelStr n) then x = [#] (CompleteRelStr n) by TARSKI:def_1; hence x is Clique of (CompleteRelStr n) ; ::_thesis: verum end; A2: now__::_thesis:_ex_C_being_a_partition_of_the_carrier_of_(CompleteRelStr_n)_st_ (_C_is_finite_&_C_is_Clique-partition_of_(CompleteRelStr_n)_&_card_C_=_1_) take C = C; ::_thesis: ( C is finite & C is Clique-partition of (CompleteRelStr n) & card C = 1 ) thus C is finite ; ::_thesis: ( C is Clique-partition of (CompleteRelStr n) & card C = 1 ) thus C is Clique-partition of (CompleteRelStr n) by A1, DILWORTH:def_11; ::_thesis: card C = 1 thus card C = 1 by CARD_1:30; ::_thesis: verum end; now__::_thesis:_for_C_being_finite_Clique-partition_of_(CompleteRelStr_n)_holds_1_<=_card_C let C be finite Clique-partition of (CompleteRelStr n); ::_thesis: 1 <= card C 0 + 1 <= card C by NAT_1:13; hence 1 <= card C ; ::_thesis: verum end; hence cliquecover# (CompleteRelStr n) = 1 by A2, Def5; ::_thesis: verum end; begin definition let n be Nat; let R be NatRelStr of n; func Mycielskian R -> NatRelStr of (2 * n) + 1 means :Def9: :: MYCIELSK:def 9 the InternalRel of it = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:]; existence ex b1 being NatRelStr of (2 * n) + 1 st the InternalRel of b1 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] proof set cR = the carrier of R; set iR = the InternalRel of R; set cMR = (2 * n) + 1; set iMR = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:]; A1: the carrier of R = n by Def7; n <= n + n by NAT_1:11; then A2: n < (2 * n) + 1 by NAT_1:13; ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] c= [:((2 * n) + 1),((2 * n) + 1):] proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] or z in [:((2 * n) + 1),((2 * n) + 1):] ) assume A3: z in ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] ; ::_thesis: z in [:((2 * n) + 1),((2 * n) + 1):] percases ( z in the InternalRel of R or z in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } or z in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } or z in [:{(2 * n)},((2 * n) \ n):] or z in [:((2 * n) \ n),{(2 * n)}:] ) by A3, Th4; suppose z in the InternalRel of R ; ::_thesis: z in [:((2 * n) + 1),((2 * n) + 1):] then consider c, d being set such that A4: c in the carrier of R and A5: d in the carrier of R and A6: z = [c,d] by ZFMISC_1:def_2; reconsider c = c, d = d as Nat by A1, A4, A5, NECKLACE:3; ( c < n & d < n ) by A1, A4, A5, NAT_1:44; then ( c < (2 * n) + 1 & d < (2 * n) + 1 ) by A2, XXREAL_0:2; then ( c in (2 * n) + 1 & d in (2 * n) + 1 ) by NAT_1:44; hence z in [:((2 * n) + 1),((2 * n) + 1):] by A6, ZFMISC_1:def_2; ::_thesis: verum end; suppose z in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: z in [:((2 * n) + 1),((2 * n) + 1):] then consider x, y being Element of NAT such that A7: z = [x,(y + n)] and A8: [x,y] in the InternalRel of R ; x in the carrier of R by A8, ZFMISC_1:87; then x < n by A1, NAT_1:44; then x < (2 * n) + 1 by A2, XXREAL_0:2; then A9: x in (2 * n) + 1 by NAT_1:44; y in the carrier of R by A8, ZFMISC_1:87; then y < n by A1, NAT_1:44; then y + n < n + n by XREAL_1:6; then y + n < (2 * n) + 1 by NAT_1:13; then y + n in (2 * n) + 1 by NAT_1:44; hence z in [:((2 * n) + 1),((2 * n) + 1):] by A7, A9, ZFMISC_1:def_2; ::_thesis: verum end; suppose z in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: z in [:((2 * n) + 1),((2 * n) + 1):] then consider x, y being Element of NAT such that A10: z = [(x + n),y] and A11: [x,y] in the InternalRel of R ; y in the carrier of R by A11, ZFMISC_1:87; then y < n by A1, NAT_1:44; then y < (2 * n) + 1 by A2, XXREAL_0:2; then A12: y in (2 * n) + 1 by NAT_1:44; x in the carrier of R by A11, ZFMISC_1:87; then x < n by A1, NAT_1:44; then x + n < n + n by XREAL_1:6; then x + n < (2 * n) + 1 by NAT_1:13; then x + n in (2 * n) + 1 by NAT_1:44; hence z in [:((2 * n) + 1),((2 * n) + 1):] by A10, A12, ZFMISC_1:def_2; ::_thesis: verum end; suppose z in [:{(2 * n)},((2 * n) \ n):] ; ::_thesis: z in [:((2 * n) + 1),((2 * n) + 1):] then consider c, d being set such that A13: c in {(2 * n)} and A14: d in (2 * n) \ n and A15: z = [c,d] by ZFMISC_1:def_2; A16: c = 2 * n by A13, TARSKI:def_1; reconsider c = c as Nat by A13, TARSKI:def_1; c < (2 * n) + 1 by A16, NAT_1:13; then A17: c in (2 * n) + 1 by NAT_1:44; reconsider d = d as Nat by A14, NECKLACE:3; d < 2 * n by A14, Th2; then d < (2 * n) + 1 by NAT_1:13; then d in (2 * n) + 1 by NAT_1:44; hence z in [:((2 * n) + 1),((2 * n) + 1):] by A17, A15, ZFMISC_1:def_2; ::_thesis: verum end; suppose z in [:((2 * n) \ n),{(2 * n)}:] ; ::_thesis: z in [:((2 * n) + 1),((2 * n) + 1):] then consider c, d being set such that A18: c in (2 * n) \ n and A19: d in {(2 * n)} and A20: z = [c,d] by ZFMISC_1:def_2; A21: d = 2 * n by A19, TARSKI:def_1; reconsider d = d as Nat by A19, TARSKI:def_1; d < (2 * n) + 1 by A21, NAT_1:13; then A22: d in (2 * n) + 1 by NAT_1:44; reconsider c = c as Nat by A18, NECKLACE:3; c < 2 * n by A18, Th2; then c < (2 * n) + 1 by NAT_1:13; then c in (2 * n) + 1 by NAT_1:44; hence z in [:((2 * n) + 1),((2 * n) + 1):] by A22, A20, ZFMISC_1:def_2; ::_thesis: verum end; end; end; then reconsider iMR = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] as Relation of ((2 * n) + 1) ; set MR = RelStr(# ((2 * n) + 1),iMR #); take RelStr(# ((2 * n) + 1),iMR #) ; ::_thesis: ( RelStr(# ((2 * n) + 1),iMR #) is NatRelStr of (2 * n) + 1 & the InternalRel of RelStr(# ((2 * n) + 1),iMR #) = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] ) thus the carrier of RelStr(# ((2 * n) + 1),iMR #) = (2 * n) + 1 ; :: according to MYCIELSK:def_7 ::_thesis: the InternalRel of RelStr(# ((2 * n) + 1),iMR #) = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] thus the InternalRel of RelStr(# ((2 * n) + 1),iMR #) = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] ; ::_thesis: verum end; uniqueness for b1, b2 being NatRelStr of (2 * n) + 1 st the InternalRel of b1 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] & the InternalRel of b2 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] holds b1 = b2 proof let A, B be NatRelStr of (2 * n) + 1; ::_thesis: ( the InternalRel of A = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] & the InternalRel of B = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] implies A = B ) ( the carrier of A = (2 * n) + 1 & the carrier of B = (2 * n) + 1 ) by Def7; hence ( the InternalRel of A = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] & the InternalRel of B = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] implies A = B ) ; ::_thesis: verum end; end; :: deftheorem Def9 defines Mycielskian MYCIELSK:def_9_:_ for n being Nat for R being NatRelStr of n for b3 being NatRelStr of (2 * n) + 1 holds ( b3 = Mycielskian R iff the InternalRel of b3 = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] ); theorem Th37: :: MYCIELSK:37 for n being Nat for R being NatRelStr of n holds the carrier of R c= the carrier of (Mycielskian R) proof let n be Nat; ::_thesis: for R being NatRelStr of n holds the carrier of R c= the carrier of (Mycielskian R) let R be NatRelStr of n; ::_thesis: the carrier of R c= the carrier of (Mycielskian R) A1: the carrier of R = n by Def7; n <= n + n by NAT_1:12; then n <= (2 * n) + 1 by NAT_1:12; then n c= (2 * n) + 1 by NAT_1:39; hence the carrier of R c= the carrier of (Mycielskian R) by A1, Def7; ::_thesis: verum end; theorem Th38: :: MYCIELSK:38 for n being Nat for R being NatRelStr of n for x, y being Nat holds ( not [x,y] in the InternalRel of (Mycielskian R) or ( x < n & y < n ) or ( x < n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y < n ) or ( x = 2 * n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y = 2 * n ) ) proof let n be Nat; ::_thesis: for R being NatRelStr of n for x, y being Nat holds ( not [x,y] in the InternalRel of (Mycielskian R) or ( x < n & y < n ) or ( x < n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y < n ) or ( x = 2 * n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y = 2 * n ) ) let R be NatRelStr of n; ::_thesis: for x, y being Nat holds ( not [x,y] in the InternalRel of (Mycielskian R) or ( x < n & y < n ) or ( x < n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y < n ) or ( x = 2 * n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y = 2 * n ) ) let a, b be Nat; ::_thesis: ( not [a,b] in the InternalRel of (Mycielskian R) or ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) ) set cR = the carrier of R; set iR = the InternalRel of R; defpred S1[] means [a,b] in the InternalRel of (Mycielskian R); defpred S2[] means ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) ); A1: the InternalRel of (Mycielskian R) = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] by Def9; assume A2: S1[] ; ::_thesis: ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) ) percases ( [a,b] in the InternalRel of R or [a,b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,b] in [:{(2 * n)},((2 * n) \ n):] or [a,b] in [:((2 * n) \ n),{(2 * n)}:] ) by A2, A1, Th4; suppose [a,b] in the InternalRel of R ; ::_thesis: ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) ) then ( a in the carrier of R & b in the carrier of R ) by ZFMISC_1:87; then ( a in n & b in n ) by Def7; hence S2[] by NAT_1:44; ::_thesis: verum end; suppose [a,b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) ) then consider x, y being Element of NAT such that A3: [x,(y + n)] = [a,b] and A4: [x,y] in the InternalRel of R ; y in the carrier of R by A4, ZFMISC_1:87; then y in n by Def7; then y < n by NAT_1:44; then A5: y + n < n + n by XREAL_1:6; x in the carrier of R by A4, ZFMISC_1:87; then x in n by Def7; then x < n by NAT_1:44; hence S2[] by A5, A3, XTUPLE_0:1; ::_thesis: verum end; suppose [a,b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) ) then consider x, y being Element of NAT such that A6: [(x + n),y] = [a,b] and A7: [x,y] in the InternalRel of R ; x in the carrier of R by A7, ZFMISC_1:87; then x in n by Def7; then x < n by NAT_1:44; then A8: x + n < n + n by XREAL_1:6; y in the carrier of R by A7, ZFMISC_1:87; then y in n by Def7; then y < n by NAT_1:44; hence S2[] by A8, A6, XTUPLE_0:1; ::_thesis: verum end; supposeA9: [a,b] in [:{(2 * n)},((2 * n) \ n):] ; ::_thesis: ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) ) A10: b in (2 * n) \ n by A9, ZFMISC_1:87; a in {(2 * n)} by A9, ZFMISC_1:87; hence S2[] by A10, Th2, TARSKI:def_1; ::_thesis: verum end; supposeA11: [a,b] in [:((2 * n) \ n),{(2 * n)}:] ; ::_thesis: ( ( a < n & b < n ) or ( a < n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b < n ) or ( a = 2 * n & n <= b & b < 2 * n ) or ( n <= a & a < 2 * n & b = 2 * n ) ) A12: a in (2 * n) \ n by A11, ZFMISC_1:87; b in {(2 * n)} by A11, ZFMISC_1:87; hence S2[] by A12, Th2, TARSKI:def_1; ::_thesis: verum end; end; end; theorem Th39: :: MYCIELSK:39 for n being Nat for R being NatRelStr of n holds the InternalRel of R c= the InternalRel of (Mycielskian R) proof let n be Nat; ::_thesis: for R being NatRelStr of n holds the InternalRel of R c= the InternalRel of (Mycielskian R) let R be NatRelStr of n; ::_thesis: the InternalRel of R c= the InternalRel of (Mycielskian R) set iR = the InternalRel of R; set MR = Mycielskian R; set iMR = the InternalRel of (Mycielskian R); the InternalRel of (Mycielskian R) = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] by Def9; hence the InternalRel of R c= the InternalRel of (Mycielskian R) by Th3; ::_thesis: verum end; theorem Th40: :: MYCIELSK:40 for n being Nat for R being NatRelStr of n for x, y being set st x in n & y in n & [x,y] in the InternalRel of (Mycielskian R) holds [x,y] in the InternalRel of R proof let n be Nat; ::_thesis: for R being NatRelStr of n for x, y being set st x in n & y in n & [x,y] in the InternalRel of (Mycielskian R) holds [x,y] in the InternalRel of R let R be NatRelStr of n; ::_thesis: for x, y being set st x in n & y in n & [x,y] in the InternalRel of (Mycielskian R) holds [x,y] in the InternalRel of R let a, b be set ; ::_thesis: ( a in n & b in n & [a,b] in the InternalRel of (Mycielskian R) implies [a,b] in the InternalRel of R ) assume that A1: a in n and A2: b in n and A3: [a,b] in the InternalRel of (Mycielskian R) ; ::_thesis: [a,b] in the InternalRel of R set iR = the InternalRel of R; set MR = Mycielskian R; set iMR = the InternalRel of (Mycielskian R); A4: the InternalRel of (Mycielskian R) = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] by Def9; percases ( [a,b] in the InternalRel of R or [a,b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,b] in [:{(2 * n)},((2 * n) \ n):] or [a,b] in [:((2 * n) \ n),{(2 * n)}:] ) by A3, A4, Th4; suppose [a,b] in the InternalRel of R ; ::_thesis: [a,b] in the InternalRel of R hence [a,b] in the InternalRel of R ; ::_thesis: verum end; suppose [a,b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: [a,b] in the InternalRel of R then consider x, y being Element of NAT such that A5: [a,b] = [x,(y + n)] and [x,y] in the InternalRel of R ; b = y + n by A5, XTUPLE_0:1; then y + n < n by A2, NAT_1:44; then y < n - n by XREAL_1:20; then y < 0 ; hence [a,b] in the InternalRel of R ; ::_thesis: verum end; suppose [a,b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: [a,b] in the InternalRel of R then consider x, y being Element of NAT such that A6: [a,b] = [(x + n),y] and [x,y] in the InternalRel of R ; a = x + n by A6, XTUPLE_0:1; then x + n < n by A1, NAT_1:44; then x < n - n by XREAL_1:20; then x < 0 ; hence [a,b] in the InternalRel of R ; ::_thesis: verum end; suppose [a,b] in [:{(2 * n)},((2 * n) \ n):] ; ::_thesis: [a,b] in the InternalRel of R then consider c, d being set such that A7: c in {(2 * n)} and d in (2 * n) \ n and A8: [a,b] = [c,d] by ZFMISC_1:def_2; A9: c = 2 * n by A7, TARSKI:def_1; A10: c = a by A8, XTUPLE_0:1; n + n < n by A1, A10, A9, NAT_1:44; then n < n - n by XREAL_1:20; then n < 0 ; hence [a,b] in the InternalRel of R ; ::_thesis: verum end; suppose [a,b] in [:((2 * n) \ n),{(2 * n)}:] ; ::_thesis: [a,b] in the InternalRel of R then consider c, d being set such that c in (2 * n) \ n and A11: d in {(2 * n)} and A12: [a,b] = [c,d] by ZFMISC_1:def_2; A13: d = 2 * n by A11, TARSKI:def_1; A14: d = b by A12, XTUPLE_0:1; n + n < n by A2, A14, A13, NAT_1:44; then n < n - n by XREAL_1:20; then n < 0 ; hence [a,b] in the InternalRel of R ; ::_thesis: verum end; end; end; theorem Th41: :: MYCIELSK:41 for n being Nat for R being NatRelStr of n for x, y being Nat st [x,y] in the InternalRel of R holds ( [x,(y + n)] in the InternalRel of (Mycielskian R) & [(x + n),y] in the InternalRel of (Mycielskian R) ) proof let n be Nat; ::_thesis: for R being NatRelStr of n for x, y being Nat st [x,y] in the InternalRel of R holds ( [x,(y + n)] in the InternalRel of (Mycielskian R) & [(x + n),y] in the InternalRel of (Mycielskian R) ) let R be NatRelStr of n; ::_thesis: for x, y being Nat st [x,y] in the InternalRel of R holds ( [x,(y + n)] in the InternalRel of (Mycielskian R) & [(x + n),y] in the InternalRel of (Mycielskian R) ) let a, b be Nat; ::_thesis: ( [a,b] in the InternalRel of R implies ( [a,(b + n)] in the InternalRel of (Mycielskian R) & [(a + n),b] in the InternalRel of (Mycielskian R) ) ) assume A1: [a,b] in the InternalRel of R ; ::_thesis: ( [a,(b + n)] in the InternalRel of (Mycielskian R) & [(a + n),b] in the InternalRel of (Mycielskian R) ) set iR = the InternalRel of R; set MR = Mycielskian R; set iMR = the InternalRel of (Mycielskian R); A2: the InternalRel of (Mycielskian R) = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] by Def9; reconsider ap1 = a, bp1 = b as Element of NAT by ORDINAL1:def_12; [ap1,(bp1 + n)] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } by A1; hence [a,(b + n)] in the InternalRel of (Mycielskian R) by A2, Th4; ::_thesis: [(a + n),b] in the InternalRel of (Mycielskian R) [(ap1 + n),bp1] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } by A1; hence [(a + n),b] in the InternalRel of (Mycielskian R) by A2, Th4; ::_thesis: verum end; theorem Th42: :: MYCIELSK:42 for n being Nat for R being NatRelStr of n for x, y being Nat st x in n & [x,(y + n)] in the InternalRel of (Mycielskian R) holds [x,y] in the InternalRel of R proof let n be Nat; ::_thesis: for R being NatRelStr of n for x, y being Nat st x in n & [x,(y + n)] in the InternalRel of (Mycielskian R) holds [x,y] in the InternalRel of R let R be NatRelStr of n; ::_thesis: for x, y being Nat st x in n & [x,(y + n)] in the InternalRel of (Mycielskian R) holds [x,y] in the InternalRel of R let a, b be Nat; ::_thesis: ( a in n & [a,(b + n)] in the InternalRel of (Mycielskian R) implies [a,b] in the InternalRel of R ) set cR = the carrier of R; set iR = the InternalRel of R; set MR = Mycielskian R; set iMR = the InternalRel of (Mycielskian R); assume that A1: a in n and A2: [a,(b + n)] in the InternalRel of (Mycielskian R) ; ::_thesis: [a,b] in the InternalRel of R A3: the InternalRel of (Mycielskian R) = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] by Def9; percases ( [a,(b + n)] in the InternalRel of R or [a,(b + n)] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,(b + n)] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [a,(b + n)] in [:{(2 * n)},((2 * n) \ n):] or [a,(b + n)] in [:((2 * n) \ n),{(2 * n)}:] ) by A2, A3, Th4; suppose [a,(b + n)] in the InternalRel of R ; ::_thesis: [a,b] in the InternalRel of R then b + n in the carrier of R by ZFMISC_1:87; then b + n in n by Def7; then b + n < n by NAT_1:44; then b < n - n by XREAL_1:20; then b < 0 ; hence [a,b] in the InternalRel of R ; ::_thesis: verum end; suppose [a,(b + n)] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: [a,b] in the InternalRel of R then consider x, y being Element of NAT such that A4: [a,(b + n)] = [x,(y + n)] and A5: [x,y] in the InternalRel of R ; b + n = y + n by A4, XTUPLE_0:1; hence [a,b] in the InternalRel of R by A5, A4, XTUPLE_0:1; ::_thesis: verum end; suppose [a,(b + n)] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: [a,b] in the InternalRel of R then consider x, y being Element of NAT such that A6: [a,(b + n)] = [(x + n),y] and A7: [x,y] in the InternalRel of R ; b + n = y by A6, XTUPLE_0:1; then b + n in the carrier of R by A7, ZFMISC_1:87; then b + n in n by Def7; then b + n < n by NAT_1:44; then b < n - n by XREAL_1:20; then b < 0 ; hence [a,b] in the InternalRel of R ; ::_thesis: verum end; suppose [a,(b + n)] in [:{(2 * n)},((2 * n) \ n):] ; ::_thesis: [a,b] in the InternalRel of R then consider c, d being set such that A8: c in {(2 * n)} and d in (2 * n) \ n and A9: [a,(b + n)] = [c,d] by ZFMISC_1:def_2; A10: c = 2 * n by A8, TARSKI:def_1; A11: c = a by A9, XTUPLE_0:1; n + n < n by A1, A11, A10, NAT_1:44; then n < n - n by XREAL_1:20; then n < 0 ; hence [a,b] in the InternalRel of R ; ::_thesis: verum end; suppose [a,(b + n)] in [:((2 * n) \ n),{(2 * n)}:] ; ::_thesis: [a,b] in the InternalRel of R then consider c, d being set such that A12: c in (2 * n) \ n and d in {(2 * n)} and A13: [a,(b + n)] = [c,d] by ZFMISC_1:def_2; c = a by A13, XTUPLE_0:1; then n <= a by A12, Th2; hence [a,b] in the InternalRel of R by A1, NAT_1:44; ::_thesis: verum end; end; end; theorem Th43: :: MYCIELSK:43 for n being Nat for R being NatRelStr of n for x, y being Nat st y in n & [(x + n),y] in the InternalRel of (Mycielskian R) holds [x,y] in the InternalRel of R proof let n be Nat; ::_thesis: for R being NatRelStr of n for x, y being Nat st y in n & [(x + n),y] in the InternalRel of (Mycielskian R) holds [x,y] in the InternalRel of R let R be NatRelStr of n; ::_thesis: for x, y being Nat st y in n & [(x + n),y] in the InternalRel of (Mycielskian R) holds [x,y] in the InternalRel of R let a, b be Nat; ::_thesis: ( b in n & [(a + n),b] in the InternalRel of (Mycielskian R) implies [a,b] in the InternalRel of R ) set cR = the carrier of R; set iR = the InternalRel of R; set MR = Mycielskian R; set iMR = the InternalRel of (Mycielskian R); assume that A1: b in n and A2: [(a + n),b] in the InternalRel of (Mycielskian R) ; ::_thesis: [a,b] in the InternalRel of R A3: the InternalRel of (Mycielskian R) = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] by Def9; percases ( [(a + n),b] in the InternalRel of R or [(a + n),b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [(a + n),b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } or [(a + n),b] in [:{(2 * n)},((2 * n) \ n):] or [(a + n),b] in [:((2 * n) \ n),{(2 * n)}:] ) by A2, A3, Th4; suppose [(a + n),b] in the InternalRel of R ; ::_thesis: [a,b] in the InternalRel of R then a + n in the carrier of R by ZFMISC_1:87; then a + n in n by Def7; then a + n < n by NAT_1:44; then a < n - n by XREAL_1:20; then a < 0 ; hence [a,b] in the InternalRel of R ; ::_thesis: verum end; suppose [(a + n),b] in { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: [a,b] in the InternalRel of R then consider x, y being Element of NAT such that A4: [(a + n),b] = [x,(y + n)] and A5: [x,y] in the InternalRel of R ; a + n = x by A4, XTUPLE_0:1; then a + n in the carrier of R by A5, ZFMISC_1:87; then a + n in n by Def7; then a + n < n by NAT_1:44; then a < n - n by XREAL_1:20; then a < 0 ; hence [a,b] in the InternalRel of R ; ::_thesis: verum end; suppose [(a + n),b] in { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ; ::_thesis: [a,b] in the InternalRel of R then consider x, y being Element of NAT such that A6: [(a + n),b] = [(x + n),y] and A7: [x,y] in the InternalRel of R ; a + n = x + n by A6, XTUPLE_0:1; hence [a,b] in the InternalRel of R by A7, A6, XTUPLE_0:1; ::_thesis: verum end; suppose [(a + n),b] in [:{(2 * n)},((2 * n) \ n):] ; ::_thesis: [a,b] in the InternalRel of R then consider c, d being set such that c in {(2 * n)} and A8: d in (2 * n) \ n and A9: [(a + n),b] = [c,d] by ZFMISC_1:def_2; b = d by A9, XTUPLE_0:1; then n <= b by A8, Th2; hence [a,b] in the InternalRel of R by A1, NAT_1:44; ::_thesis: verum end; suppose [(a + n),b] in [:((2 * n) \ n),{(2 * n)}:] ; ::_thesis: [a,b] in the InternalRel of R then consider c, d being set such that c in (2 * n) \ n and A10: d in {(2 * n)} and A11: [(a + n),b] = [c,d] by ZFMISC_1:def_2; A12: d = 2 * n by A10, TARSKI:def_1; d = b by A11, XTUPLE_0:1; then n + n < n by A1, A12, NAT_1:44; then n < n - n by XREAL_1:20; then n < 0 ; hence [a,b] in the InternalRel of R ; ::_thesis: verum end; end; end; theorem Th44: :: MYCIELSK:44 for n being Nat for R being NatRelStr of n for m being Nat st n <= m & m < 2 * n holds ( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) ) proof let n be Nat; ::_thesis: for R being NatRelStr of n for m being Nat st n <= m & m < 2 * n holds ( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) ) let R be NatRelStr of n; ::_thesis: for m being Nat st n <= m & m < 2 * n holds ( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) ) let m be Nat; ::_thesis: ( n <= m & m < 2 * n implies ( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) ) ) assume that A1: n <= m and A2: m < 2 * n ; ::_thesis: ( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) ) set iR = the InternalRel of R; set MR = Mycielskian R; set iMR = the InternalRel of (Mycielskian R); A3: the InternalRel of (Mycielskian R) = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] by Def9; A4: m in (2 * n) \ n by A1, A2, Th2; A5: 2 * n in {(2 * n)} by TARSKI:def_1; then [m,(2 * n)] in [:((2 * n) \ n),{(2 * n)}:] by A4, ZFMISC_1:def_2; hence [m,(2 * n)] in the InternalRel of (Mycielskian R) by A3, XBOOLE_0:def_3; ::_thesis: [(2 * n),m] in the InternalRel of (Mycielskian R) [(2 * n),m] in [:{(2 * n)},((2 * n) \ n):] by A4, A5, ZFMISC_1:def_2; hence [(2 * n),m] in the InternalRel of (Mycielskian R) by A3, Th4; ::_thesis: verum end; theorem Th45: :: MYCIELSK:45 for n being Nat for R being NatRelStr of n for S being Subset of (Mycielskian R) st S = n holds R = subrelstr S proof let n be Nat; ::_thesis: for R being NatRelStr of n for S being Subset of (Mycielskian R) st S = n holds R = subrelstr S let R be NatRelStr of n; ::_thesis: for S being Subset of (Mycielskian R) st S = n holds R = subrelstr S let S be Subset of (Mycielskian R); ::_thesis: ( S = n implies R = subrelstr S ) assume A1: S = n ; ::_thesis: R = subrelstr S set cR = the carrier of R; set iR = the InternalRel of R; set sS = subrelstr S; set csS = the carrier of (subrelstr S); set isS = the InternalRel of (subrelstr S); set MR = Mycielskian R; set cMR = the carrier of (Mycielskian R); set iMR = the InternalRel of (Mycielskian R); A2: the carrier of R = n by Def7; A3: the carrier of (subrelstr S) = n by A1, YELLOW_0:def_15; A4: the InternalRel of R = the InternalRel of (subrelstr S) proof thus the InternalRel of R c= the InternalRel of (subrelstr S) :: according to XBOOLE_0:def_10 ::_thesis: the InternalRel of (subrelstr S) c= the InternalRel of R proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the InternalRel of R or z in the InternalRel of (subrelstr S) ) assume A5: z in the InternalRel of R ; ::_thesis: z in the InternalRel of (subrelstr S) then consider x, y being set such that A6: x in the carrier of R and A7: y in the carrier of R and A8: z = [x,y] by ZFMISC_1:def_2; the carrier of R c= the carrier of (Mycielskian R) by Th37; then reconsider xMR = x, yMR = y as Element of (Mycielskian R) by A6, A7; reconsider xsS = x, ysS = y as Element of (subrelstr S) by A6, A7, Def7, A3; the InternalRel of R c= the InternalRel of (Mycielskian R) by Th39; then xMR <= yMR by A5, A8, ORDERS_2:def_5; then xsS <= ysS by A3, A2, A7, YELLOW_0:60; hence z in the InternalRel of (subrelstr S) by A8, ORDERS_2:def_5; ::_thesis: verum end; thus the InternalRel of (subrelstr S) c= the InternalRel of R ::_thesis: verum proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the InternalRel of (subrelstr S) or z in the InternalRel of R ) assume A9: z in the InternalRel of (subrelstr S) ; ::_thesis: z in the InternalRel of R then consider x, y being set such that A10: x in the carrier of (subrelstr S) and A11: y in the carrier of (subrelstr S) and A12: z = [x,y] by ZFMISC_1:def_2; the carrier of R c= the carrier of (Mycielskian R) by Th37; then reconsider xMR = x, yMR = y as Element of (Mycielskian R) by A10, A11, A2, A3; reconsider xsS = x, ysS = y as Element of (subrelstr S) by A10, A11; xsS <= ysS by A9, A12, ORDERS_2:def_5; then xMR <= yMR by YELLOW_0:59; then z in the InternalRel of (Mycielskian R) by A12, ORDERS_2:def_5; hence z in the InternalRel of R by A10, A11, A3, A12, Th40; ::_thesis: verum end; end; thus R = subrelstr S by Def7, A3, A4; ::_thesis: verum end; theorem Th46: :: MYCIELSK:46 for n being Nat for R being irreflexive NatRelStr of n st 2 <= clique# R holds clique# R = clique# (Mycielskian R) proof let n be Nat; ::_thesis: for R being irreflexive NatRelStr of n st 2 <= clique# R holds clique# R = clique# (Mycielskian R) let R be irreflexive NatRelStr of n; ::_thesis: ( 2 <= clique# R implies clique# R = clique# (Mycielskian R) ) assume that A1: 2 <= clique# R and A2: clique# R <> clique# (Mycielskian R) ; ::_thesis: contradiction set cR = the carrier of R; set iR = the InternalRel of R; set MR = Mycielskian R; set cMR = the carrier of (Mycielskian R); set iMR = the InternalRel of (Mycielskian R); set cnMR = clique# (Mycielskian R); A3: the carrier of R = n by Def7; A4: the carrier of R c= the carrier of (Mycielskian R) by Th37; consider C being finite Clique of R such that A5: card C = clique# R by DILWORTH:def_4; n <= n + n by NAT_1:11; then n < (2 * n) + 1 by NAT_1:13; then n c= (2 * n) + 1 by NAT_1:39; then reconsider S = n as Subset of (Mycielskian R) by Def7; A6: R = subrelstr S by Th45; then C is Clique of (Mycielskian R) by DILWORTH:28; then card C <= clique# (Mycielskian R) by DILWORTH:def_4; then A7: clique# R < clique# (Mycielskian R) by A2, A5, XXREAL_0:1; then 2 < clique# (Mycielskian R) by A1, XXREAL_0:2; then A8: 2 + 1 <= clique# (Mycielskian R) by NAT_1:13; consider D being finite Clique of (Mycielskian R) such that A9: card D = clique# (Mycielskian R) by DILWORTH:def_4; percases ( D c= n or not D c= n ) ; supposeA10: D c= n ; ::_thesis: contradiction D /\ S is Clique of R by A6, DILWORTH:29; then D is Clique of R by A10, XBOOLE_1:28; hence contradiction by A9, A7, DILWORTH:def_4; ::_thesis: verum end; suppose not D c= n ; ::_thesis: contradiction then consider x being set such that A11: x in D and A12: not x in n by TARSKI:def_3; x in the carrier of (Mycielskian R) by A11; then A13: x in (2 * n) + 1 by Def7; reconsider x = x as Nat by A13, NECKLACE:3; reconsider xp1 = x as Element of (Mycielskian R) by A11; A14: x >= n by A12, NAT_1:44; x < (2 * n) + 1 by A13, NAT_1:44; then A15: x <= 2 * n by NAT_1:13; A16: for y being set st y in D & x <> y holds y in n proof let y be set ; ::_thesis: ( y in D & x <> y implies y in n ) assume that A17: y in D and A18: x <> y and A19: not y in n ; ::_thesis: contradiction y in the carrier of (Mycielskian R) by A17; then A20: y in (2 * n) + 1 by Def7; reconsider y = y as Nat by A20, NECKLACE:3; reconsider yp1 = y as Element of (Mycielskian R) by A17; A21: y >= n by A19, NAT_1:44; y < (2 * n) + 1 by A20, NAT_1:44; then A22: y <= 2 * n by NAT_1:13; set DD = D \ {x,y}; {x,y} c= D by A17, A11, ZFMISC_1:32; then A23: card (D \ {x,y}) = (card D) - (card {x,y}) by CARD_2:44; (1 + 2) - 2 <= (card D) - 2 by A8, A9, XREAL_1:9; then 1 <= card (D \ {x,y}) by A23, A18, CARD_2:57; then consider z being set such that A24: z in D \ {x,y} by CARD_1:27, XBOOLE_0:def_1; A25: z in D by A24, XBOOLE_0:def_5; A26: z in the carrier of (Mycielskian R) by A24; reconsider zp1 = z as Element of (Mycielskian R) by A24; A27: z in (2 * n) + 1 by A26, Def7; reconsider z = z as Nat by A27, NECKLACE:3; x in {x,y} by TARSKI:def_2; then A28: z <> x by A24, XBOOLE_0:def_5; y in {x,y} by TARSKI:def_2; then A29: z <> y by A24, XBOOLE_0:def_5; percases ( ( x < 2 * n & y < 2 * n ) or ( x < 2 * n & y = 2 * n ) or ( x = 2 * n & y < 2 * n ) or ( x = 2 * n & y = 2 * n ) ) by A15, A22, XXREAL_0:1; supposeA30: ( x < 2 * n & y < 2 * n ) ; ::_thesis: contradiction ( xp1 <= yp1 or yp1 <= xp1 ) by A11, A17, A18, DILWORTH:6; then ( [x,y] in the InternalRel of (Mycielskian R) or [y,x] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5; hence contradiction by A14, A30, A21, Th38; ::_thesis: verum end; supposeA31: ( x < 2 * n & y = 2 * n ) ; ::_thesis: contradiction ( xp1 <= zp1 or zp1 <= xp1 ) by A28, A25, A11, DILWORTH:6; then A32: ( [x,z] in the InternalRel of (Mycielskian R) or [z,x] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5; ( yp1 <= zp1 or zp1 <= yp1 ) by A29, A25, A17, DILWORTH:6; then ( [y,z] in the InternalRel of (Mycielskian R) or [z,y] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5; then ( n <= z & z < 2 * n ) by A31, A21, Th38; hence contradiction by A32, A31, A14, Th38; ::_thesis: verum end; supposeA33: ( x = 2 * n & y < 2 * n ) ; ::_thesis: contradiction ( yp1 <= zp1 or zp1 <= yp1 ) by A29, A25, A17, DILWORTH:6; then A34: ( [y,z] in the InternalRel of (Mycielskian R) or [z,y] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5; ( xp1 <= zp1 or zp1 <= xp1 ) by A28, A25, A11, DILWORTH:6; then ( [x,z] in the InternalRel of (Mycielskian R) or [z,x] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5; then ( n <= z & z < 2 * n ) by A33, A14, Th38; hence contradiction by A34, A33, A21, Th38; ::_thesis: verum end; suppose ( x = 2 * n & y = 2 * n ) ; ::_thesis: contradiction hence contradiction by A18; ::_thesis: verum end; end; end; A35: card (D \ {x}) = (card D) - (card {x}) by A11, EULER_1:4 .= (card D) - 1 by CARD_1:30 ; percases ( x < 2 * n or x = 2 * n ) by A15, XXREAL_0:1; supposeA36: x < 2 * n ; ::_thesis: contradiction consider xx being Nat such that A37: x = n + xx by A14, NAT_1:10; n + xx < n + n by A36, A37; then A38: xx < n by XREAL_1:6; then A39: xx in n by NAT_1:44; reconsider xxp1 = xx as Element of (Mycielskian R) by A39, A4, A3; A40: now__::_thesis:_not_xx_in_D assume xx in D ; ::_thesis: contradiction then ( xp1 <= xxp1 or xxp1 <= xp1 ) by A11, A38, A14, DILWORTH:6; then ( [x,xx] in the InternalRel of (Mycielskian R) or [xx,x] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5; then ( [xx,xx] in the InternalRel of R or [xx,xx] in the InternalRel of R ) by A39, A37, Th42, Th43; hence contradiction by A39, A3, NECKLACE:def_5; ::_thesis: verum end; set DD = (D \ {x}) \/ {xx}; (D \ {x}) \/ {xx} c= the carrier of R proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (D \ {x}) \/ {xx} or a in the carrier of R ) assume a in (D \ {x}) \/ {xx} ; ::_thesis: a in the carrier of R then ( a in D \ {x} or a in {xx} ) by XBOOLE_0:def_3; then ( ( a in D & not a in {x} ) or a = xx ) by TARSKI:def_1, XBOOLE_0:def_5; then ( ( a in D & a <> x ) or a = xx ) by TARSKI:def_1; hence a in the carrier of R by A38, A16, A3, NAT_1:44; ::_thesis: verum end; then reconsider DD = (D \ {x}) \/ {xx} as Subset of R ; now__::_thesis:_for_a,_b_being_Element_of_R_st_a_in_DD_&_b_in_DD_&_a_<>_b_&_not_a_<=_b_holds_ b_<=_a let a, b be Element of R; ::_thesis: ( a in DD & b in DD & a <> b & not b1 <= b2 implies b2 <= b1 ) assume that A41: a in DD and A42: b in DD and A43: a <> b ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) ( a in D \ {x} or a in {xx} ) by A41, XBOOLE_0:def_3; then A44: ( ( a in D & not a in {x} ) or a = xx ) by TARSKI:def_1, XBOOLE_0:def_5; ( b in D \ {x} or b in {xx} ) by A42, XBOOLE_0:def_3; then A45: ( ( b in D & not b in {x} ) or b = xx ) by TARSKI:def_1, XBOOLE_0:def_5; A46: ( a in the carrier of R & b in the carrier of R ) by A41; reconsider an = a, bn = b as Nat by A41, A3, NECKLACE:3; reconsider ap1 = a, bp1 = b as Element of (Mycielskian R) by A46, A4; percases ( ( a in D & a <> x & b in D & b <> x ) or ( a in D & a <> x & b = xx ) or ( a = xx & b in D & b <> x ) ) by A43, A44, A45, TARSKI:def_1; supposeA47: ( a in D & a <> x & b in D & b <> x ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) ( ap1 <= bp1 or bp1 <= ap1 ) by A47, A43, DILWORTH:6; hence ( a <= b or b <= a ) by A6, A41, YELLOW_0:60; ::_thesis: verum end; supposeA48: ( a in D & a <> x & b = xx ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) ( ap1 <= xp1 or xp1 <= ap1 ) by A48, A11, DILWORTH:6; then ( [ap1,x] in the InternalRel of (Mycielskian R) or [x,ap1] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5; then ( [an,xx] in the InternalRel of R or [xx,an] in the InternalRel of R ) by A3, A38, A37, Th42, Th43; hence ( a <= b or b <= a ) by A48, ORDERS_2:def_5; ::_thesis: verum end; supposeA49: ( a = xx & b in D & b <> x ) ; ::_thesis: ( b1 <= b2 or b2 <= b1 ) ( bp1 <= xp1 or xp1 <= bp1 ) by A49, A11, DILWORTH:6; then ( [bp1,x] in the InternalRel of (Mycielskian R) or [x,bp1] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5; then ( [bn,xx] in the InternalRel of R or [xx,bn] in the InternalRel of R ) by A3, A38, A37, Th42, Th43; hence ( a <= b or b <= a ) by A49, ORDERS_2:def_5; ::_thesis: verum end; end; end; then reconsider DD = DD as Clique of R by DILWORTH:6; A50: not xx in D \ {x} by A40, XBOOLE_0:def_5; card DD = ((card D) - 1) + 1 by A50, A35, CARD_2:41 .= card D ; hence contradiction by A9, A7, DILWORTH:def_4; ::_thesis: verum end; supposeA51: x = 2 * n ; ::_thesis: contradiction (2 + 1) - 1 <= (card D) - 1 by A9, A8, XREAL_1:9; then 2 c= card (D \ {x}) by A35, NAT_1:39; then consider y, z being set such that A52: y in D \ {x} and z in D \ {x} and y <> z by PENCIL_1:2; A53: y in D by A52, ZFMISC_1:56; A54: x <> y by A52, ZFMISC_1:56; y in the carrier of (Mycielskian R) by A52; then y in (2 * n) + 1 by Def7; then reconsider y = y as Nat by NECKLACE:3; reconsider yp1 = y as Element of (Mycielskian R) by A52; ( yp1 <= xp1 or xp1 <= yp1 ) by A54, A53, A11, DILWORTH:6; then A55: ( [y,x] in the InternalRel of (Mycielskian R) or [x,y] in the InternalRel of (Mycielskian R) ) by ORDERS_2:def_5; y in n by A16, A53, A54; then A56: y < n by NAT_1:44; n <= n + n by NAT_1:11; hence contradiction by A55, A51, A56, Th38; ::_thesis: verum end; end; end; end; end; theorem Th47: :: MYCIELSK:47 for R being with_finite_chromatic# RelStr for S being Subset of R holds chromatic# R >= chromatic# (subrelstr S) proof let R be with_finite_chromatic# RelStr ; ::_thesis: for S being Subset of R holds chromatic# R >= chromatic# (subrelstr S) let S be Subset of R; ::_thesis: chromatic# R >= chromatic# (subrelstr S) consider C being finite Coloring of R such that A1: card C = chromatic# R by Def3; C | S is Coloring of (subrelstr S) by Th10; then A2: card (C | S) >= chromatic# (subrelstr S) by Def3; card C >= card (C | S) by Th8; hence chromatic# R >= chromatic# (subrelstr S) by A1, A2, XXREAL_0:2; ::_thesis: verum end; theorem Th48: :: MYCIELSK:48 for n being Nat for R being irreflexive NatRelStr of n holds chromatic# (Mycielskian R) = 1 + (chromatic# R) proof let n be Nat; ::_thesis: for R being irreflexive NatRelStr of n holds chromatic# (Mycielskian R) = 1 + (chromatic# R) let R be irreflexive NatRelStr of n; ::_thesis: chromatic# (Mycielskian R) = 1 + (chromatic# R) set cR = the carrier of R; set iR = the InternalRel of R; set cnR = chromatic# R; set MR = Mycielskian R; set cnMR = chromatic# (Mycielskian R); set cMR = the carrier of (Mycielskian R); set iMR = the InternalRel of (Mycielskian R); A1: the carrier of R = n by Def7; A2: ex C being finite Coloring of (Mycielskian R) st card C = 1 + (chromatic# R) proof consider C being finite Coloring of R such that A3: card C = chromatic# R by Def3; defpred S1[ set , set ] means $2 = { (m + n) where m is Element of NAT : m in $1 } ; A4: for e being set st e in C holds ex u being set st S1[e,u] ; consider r being Function such that dom r = C and A5: for e being set st e in C holds S1[e,r . e] from CLASSES1:sch_1(A4); set D = { (d \/ (r . d)) where d is Element of C : d in C } ; A6: card { (d \/ (r . d)) where d is Element of C : d in C } = card C proof percases ( { (d \/ (r . d)) where d is Element of C : d in C } is empty or not { (d \/ (r . d)) where d is Element of C : d in C } is empty ) ; supposeA7: { (d \/ (r . d)) where d is Element of C : d in C } is empty ; ::_thesis: card { (d \/ (r . d)) where d is Element of C : d in C } = card C now__::_thesis:_C_is_empty assume not C is empty ; ::_thesis: contradiction then consider c being set such that A8: c in C by XBOOLE_0:def_1; c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } by A8; hence contradiction by A7; ::_thesis: verum end; hence card { (d \/ (r . d)) where d is Element of C : d in C } = card C by A7; ::_thesis: verum end; supposeA9: not { (d \/ (r . d)) where d is Element of C : d in C } is empty ; ::_thesis: card { (d \/ (r . d)) where d is Element of C : d in C } = card C defpred S2[ set , set ] means $2 = $1 \/ (r . $1); A10: for e being set st e in C holds ex u being set st S2[e,u] ; consider s being Function such that A11: dom s = C and A12: for e being set st e in C holds S2[e,s . e] from CLASSES1:sch_1(A10); A13: rng s c= { (d \/ (r . d)) where d is Element of C : d in C } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s or y in { (d \/ (r . d)) where d is Element of C : d in C } ) assume y in rng s ; ::_thesis: y in { (d \/ (r . d)) where d is Element of C : d in C } then consider x being set such that A14: x in dom s and A15: y = s . x by FUNCT_1:def_3; y = x \/ (r . x) by A14, A15, A11, A12; hence y in { (d \/ (r . d)) where d is Element of C : d in C } by A14, A11; ::_thesis: verum end; then reconsider s = s as Function of C, { (d \/ (r . d)) where d is Element of C : d in C } by A11, FUNCT_2:2; { (d \/ (r . d)) where d is Element of C : d in C } c= rng s proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (d \/ (r . d)) where d is Element of C : d in C } or x in rng s ) assume x in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: x in rng s then consider c being Element of C such that A16: x = c \/ (r . c) and A17: c in C ; x = s . c by A16, A17, A12; hence x in rng s by A17, A11, FUNCT_1:def_3; ::_thesis: verum end; then rng s = { (d \/ (r . d)) where d is Element of C : d in C } by A13, XBOOLE_0:def_10; then A18: s is onto by FUNCT_2:def_3; s is one-to-one proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom s or not x2 in dom s or not s . x1 = s . x2 or x1 = x2 ) assume that A19: x1 in dom s and A20: x2 in dom s and A21: s . x1 = s . x2 ; ::_thesis: x1 = x2 A22: s . x1 = x1 \/ (r . x1) by A19, A12; A23: s . x2 = x2 \/ (r . x2) by A20, A12; thus x1 c= x2 :: according to XBOOLE_0:def_10 ::_thesis: x2 c= x1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in x1 or x in x2 ) assume A24: x in x1 ; ::_thesis: x in x2 A25: x in s . x1 by A22, A24, XBOOLE_0:def_3; percases ( x in x2 or x in r . x2 ) by A25, A21, A23, XBOOLE_0:def_3; suppose x in x2 ; ::_thesis: x in x2 hence x in x2 ; ::_thesis: verum end; suppose x in r . x2 ; ::_thesis: x in x2 then x in { (m + n) where m is Element of NAT : m in x2 } by A5, A20; then consider m being Element of NAT such that A26: x = m + n and m in x2 ; m + n < 0 + n by A24, A26, A19, A11, A1, NAT_1:44; hence x in x2 by XREAL_1:6; ::_thesis: verum end; end; end; thus x2 c= x1 ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in x2 or x in x1 ) assume A27: x in x2 ; ::_thesis: x in x1 A28: x in s . x2 by A23, A27, XBOOLE_0:def_3; percases ( x in x1 or x in r . x1 ) by A28, A21, A22, XBOOLE_0:def_3; suppose x in x1 ; ::_thesis: x in x1 hence x in x1 ; ::_thesis: verum end; suppose x in r . x1 ; ::_thesis: x in x1 then x in { (m + n) where m is Element of NAT : m in x1 } by A5, A19; then consider m being Element of NAT such that A29: x = m + n and m in x1 ; m + n < 0 + n by A27, A29, A20, A11, A1, NAT_1:44; hence x in x1 by XREAL_1:6; ::_thesis: verum end; end; end; end; hence card { (d \/ (r . d)) where d is Element of C : d in C } = card C by A18, A9, EULER_1:11; ::_thesis: verum end; end; end; then A30: { (d \/ (r . d)) where d is Element of C : d in C } is finite ; set E = { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}; A31: union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) c= the carrier of (Mycielskian R) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) or x in the carrier of (Mycielskian R) ) assume x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) ; ::_thesis: x in the carrier of (Mycielskian R) then consider Y being set such that A32: x in Y and A33: Y in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} by TARSKI:def_4; percases ( Y in { (d \/ (r . d)) where d is Element of C : d in C } or Y in {{(2 * n)}} ) by A33, XBOOLE_0:def_3; suppose Y in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: x in the carrier of (Mycielskian R) then consider d being Element of C such that A34: Y = d \/ (r . d) and A35: d in C ; A36: r . d = { (m + n) where m is Element of NAT : m in d } by A35, A5; percases ( x in d or x in r . d ) by A32, A34, XBOOLE_0:def_3; supposeA37: x in d ; ::_thesis: x in the carrier of (Mycielskian R) reconsider a = x as Nat by A37, A35, A1, NECKLACE:3; a < n by A37, A35, A1, NAT_1:44; then a + 0 < n + n by XREAL_1:8; then a < (2 * n) + 1 by NAT_1:13; then a in (2 * n) + 1 by NAT_1:44; hence x in the carrier of (Mycielskian R) by Def7; ::_thesis: verum end; suppose x in r . d ; ::_thesis: x in the carrier of (Mycielskian R) then consider m being Element of NAT such that A38: x = m + n and A39: m in d by A36; m < n by A39, A35, A1, NAT_1:44; then m + n < n + n by XREAL_1:6; then m + n < (2 * n) + 1 by NAT_1:13; then x in (2 * n) + 1 by A38, NAT_1:44; hence x in the carrier of (Mycielskian R) by Def7; ::_thesis: verum end; end; end; suppose Y in {{(2 * n)}} ; ::_thesis: x in the carrier of (Mycielskian R) then Y = {(2 * n)} by TARSKI:def_1; then A40: x = 2 * n by A32, TARSKI:def_1; 2 * n < (2 * n) + 1 by NAT_1:13; then 2 * n in (2 * n) + 1 by NAT_1:44; hence x in the carrier of (Mycielskian R) by A40, Def7; ::_thesis: verum end; end; end; A41: { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} c= bool the carrier of (Mycielskian R) proof let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} or X in bool the carrier of (Mycielskian R) ) assume A42: X in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} ; ::_thesis: X in bool the carrier of (Mycielskian R) X c= the carrier of (Mycielskian R) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in the carrier of (Mycielskian R) ) assume x in X ; ::_thesis: x in the carrier of (Mycielskian R) then x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) by A42, TARSKI:def_4; hence x in the carrier of (Mycielskian R) by A31; ::_thesis: verum end; hence X in bool the carrier of (Mycielskian R) ; ::_thesis: verum end; A43: union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) = the carrier of (Mycielskian R) proof thus union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) c= the carrier of (Mycielskian R) by A31; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (Mycielskian R) c= union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) thus the carrier of (Mycielskian R) c= union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (Mycielskian R) or x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) ) assume x in the carrier of (Mycielskian R) ; ::_thesis: x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) then A44: x in (2 * n) + 1 by Def7; then reconsider a = x as Nat by NECKLACE:3; a < (2 * n) + 1 by A44, NAT_1:44; then A45: a <= 2 * n by NAT_1:13; percases ( a < n or a >= n ) ; suppose a < n ; ::_thesis: x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) then a in n by NAT_1:44; then a in union C by A1, EQREL_1:def_4; then consider c being set such that A46: a in c and A47: c in C by TARSKI:def_4; A48: x in c \/ (r . c) by A46, XBOOLE_0:def_3; c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } by A47; then c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} by XBOOLE_0:def_3; hence x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) by A48, TARSKI:def_4; ::_thesis: verum end; supposeA49: a >= n ; ::_thesis: x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) percases ( a < n + n or a = 2 * n ) by A45, XXREAL_0:1; supposeA50: a < n + n ; ::_thesis: x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) consider b being Nat such that A51: a = n + b by A49, NAT_1:10; reconsider b = b as Element of NAT by ORDINAL1:def_12; b < n by A51, A50, XREAL_1:6; then b in the carrier of R by A1, NAT_1:44; then b in union C by EQREL_1:def_4; then consider c being set such that A52: b in c and A53: c in C by TARSKI:def_4; r . c = { (m + n) where m is Element of NAT : m in c } by A53, A5; then a in r . c by A52, A51; then A54: x in c \/ (r . c) by XBOOLE_0:def_3; c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } by A53; then c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} by XBOOLE_0:def_3; hence x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) by A54, TARSKI:def_4; ::_thesis: verum end; suppose a = 2 * n ; ::_thesis: x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) then A55: a in {(2 * n)} by TARSKI:def_1; {(2 * n)} in {{(2 * n)}} by TARSKI:def_1; then {(2 * n)} in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} by XBOOLE_0:def_3; hence x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) by A55, TARSKI:def_4; ::_thesis: verum end; end; end; end; end; end; now__::_thesis:_for_A_being_Subset_of_the_carrier_of_(Mycielskian_R)_st_A_in__{__(d_\/_(r_._d))_where_d_is_Element_of_C_:_d_in_C__}__\/_{{(2_*_n)}}_holds_ (_A_<>_{}_&_(_for_B_being_Subset_of_the_carrier_of_(Mycielskian_R)_st_B_in__{__(d_\/_(r_._d))_where_d_is_Element_of_C_:_d_in_C__}__\/_{{(2_*_n)}}_&_A_<>_B_holds_ not_A_meets_B_)_) let A be Subset of the carrier of (Mycielskian R); ::_thesis: ( A in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} implies ( A <> {} & ( for B being Subset of the carrier of (Mycielskian R) st B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} & A <> B holds not A meets B ) ) ) assume A56: A in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} ; ::_thesis: ( A <> {} & ( for B being Subset of the carrier of (Mycielskian R) st B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} & A <> B holds not A meets B ) ) thus A <> {} ::_thesis: for B being Subset of the carrier of (Mycielskian R) st B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} & A <> B holds not A meets B proof percases ( A in { (d \/ (r . d)) where d is Element of C : d in C } or A in {{(2 * n)}} ) by A56, XBOOLE_0:def_3; suppose A in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: A <> {} then consider d being Element of C such that A57: A = d \/ (r . d) and A58: d in C ; d <> {} by A58, EQREL_1:def_4; hence A <> {} by A57; ::_thesis: verum end; suppose A in {{(2 * n)}} ; ::_thesis: A <> {} hence A <> {} by TARSKI:def_1; ::_thesis: verum end; end; end; let B be Subset of the carrier of (Mycielskian R); ::_thesis: ( B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} & A <> B implies not A meets B ) assume A59: B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} ; ::_thesis: ( A <> B implies not A meets B ) assume A60: A <> B ; ::_thesis: not A meets B assume A meets B ; ::_thesis: contradiction then consider x being set such that A61: x in A and A62: x in B by XBOOLE_0:3; percases ( ( A in { (d \/ (r . d)) where d is Element of C : d in C } & B in { (d \/ (r . d)) where d is Element of C : d in C } ) or ( A in { (d \/ (r . d)) where d is Element of C : d in C } & B in {{(2 * n)}} ) or ( A in {{(2 * n)}} & B in { (d \/ (r . d)) where d is Element of C : d in C } ) or ( A in {{(2 * n)}} & B in {{(2 * n)}} ) ) by A56, A59, XBOOLE_0:def_3; supposethat A63: A in { (d \/ (r . d)) where d is Element of C : d in C } and A64: B in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: contradiction consider d being Element of C such that A65: A = d \/ (r . d) and A66: d in C by A63; consider e being Element of C such that A67: B = e \/ (r . e) and A68: e in C by A64; percases ( ( x in d & x in e ) or ( x in d & x in r . e ) or ( x in r . d & x in e ) or ( x in r . d & x in r . e ) ) by A65, A67, A61, A62, XBOOLE_0:def_3; suppose ( x in d & x in e ) ; ::_thesis: contradiction then d meets e by XBOOLE_0:3; then d = e by A66, A68, EQREL_1:def_4; hence contradiction by A65, A67, A60; ::_thesis: verum end; supposethat A69: x in d and A70: x in r . e ; ::_thesis: contradiction x in { (m + n) where m is Element of NAT : m in e } by A70, A68, A5; then consider mb being Element of NAT such that A71: x = mb + n and mb in e ; mb + n < n + 0 by A71, A69, A66, A1, NAT_1:44; hence contradiction by XREAL_1:6; ::_thesis: verum end; supposethat A72: x in r . d and A73: x in e ; ::_thesis: contradiction x in { (m + n) where m is Element of NAT : m in d } by A72, A66, A5; then consider ma being Element of NAT such that A74: x = ma + n and ma in d ; ma + n < n + 0 by A74, A73, A68, A1, NAT_1:44; hence contradiction by XREAL_1:6; ::_thesis: verum end; supposethat A75: x in r . d and A76: x in r . e ; ::_thesis: contradiction x in { (m + n) where m is Element of NAT : m in d } by A75, A66, A5; then consider ma being Element of NAT such that A77: x = ma + n and A78: ma in d ; x in { (m + n) where m is Element of NAT : m in e } by A76, A68, A5; then consider mb being Element of NAT such that A79: x = mb + n and A80: mb in e ; d meets e by A77, A79, A78, A80, XBOOLE_0:3; then d = e by A66, A68, EQREL_1:def_4; hence contradiction by A65, A67, A60; ::_thesis: verum end; end; end; supposethat A81: A in { (d \/ (r . d)) where d is Element of C : d in C } and A82: B in {{(2 * n)}} ; ::_thesis: contradiction B = {(2 * n)} by A82, TARSKI:def_1; then A83: x = 2 * n by A62, TARSKI:def_1; consider d being Element of C such that A84: A = d \/ (r . d) and A85: d in C by A81; percases ( x in d or x in r . d ) by A84, A61, XBOOLE_0:def_3; suppose x in d ; ::_thesis: contradiction then n + n < n by A85, A1, A83, NAT_1:44; hence contradiction by NAT_1:11; ::_thesis: verum end; suppose x in r . d ; ::_thesis: contradiction then x in { (m + n) where m is Element of NAT : m in d } by A85, A5; then consider m being Element of NAT such that A86: x = m + n and A87: m in d ; m in n by A87, A85, A1; hence contradiction by A86, A83; ::_thesis: verum end; end; end; supposethat A88: A in {{(2 * n)}} and A89: B in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: contradiction A = {(2 * n)} by A88, TARSKI:def_1; then A90: x = 2 * n by A61, TARSKI:def_1; consider d being Element of C such that A91: B = d \/ (r . d) and A92: d in C by A89; percases ( x in d or x in r . d ) by A91, A62, XBOOLE_0:def_3; suppose x in d ; ::_thesis: contradiction then n + n < n by A92, A1, A90, NAT_1:44; hence contradiction by NAT_1:11; ::_thesis: verum end; suppose x in r . d ; ::_thesis: contradiction then x in { (m + n) where m is Element of NAT : m in d } by A92, A5; then consider m being Element of NAT such that A93: x = m + n and A94: m in d ; m in n by A94, A92, A1; hence contradiction by A93, A90; ::_thesis: verum end; end; end; suppose ( A in {{(2 * n)}} & B in {{(2 * n)}} ) ; ::_thesis: contradiction then ( A = {(2 * n)} & B = {(2 * n)} ) by TARSKI:def_1; hence contradiction by A60; ::_thesis: verum end; end; end; then reconsider E = { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} as a_partition of the carrier of (Mycielskian R) by A41, A43, EQREL_1:def_4; now__::_thesis:_for_x_being_set_st_x_in_E_holds_ x_is_StableSet_of_(Mycielskian_R) let x be set ; ::_thesis: ( x in E implies b1 is StableSet of (Mycielskian R) ) assume A95: x in E ; ::_thesis: b1 is StableSet of (Mycielskian R) percases ( x in { (d \/ (r . d)) where d is Element of C : d in C } or x in {{(2 * n)}} ) by A95, XBOOLE_0:def_3; suppose x in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: b1 is StableSet of (Mycielskian R) then consider d being Element of C such that A96: x = d \/ (r . d) and A97: d in C ; reconsider d = d as Subset of R by A97; A98: r . d = { (m + n) where m is Element of NAT : m in d } by A97, A5; A99: x c= the carrier of (Mycielskian R) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x or a in the carrier of (Mycielskian R) ) assume A100: a in x ; ::_thesis: a in the carrier of (Mycielskian R) percases ( a in d or a in r . d ) by A96, A100, XBOOLE_0:def_3; supposeA101: a in d ; ::_thesis: a in the carrier of (Mycielskian R) then reconsider ap1 = a as Nat by A1, NECKLACE:3; A102: ap1 < n by A101, A1, NAT_1:44; n <= n + n by NAT_1:12; then ap1 < n + n by A102, XXREAL_0:2; then ap1 < (2 * n) + 1 by NAT_1:13; then a in (2 * n) + 1 by NAT_1:44; hence a in the carrier of (Mycielskian R) by Def7; ::_thesis: verum end; suppose a in r . d ; ::_thesis: a in the carrier of (Mycielskian R) then consider am being Element of NAT such that A103: a = am + n and A104: am in d by A98; am < n by A104, A1, NAT_1:44; then am + n < n + n by XREAL_1:6; then am + n < (2 * n) + 1 by NAT_1:13; then a in (2 * n) + 1 by A103, NAT_1:44; hence a in the carrier of (Mycielskian R) by Def7; ::_thesis: verum end; end; end; A105: now__::_thesis:_for_x_being_Nat_st_x_in_r_._d_holds_ (_n_<=_x_&_x_<_2_*_n_) let x be Nat; ::_thesis: ( x in r . d implies ( n <= x & x < 2 * n ) ) assume x in r . d ; ::_thesis: ( n <= x & x < 2 * n ) then consider m being Element of NAT such that A106: x = m + n and A107: m in d by A98; thus n <= x by A106, NAT_1:11; ::_thesis: x < 2 * n m < n by A107, A1, NAT_1:44; then m + n < n + n by XREAL_1:6; hence x < 2 * n by A106; ::_thesis: verum end; A108: d is stable by A97, DILWORTH:def_12; now__::_thesis:_for_a,_b_being_Element_of_(Mycielskian_R)_st_a_in_x_&_b_in_x_&_a_<>_b_holds_ (_not_a_<=_b_&_not_b_<=_a_) let a, b be Element of (Mycielskian R); ::_thesis: ( a in x & b in x & a <> b implies ( not a <= b & not b <= a ) ) assume that A109: a in x and A110: b in x and A111: a <> b and A112: ( a <= b or b <= a ) ; ::_thesis: contradiction A113: ( [a,b] in the InternalRel of (Mycielskian R) or [b,a] in the InternalRel of (Mycielskian R) ) by A112, ORDERS_2:def_5; percases ( ( a in d & b in d ) or ( a in d & b in r . d ) or ( a in r . d & b in d ) or ( a in r . d & b in r . d ) ) by A109, A110, A96, XBOOLE_0:def_3; supposeA114: ( a in d & b in d ) ; ::_thesis: contradiction then A115: ( [a,b] in the InternalRel of R or [b,a] in the InternalRel of R ) by A1, A113, Th40; reconsider a = a, b = b as Element of R by A114; ( a <= b or b <= a ) by A115, ORDERS_2:def_5; hence contradiction by A114, A111, A108, DILWORTH:def_2; ::_thesis: verum end; supposethat A116: a in d and A117: b in r . d ; ::_thesis: contradiction consider bm being Element of NAT such that A118: b = bm + n and A119: bm in d by A117, A98; reconsider ap1 = a as Nat by A116, A1, NECKLACE:3; A120: ( [ap1,bm] in the InternalRel of R or [bm,ap1] in the InternalRel of R ) by A113, Th42, Th43, A118, A116, A1; reconsider bmp1 = bm, a = a as Element of R by A119, A116; A121: ( bmp1 <= a or a <= bmp1 ) by A120, ORDERS_2:def_5; bmp1 <> a by A120, A116, NECKLACE:def_5; hence contradiction by A121, A119, A116, A108, DILWORTH:def_2; ::_thesis: verum end; supposethat A122: a in r . d and A123: b in d ; ::_thesis: contradiction consider am being Element of NAT such that A124: a = am + n and A125: am in d by A122, A98; reconsider bp1 = b as Nat by A123, A1, NECKLACE:3; A126: ( [am,bp1] in the InternalRel of R or [bp1,am] in the InternalRel of R ) by A113, Th42, Th43, A124, A123, A1; reconsider amp1 = am, b = b as Element of R by A125, A123; A127: ( amp1 <= b or b <= amp1 ) by A126, ORDERS_2:def_5; amp1 <> b by A126, A123, NECKLACE:def_5; hence contradiction by A127, A125, A123, A108, DILWORTH:def_2; ::_thesis: verum end; supposethat A128: a in r . d and A129: b in r . d ; ::_thesis: contradiction consider am being Element of NAT such that A130: a = am + n and am in d by A128, A98; consider bm being Element of NAT such that A131: b = bm + n and bm in d by A129, A98; ( n <= am + n & am + n < 2 * n & n <= bm + n & bm + n < 2 * n ) by A128, A129, A130, A131, A105; hence contradiction by A130, A131, A113, Th38; ::_thesis: verum end; end; end; hence x is StableSet of (Mycielskian R) by A99, DILWORTH:def_2; ::_thesis: verum end; suppose x in {{(2 * n)}} ; ::_thesis: b1 is StableSet of (Mycielskian R) then A132: x = {(2 * n)} by TARSKI:def_1; 2 * n < (2 * n) + 1 by NAT_1:13; then 2 * n in (2 * n) + 1 by NAT_1:44; then A133: 2 * n in the carrier of (Mycielskian R) by Def7; x is Subset of (Mycielskian R) by A132, A133, SUBSET_1:33; hence x is StableSet of (Mycielskian R) by A132; ::_thesis: verum end; end; end; then reconsider E = E as Coloring of (Mycielskian R) by DILWORTH:def_12; take E ; ::_thesis: card E = 1 + (chromatic# R) now__::_thesis:_not_{(2_*_n)}_in__{__(d_\/_(r_._d))_where_d_is_Element_of_C_:_d_in_C__}_ assume {(2 * n)} in { (d \/ (r . d)) where d is Element of C : d in C } ; ::_thesis: contradiction then consider d being Element of C such that A134: {(2 * n)} = d \/ (r . d) and A135: d in C ; A136: 2 * n in d \/ (r . d) by A134, TARSKI:def_1; percases ( 2 * n in d or 2 * n in r . d ) by A136, XBOOLE_0:def_3; suppose 2 * n in d ; ::_thesis: contradiction then 2 * n in the carrier of R by A135; then 2 * n in n by Def7; then n + n < n by NAT_1:44; hence contradiction by NAT_1:11; ::_thesis: verum end; suppose 2 * n in r . d ; ::_thesis: contradiction then 2 * n in { (m + n) where m is Element of NAT : m in d } by A135, A5; then consider m being Element of NAT such that A137: 2 * n = m + n and A138: m in d ; m in the carrier of R by A135, A138; then m in n by Def7; hence contradiction by A137; ::_thesis: verum end; end; end; hence card E = 1 + (chromatic# R) by A6, A30, A3, CARD_2:41; ::_thesis: verum end; for C being finite Coloring of (Mycielskian R) holds 1 + (chromatic# R) <= card C proof let E be finite Coloring of (Mycielskian R); ::_thesis: 1 + (chromatic# R) <= card E assume 1 + (chromatic# R) > card E ; ::_thesis: contradiction then A139: chromatic# R >= card E by NAT_1:13; A140: chromatic# (Mycielskian R) <= card E by Def3; then A141: chromatic# (Mycielskian R) <= chromatic# R by A139, XXREAL_0:2; n <= n + n by NAT_1:11; then n < (2 * n) + 1 by NAT_1:13; then n c= (2 * n) + 1 by NAT_1:39; then reconsider S = n as Subset of (Mycielskian R) by Def7; A142: R = subrelstr S by Th45; then chromatic# R <= chromatic# (Mycielskian R) by Th47; then chromatic# R = chromatic# (Mycielskian R) by A141, XXREAL_0:1; then A143: card E = chromatic# R by A139, A140, XXREAL_0:1; reconsider C = E | S as Coloring of R by A142, Th10; A144: card C >= chromatic# R by Def3; A145: card C <= card E by Th8; then A146: card C = chromatic# R by A143, A144, XXREAL_0:1; 2 * n < (2 * n) + 1 by NAT_1:13; then 2 * n in (2 * n) + 1 by NAT_1:44; then 2 * n in the carrier of (Mycielskian R) by Def7; then 2 * n in union E by EQREL_1:def_4; then consider e being set such that A147: 2 * n in e and A148: e in E by TARSKI:def_4; reconsider e = e as Subset of (Mycielskian R) by A148; reconsider n2 = 2 * n as Element of (Mycielskian R) by A147, A148; set se = e /\ S; e meets S by A143, A146, A148, Th9; then A149: e /\ S in C by A148; then consider mp1 being Element of R such that A150: mp1 in e /\ S and A151: for d being Element of C st d <> e /\ S holds ex w being Element of R st ( w in Adjacent mp1 & w in d ) by A145, A143, A144, Th31, XXREAL_0:1; reconsider m = mp1 as Nat by A150, A149, NECKLACE:3; set mn = m + n; A152: 0 + n <= m + n by XREAL_1:6; m < n by A150, A149, NAT_1:44; then A153: m + n < n + n by XREAL_1:6; then m + n < (2 * n) + 1 by NAT_1:13; then A154: m + n in (2 * n) + 1 by NAT_1:44; then m + n in the carrier of (Mycielskian R) by Def7; then m + n in union E by EQREL_1:def_4; then consider f being set such that A155: m + n in f and A156: f in E by TARSKI:def_4; reconsider f = f as Subset of (Mycielskian R) by A156; reconsider mnp1 = m + n as Element of (Mycielskian R) by A154, Def7; A157: now__::_thesis:_not_e_<>_f assume A158: e <> f ; ::_thesis: contradiction set sf = f /\ S; f meets S by A143, A146, A156, Th9; then A159: f /\ S in C by A156; A160: f /\ S c= f by XBOOLE_1:17; now__::_thesis:_not_f_/\_S_=_e_/\_S assume A161: f /\ S = e /\ S ; ::_thesis: contradiction f /\ S <> {} by A159, EQREL_1:def_4; then consider x being set such that A162: x in f /\ S by XBOOLE_0:def_1; e /\ S c= e by XBOOLE_1:17; then e meets f by A161, A162, A160, XBOOLE_0:3; hence contradiction by A158, A156, A148, EQREL_1:def_4; ::_thesis: verum end; then consider wp1 being Element of R such that A163: wp1 in Adjacent mp1 and A164: wp1 in f /\ S by A159, A151; reconsider w = wp1 as Nat by A164, A159, NECKLACE:3; A165: w < n by A164, A159, NAT_1:44; ( mp1 < wp1 or wp1 < mp1 ) by A163, Def6; then ( mp1 <= wp1 or wp1 <= mp1 ) by ORDERS_2:def_6; then ( [m,w] in the InternalRel of R or [w,m] in the InternalRel of R ) by ORDERS_2:def_5; then A166: ( [(m + n),w] in the InternalRel of (Mycielskian R) or [w,(m + n)] in the InternalRel of (Mycielskian R) ) by Th41; reconsider wp2 = wp1 as Element of (Mycielskian R) by A164; f is stable by A156, DILWORTH:def_12; then ( not wp2 <= mnp1 & not mnp1 <= wp2 ) by A165, A152, A164, A160, A155, DILWORTH:def_2; hence contradiction by A166, ORDERS_2:def_5; ::_thesis: verum end; A167: [(m + n),(2 * n)] in the InternalRel of (Mycielskian R) by A153, A152, Th44; e is stable by A148, DILWORTH:def_12; then ( not mnp1 <= n2 & not n2 <= mnp1 ) by A147, A155, A157, A153, DILWORTH:def_2; hence contradiction by A167, ORDERS_2:def_5; ::_thesis: verum end; hence chromatic# (Mycielskian R) = 1 + (chromatic# R) by A2, Def3; ::_thesis: verum end; Lm1: now__::_thesis:_for_myc1,_myc2_being_Function_st_dom_myc1_=_NAT_&_myc1_._0_=_CompleteRelStr_2_&_(_for_k_being_Nat for_R_being_NatRelStr_of_(3_*_(2_|^_k))_-'_1_st_R_=_myc1_._k_holds_ myc1_._(k_+_1)_=_Mycielskian_R_)_&_dom_myc2_=_NAT_&_myc2_._0_=_CompleteRelStr_2_&_(_for_k_being_Nat for_R_being_NatRelStr_of_(3_*_(2_|^_k))_-'_1_st_R_=_myc2_._k_holds_ myc2_._(k_+_1)_=_Mycielskian_R_)_holds_ myc1_=_myc2 let myc1, myc2 be Function; ::_thesis: ( dom myc1 = NAT & myc1 . 0 = CompleteRelStr 2 & ( for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds myc1 . (k + 1) = Mycielskian R ) & dom myc2 = NAT & myc2 . 0 = CompleteRelStr 2 & ( for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds myc2 . (k + 1) = Mycielskian R ) implies myc1 = myc2 ) assume that A1: dom myc1 = NAT and A2: myc1 . 0 = CompleteRelStr 2 and A3: for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds myc1 . (k + 1) = Mycielskian R and A4: dom myc2 = NAT and A5: myc2 . 0 = CompleteRelStr 2 and A6: for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds myc2 . (k + 1) = Mycielskian R ; ::_thesis: myc1 = myc2 defpred S1[ Nat] means ( myc1 . $1 is NatRelStr of (3 * (2 |^ $1)) -' 1 & myc1 . $1 = myc2 . $1 ); (3 * (2 |^ 0)) -' 1 = (3 * 1) -' 1 by NEWTON:4 .= (2 + 1) -' 1 .= 2 by NAT_D:34 ; then A7: S1[ 0 ] by A2, A5; A8: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A9: S1[k] ; ::_thesis: S1[k + 1] reconsider R = myc1 . k as NatRelStr of (3 * (2 |^ k)) -' 1 by A9; A10: myc1 . (k + 1) = Mycielskian R by A3; A11: 3 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64; ( 2 |^ k >= k + 1 & k + 1 >= 1 ) by NAT_1:11, NEWTON:85; then 2 |^ k >= 1 by XXREAL_0:2; then A12: 3 * (2 |^ k) >= 1 by A11, XXREAL_0:2; then A13: (3 * (2 |^ k)) - 1 >= 1 - 1 by XREAL_1:9; 2 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64; then 2 |^ (k + 1) >= 2 |^ k by NEWTON:6; then 3 * (2 |^ (k + 1)) >= 3 * (2 |^ k) by XREAL_1:64; then 3 * (2 |^ (k + 1)) >= 1 by A12, XXREAL_0:2; then A14: (3 * (2 |^ (k + 1))) - 1 >= 1 - 1 by XREAL_1:9; (2 * ((3 * (2 |^ k)) -' 1)) + 1 = (2 * ((3 * (2 |^ k)) - 1)) + 1 by A13, XREAL_0:def_2 .= ((3 * (2 * (2 |^ k))) - 2) + 1 .= ((3 * (2 |^ (k + 1))) - 2) + 1 by NEWTON:6 .= (3 * (2 |^ (k + 1))) -' 1 by A14, XREAL_0:def_2 ; hence S1[k + 1] by A10, A9, A6; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A7, A8); then for x being set st x in dom myc1 holds myc1 . x = myc2 . x by A1; hence myc1 = myc2 by A1, A4, FUNCT_1:2; ::_thesis: verum end; definition let n be Nat; func Mycielskian n -> NatRelStr of (3 * (2 |^ n)) -' 1 means :Def10: :: MYCIELSK:def 10 ex myc being Function st ( it = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds myc . (k + 1) = Mycielskian R ) ); existence ex b1 being NatRelStr of (3 * (2 |^ n)) -' 1 ex myc being Function st ( b1 = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds myc . (k + 1) = Mycielskian R ) ) proof defpred S1[ Nat, set , set ] means ( ( $2 is NatRelStr of (3 * (2 |^ $1)) -' 1 implies ex R being NatRelStr of (3 * (2 |^ $1)) -' 1 st ( $2 = R & $3 = Mycielskian R ) ) & ( $2 is not NatRelStr of (3 * (2 |^ $1)) -' 1 implies $3 = $2 ) ); A1: for n being Element of NAT for x being set ex y being set st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being set ex y being set st S1[n,x,y] let x be set ; ::_thesis: ex y being set st S1[n,x,y] percases ( x is NatRelStr of (3 * (2 |^ n)) -' 1 or not x is NatRelStr of (3 * (2 |^ n)) -' 1 ) ; suppose x is NatRelStr of (3 * (2 |^ n)) -' 1 ; ::_thesis: ex y being set st S1[n,x,y] then reconsider R = x as NatRelStr of (3 * (2 |^ n)) -' 1 ; Mycielskian R = Mycielskian R ; hence ex y being set st S1[n,x,y] ; ::_thesis: verum end; suppose x is not NatRelStr of (3 * (2 |^ n)) -' 1 ; ::_thesis: ex y being set st S1[n,x,y] hence ex y being set st S1[n,x,y] ; ::_thesis: verum end; end; end; consider f being Function such that A2: dom f = NAT and A3: f . 0 = CompleteRelStr 2 and A4: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch_1(A1); defpred S2[ Nat] means f . $1 is NatRelStr of (3 * (2 |^ $1)) -' 1; (3 * (2 |^ 0)) -' 1 = (3 * 1) -' 1 by NEWTON:4 .= (2 + 1) -' 1 .= 2 by NAT_D:34 ; then A5: S2[ 0 ] by A3; A6: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A7: S2[k] ; ::_thesis: S2[k + 1] consider R being NatRelStr of (3 * (2 |^ k)) -' 1 such that f . k = R and A8: f . (k + 1) = Mycielskian R by A7, A4; A9: 3 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64; ( 2 |^ k >= k + 1 & k + 1 >= 1 ) by NAT_1:11, NEWTON:85; then 2 |^ k >= 1 by XXREAL_0:2; then A10: 3 * (2 |^ k) >= 1 by A9, XXREAL_0:2; then A11: (3 * (2 |^ k)) - 1 >= 1 - 1 by XREAL_1:9; 2 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64; then 2 |^ (k + 1) >= 2 |^ k by NEWTON:6; then 3 * (2 |^ (k + 1)) >= 3 * (2 |^ k) by XREAL_1:64; then 3 * (2 |^ (k + 1)) >= 1 by A10, XXREAL_0:2; then A12: (3 * (2 |^ (k + 1))) - 1 >= 1 - 1 by XREAL_1:9; (2 * ((3 * (2 |^ k)) -' 1)) + 1 = (2 * ((3 * (2 |^ k)) - 1)) + 1 by A11, XREAL_0:def_2 .= ((3 * (2 * (2 |^ k))) - 2) + 1 .= ((3 * (2 |^ (k + 1))) - 2) + 1 by NEWTON:6 .= (3 * (2 |^ (k + 1))) -' 1 by A12, XREAL_0:def_2 ; hence S2[k + 1] by A8; ::_thesis: verum end; A13: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A5, A6); n is Element of NAT by ORDINAL1:def_12; then reconsider IT = f . n as NatRelStr of (3 * (2 |^ n)) -' 1 by A13; take IT ; ::_thesis: ex myc being Function st ( IT = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds myc . (k + 1) = Mycielskian R ) ) take myc = f; ::_thesis: ( IT = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds myc . (k + 1) = Mycielskian R ) ) thus IT = myc . n ; ::_thesis: ( dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds myc . (k + 1) = Mycielskian R ) ) thus dom myc = NAT by A2; ::_thesis: ( myc . 0 = CompleteRelStr 2 & ( for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds myc . (k + 1) = Mycielskian R ) ) thus myc . 0 = CompleteRelStr 2 by A3; ::_thesis: for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds myc . (k + 1) = Mycielskian R let k be Nat; ::_thesis: for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds myc . (k + 1) = Mycielskian R A14: k is Element of NAT by ORDINAL1:def_12; let R be NatRelStr of (3 * (2 |^ k)) -' 1; ::_thesis: ( R = myc . k implies myc . (k + 1) = Mycielskian R ) assume A15: R = myc . k ; ::_thesis: myc . (k + 1) = Mycielskian R then consider RR being NatRelStr of (3 * (2 |^ k)) -' 1 such that A16: f . k = RR and A17: f . (k + 1) = Mycielskian RR by A14, A4; thus myc . (k + 1) = Mycielskian R by A17, A15, A16; ::_thesis: verum end; uniqueness for b1, b2 being NatRelStr of (3 * (2 |^ n)) -' 1 st ex myc being Function st ( b1 = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds myc . (k + 1) = Mycielskian R ) ) & ex myc being Function st ( b2 = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds myc . (k + 1) = Mycielskian R ) ) holds b1 = b2 by Lm1; end; :: deftheorem Def10 defines Mycielskian MYCIELSK:def_10_:_ for n being Nat for b2 being NatRelStr of (3 * (2 |^ n)) -' 1 holds ( b2 = Mycielskian n iff ex myc being Function st ( b2 = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds myc . (k + 1) = Mycielskian R ) ) ); theorem Th49: :: MYCIELSK:49 ( Mycielskian 0 = CompleteRelStr 2 & ( for k being Nat holds Mycielskian (k + 1) = Mycielskian (Mycielskian k) ) ) proof consider myc being Function such that A1: Mycielskian 0 = myc . 0 and dom myc = NAT and A2: myc . 0 = CompleteRelStr 2 and for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds myc . (k + 1) = Mycielskian R by Def10; thus Mycielskian 0 = CompleteRelStr 2 by A1, A2; ::_thesis: for k being Nat holds Mycielskian (k + 1) = Mycielskian (Mycielskian k) let k be Nat; ::_thesis: Mycielskian (k + 1) = Mycielskian (Mycielskian k) consider myc1 being Function such that A3: Mycielskian k = myc1 . k and A4: ( dom myc1 = NAT & myc1 . 0 = CompleteRelStr 2 & ( for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds myc1 . (k + 1) = Mycielskian R ) ) by Def10; consider myc2 being Function such that A5: Mycielskian (k + 1) = myc2 . (k + 1) and A6: ( dom myc2 = NAT & myc2 . 0 = CompleteRelStr 2 ) and A7: for k being Nat for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds myc2 . (k + 1) = Mycielskian R by Def10; myc1 = myc2 by A4, A6, A7, Lm1; hence Mycielskian (k + 1) = Mycielskian (Mycielskian k) by A3, A7, A5; ::_thesis: verum end; registration let n be Nat; cluster Mycielskian n -> irreflexive ; coherence Mycielskian n is irreflexive proof defpred S1[ Nat] means Mycielskian n is irreflexive ; A1: S1[ 0 ] by Th49; A2: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) set cMRn = the carrier of (Mycielskian n); set iMRn = the InternalRel of (Mycielskian n); set cMRn1 = the carrier of (Mycielskian (n + 1)); set iMRn1 = the InternalRel of (Mycielskian (n + 1)); assume A3: S1[n] ; ::_thesis: S1[n + 1] assume not S1[n + 1] ; ::_thesis: contradiction then consider x being set such that A4: x in the carrier of (Mycielskian (n + 1)) and A5: [x,x] in the InternalRel of (Mycielskian (n + 1)) by NECKLACE:def_5; A6: Mycielskian (n + 1) = Mycielskian (Mycielskian n) by Th49; set N = (3 * (2 |^ n)) -' 1; A7: the carrier of (Mycielskian (n + 1)) = (2 * ((3 * (2 |^ n)) -' 1)) + 1 by A6, Def7; A8: the carrier of (Mycielskian n) = (3 * (2 |^ n)) -' 1 by Def7; reconsider x = x as Nat by A7, A4, NECKLACE:3; ( ( x < (3 * (2 |^ n)) -' 1 & x < (3 * (2 |^ n)) -' 1 ) or ( x < (3 * (2 |^ n)) -' 1 & (3 * (2 |^ n)) -' 1 <= x & x < 2 * ((3 * (2 |^ n)) -' 1) ) or ( (3 * (2 |^ n)) -' 1 <= x & x < 2 * ((3 * (2 |^ n)) -' 1) & x < (3 * (2 |^ n)) -' 1 ) or ( x = 2 * ((3 * (2 |^ n)) -' 1) & (3 * (2 |^ n)) -' 1 <= x & x < 2 * ((3 * (2 |^ n)) -' 1) ) or ( (3 * (2 |^ n)) -' 1 <= x & x < 2 * ((3 * (2 |^ n)) -' 1) & x = 2 * ((3 * (2 |^ n)) -' 1) ) ) by A6, A5, Th38; then A9: x in (3 * (2 |^ n)) -' 1 by NAT_1:44; then [x,x] in the InternalRel of (Mycielskian n) by A5, A6, Th40; hence contradiction by A3, A8, A9, NECKLACE:def_5; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence Mycielskian n is irreflexive ; ::_thesis: verum end; end; registration let n be Nat; cluster Mycielskian n -> symmetric ; coherence Mycielskian n is symmetric proof defpred S1[ Nat] means Mycielskian n is symmetric ; A1: S1[ 0 ] by Th49; A2: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) set cMRn = the carrier of (Mycielskian n); set iMRn = the InternalRel of (Mycielskian n); set cMRn1 = the carrier of (Mycielskian (n + 1)); set iMRn1 = the InternalRel of (Mycielskian (n + 1)); assume A3: S1[n] ; ::_thesis: S1[n + 1] A4: Mycielskian (n + 1) = Mycielskian (Mycielskian n) by Th49; set N = (3 * (2 |^ n)) -' 1; A5: the carrier of (Mycielskian (n + 1)) = (2 * ((3 * (2 |^ n)) -' 1)) + 1 by A4, Def7; A6: the carrier of (Mycielskian n) = (3 * (2 |^ n)) -' 1 by Def7; let x, y be set ; :: according to RELAT_2:def_3,NECKLACE:def_3 ::_thesis: ( not x in the carrier of (Mycielskian (n + 1)) or not y in the carrier of (Mycielskian (n + 1)) or not [x,y] in the InternalRel of (Mycielskian (n + 1)) or [y,x] in the InternalRel of (Mycielskian (n + 1)) ) assume that A7: x in the carrier of (Mycielskian (n + 1)) and A8: y in the carrier of (Mycielskian (n + 1)) and A9: [x,y] in the InternalRel of (Mycielskian (n + 1)) ; ::_thesis: [y,x] in the InternalRel of (Mycielskian (n + 1)) reconsider xp1 = x, yp1 = y as Nat by A5, A7, A8, NECKLACE:3; A10: [xp1,yp1] in the InternalRel of (Mycielskian (n + 1)) by A9; percases ( ( xp1 < (3 * (2 |^ n)) -' 1 & yp1 < (3 * (2 |^ n)) -' 1 ) or ( xp1 < (3 * (2 |^ n)) -' 1 & (3 * (2 |^ n)) -' 1 <= yp1 & yp1 < 2 * ((3 * (2 |^ n)) -' 1) ) or ( (3 * (2 |^ n)) -' 1 <= xp1 & xp1 < 2 * ((3 * (2 |^ n)) -' 1) & yp1 < (3 * (2 |^ n)) -' 1 ) or ( xp1 = 2 * ((3 * (2 |^ n)) -' 1) & (3 * (2 |^ n)) -' 1 <= yp1 & yp1 < 2 * ((3 * (2 |^ n)) -' 1) ) or ( (3 * (2 |^ n)) -' 1 <= xp1 & xp1 < 2 * ((3 * (2 |^ n)) -' 1) & yp1 = 2 * ((3 * (2 |^ n)) -' 1) ) ) by A10, A4, Th38; suppose ( xp1 < (3 * (2 |^ n)) -' 1 & yp1 < (3 * (2 |^ n)) -' 1 ) ; ::_thesis: [y,x] in the InternalRel of (Mycielskian (n + 1)) then ( xp1 in (3 * (2 |^ n)) -' 1 & yp1 in (3 * (2 |^ n)) -' 1 ) by NAT_1:44; then A11: [yp1,xp1] in the InternalRel of (Mycielskian n) by A3, A6, Th5, A9, A4, Th40; the InternalRel of (Mycielskian n) c= the InternalRel of (Mycielskian (n + 1)) by A4, Th39; hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by A11; ::_thesis: verum end; supposethat A12: xp1 < (3 * (2 |^ n)) -' 1 and A13: (3 * (2 |^ n)) -' 1 <= yp1 and A14: yp1 < 2 * ((3 * (2 |^ n)) -' 1) ; ::_thesis: [y,x] in the InternalRel of (Mycielskian (n + 1)) consider yy being Nat such that A15: yp1 = ((3 * (2 |^ n)) -' 1) + yy by A13, NAT_1:10; A16: xp1 in (3 * (2 |^ n)) -' 1 by A12, NAT_1:44; yy + ((3 * (2 |^ n)) -' 1) < ((3 * (2 |^ n)) -' 1) + ((3 * (2 |^ n)) -' 1) by A14, A15; then yy < (3 * (2 |^ n)) -' 1 by XREAL_1:6; then A17: yy in (3 * (2 |^ n)) -' 1 by NAT_1:44; [x,yy] in the InternalRel of (Mycielskian n) by A9, A16, A15, A4, Th42; then [yy,x] in the InternalRel of (Mycielskian n) by A17, A16, A6, A3, Th5; hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by A4, A10, A15, Th41; ::_thesis: verum end; supposethat A18: (3 * (2 |^ n)) -' 1 <= xp1 and A19: xp1 < 2 * ((3 * (2 |^ n)) -' 1) and A20: yp1 < (3 * (2 |^ n)) -' 1 ; ::_thesis: [y,x] in the InternalRel of (Mycielskian (n + 1)) consider xx being Nat such that A21: xp1 = ((3 * (2 |^ n)) -' 1) + xx by A18, NAT_1:10; A22: yp1 in (3 * (2 |^ n)) -' 1 by A20, NAT_1:44; xx + ((3 * (2 |^ n)) -' 1) < ((3 * (2 |^ n)) -' 1) + ((3 * (2 |^ n)) -' 1) by A21, A19; then xx < (3 * (2 |^ n)) -' 1 by XREAL_1:6; then A23: xx in (3 * (2 |^ n)) -' 1 by NAT_1:44; [xx,y] in the InternalRel of (Mycielskian n) by A22, A9, A4, A21, Th43; then [y,xx] in the InternalRel of (Mycielskian n) by A23, A22, A6, A3, Th5; hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by A4, A10, A21, Th41; ::_thesis: verum end; suppose ( xp1 = 2 * ((3 * (2 |^ n)) -' 1) & (3 * (2 |^ n)) -' 1 <= yp1 & yp1 < 2 * ((3 * (2 |^ n)) -' 1) ) ; ::_thesis: [y,x] in the InternalRel of (Mycielskian (n + 1)) hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by A4, Th44; ::_thesis: verum end; suppose ( (3 * (2 |^ n)) -' 1 <= xp1 & xp1 < 2 * ((3 * (2 |^ n)) -' 1) & yp1 = 2 * ((3 * (2 |^ n)) -' 1) ) ; ::_thesis: [y,x] in the InternalRel of (Mycielskian (n + 1)) hence [y,x] in the InternalRel of (Mycielskian (n + 1)) by A4, Th44; ::_thesis: verum end; end; end; for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); hence Mycielskian n is symmetric ; ::_thesis: verum end; end; theorem Th50: :: MYCIELSK:50 for n being Nat holds ( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) = n + 2 ) proof defpred S1[ Nat] means ( clique# (Mycielskian $1) = 2 & chromatic# (Mycielskian $1) = $1 + 2 ); A1: clique# (Mycielskian 0) = clique# (CompleteRelStr 2) by Th49 .= 2 by Th33 ; chromatic# (Mycielskian 0) = chromatic# (CompleteRelStr 2) by Th49 .= 2 by Th35 ; then A2: S1[ 0 ] by A1; 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 that A4: clique# (Mycielskian n) = 2 and A5: chromatic# (Mycielskian n) = n + 2 ; ::_thesis: S1[n + 1] A6: Mycielskian (n + 1) = Mycielskian (Mycielskian n) by Th49; thus clique# (Mycielskian (n + 1)) = 2 by A4, A6, Th46; ::_thesis: chromatic# (Mycielskian (n + 1)) = (n + 1) + 2 thus chromatic# (Mycielskian (n + 1)) = 1 + (chromatic# (Mycielskian n)) by A6, Th48 .= (n + 1) + 2 by A5 ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A2, A3); hence for n being Nat holds ( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) = n + 2 ) ; ::_thesis: verum end; theorem :: MYCIELSK:51 for n being Nat ex R being finite RelStr st ( clique# R = 2 & chromatic# R > n ) proof let n be Nat; ::_thesis: ex R being finite RelStr st ( clique# R = 2 & chromatic# R > n ) take Mycielskian n ; ::_thesis: ( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) > n ) ( (n + 1) + 1 > n + 1 & n + 1 > n ) by NAT_1:13; then n + 2 > n by XXREAL_0:2; hence ( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) > n ) by Th50; ::_thesis: verum end; theorem :: MYCIELSK:52 for n being Nat ex R being finite RelStr st ( stability# R = 2 & cliquecover# R > n ) proof let n be Nat; ::_thesis: ex R being finite RelStr st ( stability# R = 2 & cliquecover# R > n ) set R = Mycielskian n; ( (n + 1) + 1 > n + 1 & n + 1 > n ) by NAT_1:13; then n + 2 > n by XXREAL_0:2; then A1: ( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) > n ) by Th50; take S = ComplRelStr (Mycielskian n); ::_thesis: ( stability# S = 2 & cliquecover# S > n ) thus stability# S = 2 by A1, Th23; ::_thesis: cliquecover# S > n thus cliquecover# S > n by A1, Th29; ::_thesis: verum end;