mycielsk.miz



    begin

    begin

    defpred P[ set] means not contradiction;

    theorem :: MYCIELSK:1

    for x,y,z be Real st 0 <= x holds (x * (y -' z)) = ((x * y) -' (x * z))

    proof

      let x,y,z be Real;

      assume

       A1: x >= 0 ;

      per cases ;

        suppose

         A2: (y - z) >= 0 ;

        

         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;

      end;

        suppose

         A4: (y - z) < 0 ;

        per cases by A1;

          suppose

           A5: x = 0 ;

          thus (x * (y -' z)) = ((x * y) -' (x * z)) by A5, XREAL_1: 232;

        end;

          suppose

           A6: x > 0 ;

          (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;

        end;

      end;

    end;

    theorem :: MYCIELSK:2

    

     Th2: for x,y,z be Nat holds x in (( Segm y) \ ( Segm z)) iff z <= x & x < y

    proof

      let x,y,z be Nat;

      hereby

        assume

         A1: x in (( Segm y) \ ( Segm z));

         not x in ( Segm z) by A1, XBOOLE_0:def 5;

        hence z <= x by NAT_1: 44;

        x in ( Segm y) by A1, XBOOLE_0:def 5;

        hence x < y by NAT_1: 44;

      end;

      assume z <= x & x < y;

      then x in ( Segm y) & not x in ( Segm z) by NAT_1: 44;

      hence x in (( Segm y) \ ( Segm z)) by XBOOLE_0:def 5;

    end;

    theorem :: MYCIELSK:3

    

     Th3: for A,B,C,D,E,X be 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;

      assume

       A1: X c= A or X c= B or X c= C or X c= D or X c= E;

      per cases by A1;

        suppose X c= A;

        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;

      end;

        suppose X c= B;

        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;

      end;

        suppose X c= C;

        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;

      end;

        suppose X c= D;

        then X c= (((A \/ B) \/ C) \/ D) by XBOOLE_1: 10;

        hence X c= ((((A \/ B) \/ C) \/ D) \/ E) by XBOOLE_1: 10;

      end;

        suppose X c= E;

        hence X c= ((((A \/ B) \/ C) \/ D) \/ E) by XBOOLE_1: 10;

      end;

    end;

    theorem :: MYCIELSK:4

    

     Th4: for A,B,C,D,E,x be 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;

      hereby

        assume x in ((((A \/ B) \/ C) \/ D) \/ 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;

      end;

      assume

       A1: x in A or x in B or x in C or x in D or x in E;

      per cases by A1;

        suppose x in A;

        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;

      end;

        suppose x in B;

        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;

      end;

        suppose x in C;

        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;

      end;

        suppose x in D;

        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;

      end;

        suppose x in E;

        hence x in ((((A \/ B) \/ C) \/ D) \/ E) by XBOOLE_0:def 3;

      end;

    end;

    theorem :: MYCIELSK:5

    

     Th5: for R be symmetric RelStr, x,y be 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 by NECKLACE:def 3, RELAT_2:def 3;

    theorem :: MYCIELSK:6

    

     Th6: for R be symmetric RelStr, x,y be Element of R st x <= y holds y <= x

    proof

      let R be symmetric RelStr, x,y be Element of R;

      assume

       A1: x <= y;

      set cR = the carrier of R, iR = the InternalRel of R;

      

       A2: iR is_symmetric_in cR by NECKLACE:def 3;

      

       A3: [x, y] in iR by A1, ORDERS_2:def 5;

      then x in cR & y in cR by ZFMISC_1: 87;

      then [y, x] in iR by A2, A3;

      hence y <= x by ORDERS_2:def 5;

    end;

    begin

    theorem :: MYCIELSK:7

    

     Th7: for X be set, P be a_partition of X holds ( card P) c= ( card X)

    proof

      let X be set, P be a_partition of X;

      defpred P[ object, object] means ex D1 be set st D1 = $1 & $2 = the Element of D1;

      

       A1: for e be object st e in P holds ex u be object st P[e, u]

      proof

        let e be object;

        assume e in P;

        reconsider ee = e as set by TARSKI: 1;

        take u = the Element of ee;

        thus P[e, u];

      end;

      consider f be Function such that

       A2: ( dom f) = P and

       A3: for e be object st e in P holds P[e, (f . e)] from CLASSES1:sch 1( A1);

      

       A4: f is one-to-one

      proof

        let x1,x2 be object such that

         A5: x1 in ( dom f) and

         A6: x2 in ( dom f) and

         A7: (f . x1) = (f . x2);

        

         A8: x1 <> {} by A2, A5;

        

         A9: x2 <> {} by A2, A6;

        reconsider xx1 = x1, xx2 = x2 as set by TARSKI: 1;

         P[x1, (f . x1)] & P[x2, (f . x2)] by A5, A6, A2, A3;

        then (f . x1) = the Element of xx1 & (f . x2) = the Element of xx2;

        then xx1 meets xx2 by A7, A8, A9, XBOOLE_0: 3;

        hence x1 = x2 by A5, A6, A2, EQREL_1:def 4;

      end;

      ( rng f) c= X

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A10: x in ( dom f) and

         A11: y = (f . x) by FUNCT_1:def 3;

        reconsider x as set by TARSKI: 1;

         P[x, (f . x)] by A2, A3, A10;

        then

         A12: (f . x) = the Element of x;

        x <> {} by A2, A10;

        then (f . x) in x by A12;

        hence y in X by A10, A2, A11;

      end;

      hence ( card P) c= ( card X) by A2, A4, CARD_1: 10;

    end;

    definition

      let X be set, P be a_partition of X, S be Subset of X;

      :: MYCIELSK:def1

      func P | S -> a_partition of S equals { (x /\ S) where x be Element of P : x meets S };

      coherence

      proof

        set D = { (x /\ S) where x be Element of P : x meets S };

        

         A1: D c= ( bool S)

        proof

          let a be object;

          reconsider aa = a as set by TARSKI: 1;

          assume a in D;

          then

          consider x be Element of P such that

           A2: a = (x /\ S) and x meets S;

          aa c= S by A2, XBOOLE_1: 17;

          hence thesis;

        end;

        

         A3: ( union D) = S

        proof

          thus ( union D) c= S

          proof

            let x be object;

            assume x in ( union D);

            then

            consider Y be set such that

             A4: x in Y and

             A5: Y in D by TARSKI:def 4;

            thus x in S by A4, A1, A5;

          end;

          thus S c= ( union D)

          proof

            let s be object;

            assume

             A6: s in S;

            then s in X;

            then s in ( union P) by EQREL_1:def 4;

            then

            consider p be 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 D by A8;

            s in (p /\ S) by A7, A6, XBOOLE_0:def 4;

            hence s in ( union D) by A9, TARSKI:def 4;

          end;

        end;

        now

          let A be Subset of S;

          assume A in D;

          then

          consider x be Element of P such that

           A10: A = (x /\ S) and

           A11: x meets S;

          consider z be object 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;

          let B be Subset of S;

          assume B in D;

          then

          consider y be Element of P such that

           A14: B = (y /\ S) and y meets S;

          

           A15: x in Pp1 & y in Pp1;

          per cases by A15, EQREL_1:def 4;

            suppose x = y;

            hence A = B or A misses B by A10, A14;

          end;

            suppose x misses y;

            hence A = B or A misses B by A10, A14, XBOOLE_1: 76;

          end;

        end;

        hence thesis by A1, A3, EQREL_1:def 4;

      end;

    end

    registration

      let X be set;

      cluster finite for a_partition of X;

      existence

      proof

        per cases ;

          suppose X = {} ;

          hence thesis by EQREL_1: 45;

        end;

          suppose X <> {} ;

          then {X} is a_partition of X by EQREL_1: 39;

          hence thesis;

        end;

      end;

    end

    registration

      let X be set, P be finite a_partition of X, S be Subset of X;

      cluster (P | S) -> finite;

      coherence

      proof

        defpred P[ object, object] means ex D1 be set st D1 = $1 & $2 = (D1 /\ S);

        

         A1: for e be object st e in P holds ex u be object st P[e, u]

        proof

          let e be object;

          assume e in P;

          reconsider ee = e as set by TARSKI: 1;

          take (ee /\ S);

          thus thesis;

        end;

        consider f be Function such that

         A2: ( dom f) = P and

         A3: for e be object st e in P holds P[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 object;

          assume x in (P | S);

          then

          consider xx be Element of P such that

           A5: x = (xx /\ S) and

           A6: xx meets S;

          consider y be object 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 P[xx, (f . xx)] by A3;

          then x = (f . xx) by A5;

          hence x in ( rng f) by A8, A2, FUNCT_1:def 3;

        end;

        hence thesis by A4;

      end;

    end

    theorem :: MYCIELSK:8

    

     Th8: for X be set, P be finite a_partition of X, S be Subset of X holds ( card (P | S)) <= ( card P)

    proof

      let X be set, P be finite a_partition of X, S be Subset of X;

      per cases ;

        suppose X = {} ;

        then S = {} ;

        hence ( card (P | S)) <= ( card P);

      end;

        suppose X <> {} ;

        then

        reconsider Pp1 = P as finite non empty set;

        defpred P[ set] means $1 meets S;

        deffunc F( set) = ($1 /\ S);

        

         A3: (P | S) = { F(x) where x be Element of Pp1 : P[x] };

        ( card (P | S)) <= ( card Pp1) from DILWORTH:sch 1( A3);

        hence thesis;

      end;

    end;

    theorem :: MYCIELSK:9

    

     Th9: for X be set, P be finite a_partition of X, S be Subset of X holds (for p be set st p in P holds p meets S) iff ( card (P | S)) = ( card P)

    proof

      let X be set, P be finite a_partition of X, S be Subset of X;

      per cases ;

        suppose X = {} ;

        hence thesis;

      end;

        suppose

         A2: X <> {} ;

        set PS = (P | S);

        reconsider Pp1 = P as finite non empty set by A2;

        hereby

          assume

           A3: for p be set st p in P holds p meets S;

          set p = the Element of P;

          p in Pp1;

          then p meets S by A3;

          then (p /\ S) in PS;

          then

          reconsider PSp1 = PS as non empty finite set;

          defpred P[ object, object] means ex D1 be set st D1 = $1 & $1 in P & $2 = (D1 /\ S);

          

           A4: for x be object st x in P holds ex y be object st y in PSp1 & P[x, y]

          proof

            let x be object;

            assume

             A5: x in P;

            reconsider xx = x as set by TARSKI: 1;

            take (xx /\ S);

            xx meets S by A5, A3;

            hence thesis by A5;

          end;

          consider f be Function of P, PSp1 such that

           A6: for x be object st x in P holds P[x, (f . x)] from FUNCT_2:sch 1( A4);

          now

            let x1,x2 be object such that

             A7: x1 in P and

             A8: x2 in P and

             A9: (f . x1) = (f . x2);

            reconsider xx1 = x1, xx2 = x2 as set by TARSKI: 1;

             P[x1, (f . x1)] by A7, A6;

            then

             A10: (f . x1) = (xx1 /\ S);

             P[x2, (f . x2)] by A8, A6;

            then

             A11: (f . x2) = (xx2 /\ S);

            xx1 meets S by A7, A3;

            then (f . x1) in PS by A10, A7;

            then (f . x1) <> {} ;

            then

            consider x be object such that

             A12: x in (f . x1) by XBOOLE_0:def 1;

            x in xx1 & x in xx2 by A12, A9, A10, A11, XBOOLE_0:def 4;

            then xx1 meets xx2 by XBOOLE_0: 3;

            hence x1 = x2 by A7, A8, EQREL_1:def 4;

          end;

          then

           A13: f is one-to-one by FUNCT_2: 19;

          ( rng f) = PSp1

          proof

            thus ( rng f) c= PSp1

            proof

              let y be object;

              assume y in ( rng f);

              then

              consider x be object such that

               A14: x in P and

               A15: (f . x) = y by FUNCT_2: 11;

              reconsider x as set by TARSKI: 1;

              

               A16: x meets S by A3, A14;

               P[x, (f . x)] by A14, A6;

              then

              consider D1 be set such that

               A17: D1 = x & x in P & (f . x) = (D1 /\ S);

              thus y in PSp1 by A15, A17, A16;

            end;

            thus PSp1 c= ( rng f)

            proof

              let y be object;

              assume y in PSp1;

              then

              consider p be Element of P such that

               A18: y = (p /\ S) and p meets S;

              

               A19: p in Pp1;

               P[p, (f . p)] by A6, A19;

              then (f . p) = (p /\ S);

              hence y in ( rng f) by A18, A19, FUNCT_2: 4;

            end;

          end;

          then f is onto by FUNCT_2:def 3;

          hence ( card (P | S)) = ( card P) by A13, EULER_1: 11;

        end;

        assume

         A20: ( card (P | S)) = ( card P);

        defpred P[ object, object] means ex D2 be set st D2 = $2 & $1 in PS & $2 in Pp1 & $1 = (D2 /\ S);

        

         A21: for x be object st x in PS holds ex y be object st y in Pp1 & P[x, y]

        proof

          let x be object;

          assume

           A22: x in PS;

          then

          consider p be Element of P such that

           A23: x = (p /\ S) and p meets S;

          take p;

          thus thesis by A22, A23;

        end;

        consider f be Function of PS, Pp1 such that

         A24: for x be object st x in PS holds P[x, (f . x)] from FUNCT_2:sch 1( A21);

        

         A25: f is one-to-one

        proof

          let x1,x2 be object such that

           A26: x1 in ( dom f) and

           A27: x2 in ( dom f) and

           A28: (f . x1) = (f . x2);

          

           A29: P[x2, (f . x2)] by A27, A24;

           P[x1, (f . x1)] by A26, A24;

          then x1 = ((f . x1) /\ S);

          hence x1 = x2 by A28, A29;

        end;

        f is onto by A20, A25, FINSEQ_4: 63;

        then

         A30: ( rng f) = P by FUNCT_2:def 3;

        let p be set;

        assume p in P;

        then

        consider ps be object such that

         A31: ps in ( dom f) and

         A32: p = (f . ps) by A30, FUNCT_1:def 3;

         P[ps, (f . ps)] by A31, A24;

        then

         A33: ps = (p /\ S) by A32;

        reconsider ps as set by TARSKI: 1;

        ps is non empty by A31;

        then ex x be object st x in ps;

        hence p meets S by A33;

      end;

    end;

    theorem :: MYCIELSK:10

    

     Th10: for R be RelStr, C be Coloring of R, S be Subset of R holds (C | S) is Coloring of ( subrelstr S)

    proof

      let R be RelStr, C be Coloring of R, S be Subset of R;

      set sS = ( subrelstr S);

      

       A1: the carrier of sS = S by YELLOW_0:def 15;

      now

        let x be set;

        assume x in (C | S);

        then

        consider c be Element of C such that

         A2: x = (c /\ S) and

         A3: c meets S;

        consider z be object such that z in c and

         A4: z in S by A3, XBOOLE_0: 3;

        

         A5: sS is non empty by A4, YELLOW_0:def 15;

        

         A6: R is non empty by A4;

        reconsider Rp1 = R as non empty RelStr by A4;

        reconsider xp1 = x as Subset of sS by A1, A2, XBOOLE_1: 17;

        xp1 is stable

        proof

          let a,b be Element of sS such that

           A7: a in xp1 and

           A8: b in xp1 and

           A9: a <> b;

          

           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;

          C is Coloring of Rp1;

          then c in C;

          then

          reconsider cp1 = c as Subset of R;

          

           A11: cp1 is stable by DILWORTH:def 12;

          assume a <= b or b <= a;

          then ap1 <= bp1 or bp1 <= ap1 by YELLOW_0: 59;

          hence contradiction by A9, A10, A11;

        end;

        hence x is StableSet of sS;

      end;

      hence (C | S) is Coloring of sS by A1, DILWORTH:def 12;

    end;

    begin

    definition

      let R be RelStr;

      :: MYCIELSK:def2

      attr R is with_finite_chromatic# means

      : Def2: ex C be Coloring of R st C is finite;

    end

    registration

      cluster with_finite_chromatic# for RelStr;

      existence

      proof

        take R = the empty RelStr;

        reconsider S = {} as a_partition of the carrier of R by EQREL_1: 45;

        take S;

        thus S is finite;

      end;

    end

    registration

      cluster finite -> with_finite_chromatic# for RelStr;

      coherence

      proof

        let R be RelStr;

        set cR = the carrier of R;

        assume

         A1: R is finite;

        per cases ;

          suppose R is empty;

          then

          reconsider S = {} as a_partition of cR by EQREL_1: 45;

          for x be set st x in S holds x is StableSet of R;

          then

          reconsider S as Coloring of R by DILWORTH:def 12;

          take S;

          thus S is finite;

        end;

          suppose

           A2: R is non empty;

          reconsider cRp1 = cR as finite non empty set by A2, A1;

          set S = ( SmallestPartition cR);

          deffunc F( set) = {$1};

          

           A3: S = { F(x) where x be Element of cRp1 : P[x] } by EQREL_1: 37;

          

           A4: { F(x) where x be Element of cRp1 : P[x] } is finite from PRE_CIRC:sch 1;

          now

            let z be set;

            assume z in S;

            then ex x be Element of cR st z = {x} by A3;

            hence z is StableSet of R by A2, SUBSET_1: 33;

          end;

          then

          reconsider S as Coloring of R by DILWORTH:def 12;

          take S;

          thus thesis by A4;

        end;

      end;

    end

    registration

      let R be with_finite_chromatic# RelStr;

      cluster finite for Coloring of R;

      existence by Def2;

    end

    registration

      let R be with_finite_chromatic# RelStr, S be Subset of R;

      cluster ( subrelstr S) -> with_finite_chromatic#;

      coherence

      proof

        set sS = ( subrelstr S);

        consider C be Coloring of R such that

         A1: C is finite by Def2;

        

         A2: the carrier of sS = S by YELLOW_0:def 15;

        reconsider CS = (C | S) as a_partition of S;

        for x be set st x in CS holds x is StableSet of sS

        proof

          let x be set;

          assume x in CS;

          then

          consider X be Element of C such that

           A3: x = (X /\ S) and

           A4: X meets S;

          ex y be object 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 sS by A3, DILWORTH: 31;

        end;

        then CS is Coloring of sS by A2, DILWORTH:def 12;

        hence thesis by A1;

      end;

    end

    definition

      let R be with_finite_chromatic# RelStr;

      :: MYCIELSK:def3

      func chromatic# R -> Nat means

      : Def3: (ex C be finite Coloring of R st ( card C) = it ) & for C be finite Coloring of R holds it <= ( card C);

      existence

      proof

        defpred P[ Nat] means ex C be finite Coloring of R st ( card C) = $1;

        consider C be Coloring of R such that

         A1: C is finite by Def2;

        ( card C) = ( card C);

        then

         A2: ex k be Nat st P[k] by A1;

        consider n be Nat such that

         A3: P[n] and

         A4: for k be Nat st P[k] holds n <= k from NAT_1:sch 5( A2);

        take n;

        thus ex C be finite Coloring of R st ( card C) = n by A3;

        let C be finite Coloring of R;

        thus n <= ( card C) by A4;

      end;

      uniqueness

      proof

        let it1,it2 be Nat such that

         A5: ex C be finite Coloring of R st ( card C) = it1 and

         A6: for C be finite Coloring of R holds it1 <= ( card C) and

         A7: ex C be finite Coloring of R st ( card C) = it2 and

         A8: for C be finite Coloring of R holds it2 <= ( card C);

        consider C1 be finite Coloring of R such that

         A9: ( card C1) = it1 by A5;

        consider C2 be 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;

      end;

    end

    registration

      let R be empty RelStr;

      cluster ( chromatic# R) -> empty;

      coherence

      proof

        consider C be finite Coloring of R such that

         A1: ( card C) = ( chromatic# R) by Def3;

        thus thesis by A1;

      end;

    end

    registration

      let R be non empty with_finite_chromatic# RelStr;

      cluster ( chromatic# R) -> positive;

      coherence

      proof

        ex C be finite Coloring of R st ( card C) = ( chromatic# R) by Def3;

        hence thesis;

      end;

    end

    definition

      let R be RelStr;

      :: MYCIELSK:def4

      attr R is with_finite_cliquecover# means

      : Def4: ex C be Clique-partition of R st C is finite;

    end

    registration

      cluster with_finite_cliquecover# for RelStr;

      existence

      proof

        take R = the empty RelStr;

        reconsider S = {} as a_partition of the carrier of R by EQREL_1: 45;

        reconsider S as Clique-partition of R;

        take S;

        thus S is finite;

      end;

    end

    registration

      cluster finite -> with_finite_cliquecover# for RelStr;

      coherence

      proof

        let R be RelStr;

        set cR = the carrier of R;

        assume

         A1: R is finite;

        per cases ;

          suppose R is empty;

          then

          reconsider S = {} as a_partition of cR by EQREL_1: 45;

          for x be set st x in S holds x is Clique of R;

          then

          reconsider S as Clique-partition of R by DILWORTH:def 11;

          take S;

          thus S is finite;

        end;

          suppose

           A2: R is non empty;

          reconsider cRp1 = cR as finite non empty set by A2, A1;

          set S = ( SmallestPartition cR);

          deffunc F( set) = {$1};

          

           A3: S = { F(x) where x be Element of cRp1 : P[x] } by EQREL_1: 37;

          

           A4: { F(x) where x be Element of cRp1 : P[x] } is finite from PRE_CIRC:sch 1;

          now

            let z be set;

            assume

             A5: z in S;

            ex x be Element of cR st z = {x} by A5, A3;

            hence z is Clique of R by A2, SUBSET_1: 33;

          end;

          then

          reconsider S as Clique-partition of R by DILWORTH:def 11;

          take S;

          thus thesis by A4;

        end;

      end;

    end

    registration

      let R be with_finite_cliquecover# RelStr;

      cluster finite for Clique-partition of R;

      existence by Def4;

    end

    registration

      let R be with_finite_cliquecover# RelStr, S be Subset of R;

      cluster ( subrelstr S) -> with_finite_cliquecover#;

      coherence

      proof

        set sS = ( subrelstr S);

        consider C be Clique-partition of R such that

         A1: C is finite by Def4;

        

         A2: the carrier of sS = S by YELLOW_0:def 15;

        reconsider CS = (C | S) as a_partition of S;

        for x be set st x in CS holds x is Clique of sS

        proof

          let x be set;

          assume x in CS;

          then

          consider X be Element of C such that

           A3: x = (X /\ S) and

           A4: X meets S;

          ex y be object 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 sS by A3, DILWORTH: 29;

        end;

        then CS is Clique-partition of sS by A2, DILWORTH:def 11;

        hence thesis by A1;

      end;

    end

    definition

      let R be with_finite_cliquecover# RelStr;

      :: MYCIELSK:def5

      func cliquecover# R -> Nat means

      : Def5: (ex C be finite Clique-partition of R st ( card C) = it ) & for C be finite Clique-partition of R holds it <= ( card C);

      existence

      proof

        defpred P[ Nat] means ex C be finite Clique-partition of R st ( card C) = $1;

        consider C be Clique-partition of R such that

         A1: C is finite by Def4;

        ( card C) = ( card C);

        then

         A2: ex k be Nat st P[k] by A1;

        consider n be Nat such that

         A3: P[n] and

         A4: for k be Nat st P[k] holds n <= k from NAT_1:sch 5( A2);

        take n;

        thus ex C be finite Clique-partition of R st ( card C) = n by A3;

        let C be finite Clique-partition of R;

        thus n <= ( card C) by A4;

      end;

      uniqueness

      proof

        let it1,it2 be Nat such that

         A5: ex C be finite Clique-partition of R st ( card C) = it1 and

         A6: for C be finite Clique-partition of R holds it1 <= ( card C) and

         A7: ex C be finite Clique-partition of R st ( card C) = it2 and

         A8: for C be finite Clique-partition of R holds it2 <= ( card C);

        consider C1 be finite Clique-partition of R such that

         A9: ( card C1) = it1 by A5;

        consider C2 be 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;

      end;

    end

    registration

      let R be empty RelStr;

      cluster ( cliquecover# R) -> empty;

      coherence

      proof

        consider C be finite Clique-partition of R such that

         A1: ( card C) = ( cliquecover# R) by Def5;

        thus thesis by A1;

      end;

    end

    registration

      let R be non empty with_finite_cliquecover# RelStr;

      cluster ( cliquecover# R) -> positive;

      coherence

      proof

        consider C be finite Clique-partition of R such that

         A1: ( card C) = ( cliquecover# R) by Def5;

        thus thesis by A1;

      end;

    end

    theorem :: MYCIELSK:11

    

     Th11: for R be finite RelStr holds ( clique# R) <= ( card the carrier of R)

    proof

      let R be finite RelStr;

      consider C be finite Clique of R such that

       A1: ( card C) = ( clique# R) by DILWORTH:def 4;

      ( Segm ( card C)) c= ( Segm ( card the carrier of R)) by CARD_1: 11;

      hence ( clique# R) <= ( card the carrier of R) by A1, NAT_1: 39;

    end;

    theorem :: MYCIELSK:12

    for R be finite RelStr holds ( stability# R) <= ( card the carrier of R)

    proof

      let R be finite RelStr;

      consider C be finite StableSet of R such that

       A1: ( card C) = ( stability# R) by DILWORTH:def 6;

      ( Segm ( card C)) c= ( Segm ( card the carrier of R)) by CARD_1: 11;

      hence ( stability# R) <= ( card the carrier of R) by A1, NAT_1: 39;

    end;

    theorem :: MYCIELSK:13

    

     Th13: for R be finite RelStr holds ( chromatic# R) <= ( card the carrier of R)

    proof

      let R be finite RelStr;

      consider C be finite Coloring of R such that

       A1: ( card C) = ( chromatic# R) by Def3;

      ( Segm ( card C)) c= ( Segm ( card the carrier of R)) by Th7;

      hence ( chromatic# R) <= ( card the carrier of R) by A1, NAT_1: 39;

    end;

    theorem :: MYCIELSK:14

    for R be finite RelStr holds ( cliquecover# R) <= ( card the carrier of R)

    proof

      let R be finite RelStr;

      consider C be finite Clique-partition of R such that

       A1: ( card C) = ( cliquecover# R) by Def5;

      ( Segm ( card C)) c= ( Segm ( card the carrier of R)) by Th7;

      hence ( cliquecover# R) <= ( card the carrier of R) by A1, NAT_1: 39;

    end;

    theorem :: MYCIELSK:15

    

     Th15: for R be with_finite_clique# with_finite_chromatic# RelStr holds ( clique# R) <= ( chromatic# R)

    proof

      let P be with_finite_clique# with_finite_chromatic# RelStr;

      assume

       A1: ( clique# P) > ( chromatic# P);

      consider A be Clique of P such that

       A2: ( card A) = ( clique# P) by DILWORTH:def 4;

      consider C be finite Coloring of P such that

       A3: ( card C) = ( chromatic# P) by Def3;

      ( card ( Segm ( card C))) = ( card C) & ( card ( Segm ( card A))) = ( card A);

      then

       A4: ( card C) in ( card A) by A3, A1, A2, NAT_1: 41;

      set cP = the carrier of P;

      per cases ;

        suppose P is empty;

        hence contradiction by A1;

      end;

        suppose

         A5: P is non empty;

        defpred P[ object, object] means ex D2 be set st D2 = $2 & $1 in A & $2 in C & $1 in D2;

        

         A6: for x be object st x in A holds ex y be object st y in C & P[x, y]

        proof

          let x be object;

          assume

           A7: x in A;

          then

          reconsider xp1 = x as Element of P;

          cP is non empty by A5;

          then xp1 in cP;

          then x in ( union C) by EQREL_1:def 4;

          then

          consider y be set such that

           A8: x in y and

           A9: y in C by TARSKI:def 4;

          take y;

          thus thesis by A7, A8, A9;

        end;

        consider f be Function of A, C such that

         A10: for x be object st x in A holds P[x, (f . x)] from FUNCT_2:sch 1( A6);

        consider x,y be object 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;

         P[x, (f . x)] & P[y, (f . y)] by A11, A12, A10;

        then x in (f . x) & y in (f . x) by A14;

        hence contradiction by A15, A11, A12, A13, DILWORTH: 15;

      end;

    end;

    theorem :: MYCIELSK:16

    for R be with_finite_stability# with_finite_cliquecover# RelStr holds ( stability# R) <= ( cliquecover# R)

    proof

      let R be with_finite_stability# with_finite_cliquecover# RelStr;

      assume

       A1: ( stability# R) > ( cliquecover# R);

      consider A be StableSet of R such that

       A2: ( card A) = ( stability# R) by DILWORTH:def 6;

      consider C be finite Clique-partition of R such that

       A3: ( card C) = ( cliquecover# R) by Def5;

      ( card ( Segm ( card C))) = ( card C) & ( card ( Segm ( card A))) = ( card A);

      then

       A4: ( card C) in ( card A) by A3, A1, A2, NAT_1: 41;

      set cR = the carrier of R;

      per cases ;

        suppose R is empty;

        hence contradiction by A1;

      end;

        suppose

         A5: R is non empty;

        defpred P[ object, object] means ex D2 be set st D2 = $2 & $1 in A & $2 in C & $1 in D2;

        

         A6: for x be object st x in A holds ex y be object st y in C & P[x, y]

        proof

          let x be object such that

           A7: x in A;

          reconsider xp1 = x as Element of R by A7;

          cR is non empty by A5;

          then xp1 in cR;

          then x in ( union C) by EQREL_1:def 4;

          then

          consider y be set such that

           A8: x in y and

           A9: y in C by TARSKI:def 4;

          take y;

          thus thesis by A7, A8, A9;

        end;

        consider f be Function of A, C such that

         A10: for x be object st x in A holds P[x, (f . x)] from FUNCT_2:sch 1( A6);

        consider x,y be object 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;

         P[x, (f . x)] & P[y, (f . y)] by A11, A12, A10;

        then x in (f . x) & y in (f . x) by A14;

        hence contradiction by A15, A11, A12, A13, DILWORTH: 15;

      end;

    end;

    begin

    theorem :: MYCIELSK:17

    

     Th17: for R be RelStr, x,y be Element of R, a,b be Element of ( ComplRelStr R) st x = a & y = b & x <= y holds not a <= b

    proof

      let R be RelStr, x,y be Element of R, a,b be Element of ( ComplRelStr R) such that

       A1: x = a and

       A2: y = b;

      set cR = the carrier of R, iR = the InternalRel of R;

      set CR = ( ComplRelStr R);

      set iCR = the InternalRel of CR;

      

       A3: iCR = ((iR ` ) \ ( id cR)) by NECKLACE:def 8;

      assume x <= y;

      then [x, y] in iR by ORDERS_2:def 5;

      then not [x, y] in (iR ` ) by XBOOLE_0:def 5;

      then not [x, y] in iCR by A3, XBOOLE_0:def 5;

      hence not a <= b by A1, A2, ORDERS_2:def 5;

    end;

    theorem :: MYCIELSK:18

    

     Th18: for R be RelStr, x,y be Element of R, a,b be 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, x,y be Element of R, a,b be Element of ( ComplRelStr R) such that

       A1: x = a and

       A2: y = b and

       A3: x <> y and

       A4: x in the carrier of R;

      set cR = the carrier of R, iR = the InternalRel of R;

      set CR = ( ComplRelStr R);

      set iCR = the InternalRel of CR;

      

       A5: iCR = ((iR ` ) \ ( id cR)) by NECKLACE:def 8;

      

       A6: [x, y] in [:cR, cR:] by A4, ZFMISC_1:def 2;

      assume not a <= b;

      then

       A7: not [x, y] in iCR by A1, A2, ORDERS_2:def 5;

       not [x, y] in ( id cR) by A3, RELAT_1:def 10;

      then not [x, y] in (iR ` ) by A5, A7, XBOOLE_0:def 5;

      then [x, y] in iR by A6, XBOOLE_0:def 5;

      hence x <= y by ORDERS_2:def 5;

    end;

    registration

      let R be finite RelStr;

      cluster ( ComplRelStr R) -> finite;

      coherence

      proof

        the carrier of R = the carrier of ( ComplRelStr R) by NECKLACE:def 8;

        hence thesis;

      end;

    end

    theorem :: MYCIELSK:19

    

     Th19: for R be symmetric RelStr, C be Clique of R holds C is StableSet of ( ComplRelStr R)

    proof

      let R be symmetric RelStr, C be Clique of R;

      now

        let x,y be Element of ( ComplRelStr R) such that

         A1: x in C and

         A2: y in C and

         A3: x <> y;

        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;

      end;

      hence C is StableSet of ( ComplRelStr R) by DILWORTH:def 2, NECKLACE:def 8;

    end;

    theorem :: MYCIELSK:20

    

     Th20: for R be symmetric RelStr, C be Clique of ( ComplRelStr R) holds C is StableSet of R

    proof

      let R be symmetric RelStr, C be Clique of ( ComplRelStr R);

      now

        let x,y be Element of R such that

         A1: x in C and

         A2: y in C and

         A3: x <> y;

        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;

      end;

      hence C is StableSet of R by DILWORTH:def 2, NECKLACE:def 8;

    end;

    theorem :: MYCIELSK:21

    

     Th21: for R be RelStr, C be StableSet of R holds C is Clique of ( ComplRelStr R)

    proof

      let R be RelStr, C be StableSet of R;

      set CR = ( ComplRelStr R);

      

       A1: C is Subset of CR by NECKLACE:def 8;

      now

        let a,b be Element of CR such that

         A2: a in C and

         A3: b in C and

         A4: a <> b;

        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;

      end;

      hence C is Clique of ( ComplRelStr R) by A1, DILWORTH: 6;

    end;

    theorem :: MYCIELSK:22

    

     Th22: for R be RelStr, C be StableSet of ( ComplRelStr R) holds C is Clique of R

    proof

      let R be RelStr, C be StableSet of ( ComplRelStr R);

      

       A1: the carrier of R = the carrier of ( ComplRelStr R) by NECKLACE:def 8;

      now

        let a,b be Element of R such that

         A2: a in C and

         A3: b in C and

         A4: a <> b;

        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;

      end;

      hence C is Clique of R by DILWORTH: 6, NECKLACE:def 8;

    end;

    registration

      let R be with_finite_clique# RelStr;

      cluster ( ComplRelStr R) -> with_finite_stability#;

      coherence

      proof

        set CR = ( ComplRelStr R);

        consider C be finite Clique of R such that

         A1: for D be finite Clique of R holds ( card D) <= ( card C) by DILWORTH:def 3;

        assume not thesis;

        then

         A2: for A be finite StableSet of CR holds ex B be finite StableSet of CR st ( card B) > ( card A);

        defpred P[ Nat] means ex S be finite StableSet of CR st ( card S) > $1;

        consider B be finite StableSet of CR such that

         A3: ( card B) > ( card ( {} CR)) by A2;

        

         A4: P[ 0 ] by A3;

        

         A5: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          assume P[n];

          then

          consider S be finite StableSet of CR such that

           A6: ( card S) > n;

          consider T be finite StableSet of CR 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 P[(n + 1)];

        end;

        for n be Nat holds P[n] from NAT_1:sch 2( A4, A5);

        then

        consider S be finite StableSet of CR such that

         A8: ( card S) > ( card C);

        S is Clique of R by Th22;

        hence contradiction by A1, A8;

      end;

    end

    registration

      let R be with_finite_stability# symmetric RelStr;

      cluster ( ComplRelStr R) -> with_finite_clique#;

      coherence

      proof

        set CR = ( ComplRelStr R);

        consider C be finite StableSet of R such that

         A1: for D be finite StableSet of R holds ( card D) <= ( card C) by DILWORTH:def 5;

        assume not thesis;

        then

         A2: for C be finite Clique of CR holds ex D be finite Clique of CR st ( card D) > ( card C);

        defpred P[ Nat] means ex S be finite Clique of CR st ( card S) > $1;

        consider B be finite Clique of CR such that

         A3: ( card B) > ( card ( {} CR)) by A2;

        

         A4: P[ 0 ] by A3;

        

         A5: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          assume P[n];

          then

          consider S be finite Clique of CR such that

           A6: ( card S) > n;

          consider T be finite Clique of CR 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 P[(n + 1)];

        end;

        for n be Nat holds P[n] from NAT_1:sch 2( A4, A5);

        then

        consider S be finite Clique of CR such that

         A8: ( card S) > ( card C);

        S is StableSet of R by Th20;

        hence contradiction by A1, A8;

      end;

    end

    theorem :: MYCIELSK:23

    

     Th23: for R be with_finite_clique# symmetric RelStr holds ( clique# R) = ( stability# ( ComplRelStr R))

    proof

      let R be with_finite_clique# symmetric RelStr;

      set k = ( stability# ( ComplRelStr R));

      consider A be finite StableSet of ( ComplRelStr R) such that

       A1: ( card A) = k by DILWORTH:def 6;

      A is Clique of R by Th22;

      then

       A2: ex C be finite Clique of R st ( card C) = k by A1;

      now

        let T be finite Clique of R;

        T is StableSet of ( ComplRelStr R) by Th19;

        hence ( card T) <= k by DILWORTH:def 6;

      end;

      hence ( clique# R) = ( stability# ( ComplRelStr R)) by A2, DILWORTH:def 4;

    end;

    theorem :: MYCIELSK:24

    for R be with_finite_stability# symmetric RelStr holds ( stability# R) = ( clique# ( ComplRelStr R))

    proof

      let R be with_finite_stability# symmetric RelStr;

      set CR = ( ComplRelStr R);

      set k = ( clique# CR);

      consider A be finite Clique of CR such that

       A1: ( card A) = k by DILWORTH:def 4;

      A is StableSet of R by Th20;

      then

       A2: ex C be finite StableSet of R st ( card C) = k by A1;

      now

        let T be finite StableSet of R;

        T is Clique of CR by Th21;

        hence ( card T) <= k by DILWORTH:def 4;

      end;

      hence ( stability# R) = ( clique# ( ComplRelStr R)) by A2, DILWORTH:def 6;

    end;

    theorem :: MYCIELSK:25

    

     Th25: for R be RelStr, C be Coloring of R holds C is Clique-partition of ( ComplRelStr R)

    proof

      let R be RelStr, C be Coloring of R;

      

       A1: the carrier of R = the carrier of ( ComplRelStr R) by NECKLACE:def 8;

      now

        let x be set;

        assume x in C;

        then x is StableSet of R by DILWORTH:def 12;

        hence x is Clique of ( ComplRelStr R) by Th21;

      end;

      hence C is Clique-partition of ( ComplRelStr R) by A1, DILWORTH:def 11;

    end;

    theorem :: MYCIELSK:26

    

     Th26: for R be symmetric RelStr, C be Clique-partition of ( ComplRelStr R) holds C is Coloring of R

    proof

      let R be symmetric RelStr, C be Clique-partition of ( ComplRelStr R);

      set CR = ( ComplRelStr R);

      

       A1: the carrier of R = the carrier of CR by NECKLACE:def 8;

      now

        let x be set;

        assume x in C;

        then x is Clique of CR by DILWORTH:def 11;

        hence x is StableSet of R by Th20;

      end;

      hence C is Coloring of R by A1, DILWORTH:def 12;

    end;

    theorem :: MYCIELSK:27

    

     Th27: for R be symmetric RelStr, C be Clique-partition of R holds C is Coloring of ( ComplRelStr R)

    proof

      let R be symmetric RelStr, C be Clique-partition of R;

      set CR = ( ComplRelStr R);

      

       A1: the carrier of R = the carrier of CR by NECKLACE:def 8;

      now

        let x be set;

        assume x in C;

        then x is Clique of R by DILWORTH:def 11;

        hence x is StableSet of CR by Th19;

      end;

      hence C is Coloring of ( ComplRelStr R) by A1, DILWORTH:def 12;

    end;

    theorem :: MYCIELSK:28

    

     Th28: for R be RelStr, C be Coloring of ( ComplRelStr R) holds C is Clique-partition of R

    proof

      let R be RelStr, C be Coloring of ( ComplRelStr R);

      set CR = ( ComplRelStr R);

      

       A1: the carrier of R = the carrier of CR by NECKLACE:def 8;

      now

        let x be set;

        assume x in C;

        then x is StableSet of CR by DILWORTH:def 12;

        hence x is Clique of R by Th22;

      end;

      hence C is Clique-partition of R by A1, DILWORTH:def 11;

    end;

    registration

      let R be with_finite_chromatic# RelStr;

      cluster ( ComplRelStr R) -> with_finite_cliquecover#;

      coherence

      proof

        consider C be Coloring of R such that

         A1: C is finite by Def2;

        C is Clique-partition of ( ComplRelStr R) by Th25;

        hence thesis by A1;

      end;

    end

    registration

      let R be with_finite_cliquecover# symmetric RelStr;

      cluster ( ComplRelStr R) -> with_finite_chromatic#;

      coherence

      proof

        consider C be Clique-partition of R such that

         A1: C is finite by Def4;

        C is Coloring of ( ComplRelStr R) by Th27;

        hence thesis by A1;

      end;

    end

    theorem :: MYCIELSK:29

    

     Th29: for R be with_finite_chromatic# symmetric RelStr holds ( chromatic# R) = ( cliquecover# ( ComplRelStr R))

    proof

      let R be with_finite_chromatic# symmetric RelStr;

      set CR = ( ComplRelStr R);

      set k = ( cliquecover# CR);

      consider C be finite Clique-partition of CR such that

       A1: ( card C) = k by Def5;

      C is Coloring of R by Th26;

      then

       A2: ex C be finite Coloring of R st ( card C) = k by A1;

      now

        let C be finite Coloring of R;

        assume

         A3: k > ( card C);

        C is Clique-partition of CR by Th25;

        hence contradiction by A3, Def5;

      end;

      hence ( chromatic# R) = ( cliquecover# CR) by A2, Def3;

    end;

    theorem :: MYCIELSK:30

    for R be with_finite_cliquecover# symmetric RelStr holds ( cliquecover# R) = ( chromatic# ( ComplRelStr R))

    proof

      let R be with_finite_cliquecover# symmetric RelStr;

      set CR = ( ComplRelStr R);

      set k = ( chromatic# CR);

      consider C be finite Coloring of CR such that

       A1: ( card C) = k by Def3;

      C is Clique-partition of R by Th28;

      then

       A2: ex C be finite Clique-partition of R st ( card C) = k by A1;

      now

        let C be finite Clique-partition of R;

        assume

         A3: k > ( card C);

        C is Coloring of CR by Th27;

        hence contradiction by A3, Def3;

      end;

      hence ( cliquecover# R) = ( chromatic# CR) by A2, Def5;

    end;

    begin

    definition

      let R be RelStr, v be Element of R;

      :: MYCIELSK:def6

      func Adjacent v -> Subset of R means

      : Def6: for x be Element of R holds x in it iff x < v or v < x;

      existence

      proof

        set D = { x where x be Element of R : x < v or v < x };

        set cR = the carrier of R, iR = the InternalRel of R;

        D c= the carrier of R

        proof

          let x be object;

          assume x in D;

          then

          consider a be Element of R such that

           A1: x = a and

           A2: a < v or v < a;

          per cases by A2;

            suppose a < v;

            then a <= v by ORDERS_2:def 6;

            then [a, v] in iR by ORDERS_2:def 5;

            then [a, v] in [:cR, cR:];

            hence x in the carrier of R by A1, ZFMISC_1: 87;

          end;

            suppose v < a;

            then v <= a by ORDERS_2:def 6;

            then [v, a] in iR by ORDERS_2:def 5;

            then [v, a] in [:cR, cR:];

            hence x in the carrier of R by A1, ZFMISC_1: 87;

          end;

        end;

        then

        reconsider D as Subset of R;

        take D;

        let x be Element of R;

        hereby

          assume x in D;

          then

          consider a be Element of R such that

           A3: x = a and

           A4: a < v or v < a;

          thus x < v or v < x by A3, A4;

        end;

        assume x < v or v < x;

        hence x in D;

      end;

      uniqueness

      proof

        let it1,it2 be Subset of R such that

         A5: for x be Element of R holds x in it1 iff x < v or v < x and

         A6: for x be Element of R holds x in it2 iff x < v or v < x;

        hereby

          let x be object;

          assume

           A7: x in it1;

          then

          reconsider xp1 = x as Element of R;

          xp1 < v or v < xp1 by A5, A7;

          hence x in it2 by A6;

        end;

        let x be object;

        assume

         A8: x in it2;

        then

        reconsider xp1 = x as Element of R;

        xp1 < v or v < xp1 by A6, A8;

        hence x in it1 by A5;

      end;

    end

    theorem :: MYCIELSK:31

    

     Th31: for R be with_finite_chromatic# RelStr, C be finite Coloring of R, c be set st c in C & ( card C) = ( chromatic# R) holds ex v be Element of R st v in c & for d be Element of C st d <> c holds ex w be Element of R st w in ( Adjacent v) & w in d

    proof

      let R be with_finite_chromatic# RelStr, C be finite Coloring of R, c be set such that

       A1: c in C and

       A2: ( card C) = ( chromatic# R);

      assume

       A3: not thesis;

      set cR = the carrier of R;

      

       A4: ( union C) = cR by EQREL_1:def 4;

      reconsider c as Subset of cR by A1;

      

       A5: c <> {} by A1;

      set Cc = (C \ {c});

      

       A6: c in {c} by TARSKI:def 1;

      per cases ;

        suppose

         A7: Cc is empty;

        consider v be object such that

         A8: v in c by A5, XBOOLE_0:def 1;

        reconsider v as Element of R by A8;

        consider d be Element of C such that

         A9: d <> c and for w be Element of R holds not (w in ( Adjacent v) & 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 be object such that

         A10: C = {x} by CARD_2: 42;

        c = x & d = x by A1, A10, TARSKI:def 1;

        hence thesis by A9;

      end;

        suppose Cc is non empty;

        then

        reconsider Cc as non empty set;

        defpred P[ object, object] means ex D2 be set st D2 = $2 & for vv be Element of cR st $1 = vv holds $2 <> c & $2 in C & for w be Element of R holds not (w in ( Adjacent vv) & w in D2);

        

         A11: for e be object st e in c holds ex u be object st P[e, u]

        proof

          let v be object such that

           A12: v in c;

          reconsider vv = v as Element of cR by A12;

          consider d be Element of C such that

           A13: d <> c and

           A14: for w be Element of R holds not (w in ( Adjacent vv) & w in d) by A12, A3;

          take d, d;

          thus thesis by A13, A14, A1;

        end;

        consider r be Function such that

         A15: ( dom r) = c and

         A16: for e be object st e in c holds P[e, (r . e)] from CLASSES1:sch 1( A11);

        deffunc DF( set) = ($1 \/ (r " {$1}));

        reconsider Cc as finite non empty set;

        set D = { DF(d) where d be Element of Cc : P[d] };

        consider d be object such that

         A17: d in Cc by XBOOLE_0:def 1;

        reconsider d as set by TARSKI: 1;

        

         A18: (d \/ (r " {d})) in D by A17;

        

         A19: D c= ( bool cR)

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in D;

          then

          consider d be Element of Cc such that

           A20: x = (d \/ (r " {d}));

          

           A21: (r " {d}) c= c by A15, RELAT_1: 132;

          

           A22: (r " {d}) c= cR by A21, XBOOLE_1: 1;

          d in C by XBOOLE_0:def 5;

          then xx c= cR by A20, A22, XBOOLE_1: 8;

          hence x in ( bool cR);

        end;

        

         A23: ( union D) = cR

        proof

          thus ( union D) c= cR

          proof

            let x be object;

            assume x in ( union D);

            then

            consider Y be set such that

             A24: x in Y and

             A25: Y in D by TARSKI:def 4;

            thus x in cR by A24, A25, A19;

          end;

          thus cR c= ( union D)

          proof

            let x be object;

            assume

             A26: x in cR;

            then

            consider d be set such that

             A27: x in d and

             A28: d in C by A4, TARSKI:def 4;

            reconsider xp1 = x as Element of cR by A26;

            per cases ;

              suppose

               A29: d = c;

              then

               A30: P[xp1, (r . xp1)] by A27, A16;

              then (r . xp1) <> c;

              then

               A31: not (r . xp1) in {c} by TARSKI:def 1;

              (r . xp1) in C by A30;

              then

               A32: (r . xp1) in Cc by A31, 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

               A33: x in ((r . xp1) \/ (r " {(r . xp1)})) by XBOOLE_0:def 3;

              ((r . xp1) \/ (r " {(r . xp1)})) in D by A32;

              hence x in ( union D) by A33, TARSKI:def 4;

            end;

              suppose d <> c;

              then not d in {c} by TARSKI:def 1;

              then d in Cc by A28, XBOOLE_0:def 5;

              then

               A34: (d \/ (r " {d})) in D;

              x in (d \/ (r " {d})) by A27, XBOOLE_0:def 3;

              hence x in ( union D) by A34, TARSKI:def 4;

            end;

          end;

        end;

        

         A35: for A be Subset of cR st A in D holds A <> {} & for B be Subset of cR st B in D holds A = B or A misses B

        proof

          let A be Subset of cR;

          assume A in D;

          then

          consider da be Element of Cc such that

           A36: A = (da \/ (r " {da}));

          

           A37: da in C by XBOOLE_0:def 5;

          then da is non empty;

          hence A <> {} by A36;

          let B be Subset of cR;

          assume B in D;

          then

          consider db be Element of Cc such that

           A38: B = (db \/ (r " {db}));

          

           A39: db in C by XBOOLE_0:def 5;

          per cases ;

            suppose da = db;

            hence A = B or A misses B by A36, A38;

          end;

            suppose

             A40: da <> db;

            then

             A41: da misses db by A37, A39, EQREL_1:def 4;

            

             A42: (r " {da}) misses (r " {db}) by A40, FUNCT_1: 71, ZFMISC_1: 11;

            assume A <> B;

            assume A meets B;

            then

            consider x be object such that

             A43: x in A and

             A44: x in B by XBOOLE_0: 3;

            per cases by A43, A44, A36, A38, XBOOLE_0:def 3;

              suppose x in da & x in db;

              hence contradiction by A41, XBOOLE_0: 3;

            end;

              suppose that

               A45: x in da and

               A46: x in (r " {db});

              

               A47: da <> c by A6, XBOOLE_0:def 5;

              (r " {db}) c= c by A15, RELAT_1: 132;

              then da meets c by A45, A46, XBOOLE_0: 3;

              hence contradiction by A47, A37, A1, EQREL_1:def 4;

            end;

              suppose that

               A48: x in (r " {da}) and

               A49: x in db;

              

               A50: db <> c by A6, XBOOLE_0:def 5;

              (r " {da}) c= c by A15, RELAT_1: 132;

              then db meets c by A48, A49, XBOOLE_0: 3;

              hence contradiction by A50, A39, A1, EQREL_1:def 4;

            end;

              suppose x in (r " {da}) & x in (r " {db});

              hence contradiction by A42, XBOOLE_0: 3;

            end;

          end;

        end;

        reconsider D as a_partition of cR by A19, A23, A35, EQREL_1:def 4;

        now

          let x be set;

          assume

           A51: x in D;

          then

          reconsider S = x as Subset of R;

          consider d be Element of Cc such that

           A52: x = (d \/ (r " {d})) by A51;

          

           A53: (r " {d}) c= c by A15, RELAT_1: 132;

          

           A54: d in C by XBOOLE_0:def 5;

          

           A55: d is StableSet of R by A54, DILWORTH:def 12;

          

           A56: c is StableSet of R by A1, DILWORTH:def 12;

          S is stable

          proof

            let a,b be Element of R such that

             A57: a in S and

             A58: b in S and

             A59: a <> b;

            per cases by A57, A58, A52, XBOOLE_0:def 3;

              suppose a in d & b in d;

              hence not a <= b & not b <= a by A55, A59, DILWORTH:def 2;

            end;

              suppose that

               A60: a in d and

               A61: b in (r " {d});

              (r . b) in {d} by A61, FUNCT_1:def 7;

              then

               A62: (r . b) = d by TARSKI:def 1;

               P[b, (r . b)] by A53, A61, A16;

              then not a in ( Adjacent b) by A60, A62;

              then not a < b & not b < a by Def6;

              hence not a <= b & not b <= a by A59, ORDERS_2:def 6;

            end;

              suppose that

               A63: a in (r " {d}) and

               A64: b in d;

              (r . a) in {d} by A63, FUNCT_1:def 7;

              then

               A65: (r . a) = d by TARSKI:def 1;

               P[a, (r . a)] by A53, A63, A16;

              then not b in ( Adjacent a) by A64, A65;

              then not a < b & not b < a by Def6;

              hence not a <= b & not b <= a by A59, ORDERS_2:def 6;

            end;

              suppose a in (r " {d}) & b in (r " {d});

              hence not a <= b & not b <= a by A53, A56, A59, DILWORTH:def 2;

            end;

          end;

          hence x is StableSet of R;

        end;

        then

        reconsider 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

         A66: ( card Cc) < ( card C) by NAT_1: 13;

        deffunc FS( set) = ($1 \/ (r " {$1}));

        consider s be Function such that

         A67: ( dom s) = Cc and

         A68: for x be set st x in Cc holds (s . x) = FS(x) from FUNCT_1:sch 5;

        

         A69: ( rng s) c= D

        proof

          let y be object;

          assume y in ( rng s);

          then

          consider d be object such that

           A70: d in ( dom s) and

           A71: y = (s . d) by FUNCT_1:def 3;

          reconsider d as set by TARSKI: 1;

          y = (d \/ (r " {d})) by A67, A68, A70, A71;

          hence y in D by A70, A67;

        end;

        then

        reconsider s as Function of Cc, D by A67, FUNCT_2: 2;

        

         A72: s is one-to-one

        proof

          let x1,x2 be object such that

           A73: x1 in ( dom s) and

           A74: x2 in ( dom s) and

           A75: (s . x1) = (s . x2);

          reconsider x1, x2 as set by TARSKI: 1;

          

           A76: (s . x1) = (x1 \/ (r " {x1})) by A73, A68;

          

           A77: (s . x2) = (x2 \/ (r " {x2})) by A74, A68;

          

           A78: x1 c= x2

          proof

            let x be object;

            assume

             A79: x in x1;

            then

             A80: x in (s . x1) by A76, XBOOLE_0:def 3;

            per cases by A80, A75, A77, XBOOLE_0:def 3;

              suppose x in x2;

              hence thesis;

            end;

              suppose

               A81: x in (r " {x2});

              

               A82: (r " {x2}) c= ( dom r) by RELAT_1: 132;

              

               A83: x1 in C by A73, XBOOLE_0:def 5;

              then

              reconsider x1 as Subset of cR;

              x1 meets c by A82, A81, A15, A79, XBOOLE_0: 3;

              then x1 = c by A83, A1, EQREL_1:def 4;

              hence thesis by A6, A73, XBOOLE_0:def 5;

            end;

          end;

          x2 c= x1

          proof

            let x be object;

            assume

             A84: x in x2;

            then

             A85: x in (s . x2) by A77, XBOOLE_0:def 3;

            per cases by A85, A75, A76, XBOOLE_0:def 3;

              suppose x in x1;

              hence thesis;

            end;

              suppose

               A86: x in (r " {x1});

              

               A87: (r " {x1}) c= ( dom r) by RELAT_1: 132;

              

               A88: x2 in C by A74, XBOOLE_0:def 5;

              then

              reconsider x2 as Subset of cR;

              x2 meets c by A87, A86, A15, A84, XBOOLE_0: 3;

              then x2 = c by A88, A1, EQREL_1:def 4;

              hence thesis by A6, A74, XBOOLE_0:def 5;

            end;

          end;

          hence thesis by A78, XBOOLE_0:def 10;

        end;

        D c= ( rng s)

        proof

          let x be object;

          assume x in D;

          then

          consider d be Element of Cc such that

           A89: x = (d \/ (r " {d}));

          (s . d) = (d \/ (r " {d})) by A68;

          hence x in ( rng s) by A89, A67, FUNCT_1:def 3;

        end;

        then D = ( rng s) by A69;

        then s is onto by FUNCT_2:def 3;

        then

         A90: ( card Cc) = ( card D) by A72, A18, EULER_1: 11;

        then D is finite;

        hence contradiction by A66, A90, A2, Def3;

      end;

    end;

    begin

    definition

      let n be Nat;

      :: MYCIELSK:def7

      mode NatRelStr of n -> strict RelStr means

      : Def7: the carrier of it = n;

      existence

      proof

        reconsider I = {} as Relation of n, n by RELSET_1: 12;

        take RelStr (# n, I #);

        thus thesis;

      end;

    end

    registration

      cluster -> empty for NatRelStr of 0 ;

      coherence by Def7;

    end

    registration

      let n be non zero Nat;

      cluster -> non empty for NatRelStr of n;

      coherence by Def7;

    end

    registration

      let n be Nat;

      cluster -> finite for NatRelStr of n;

      coherence by Def7;

      cluster irreflexive for NatRelStr of n;

      existence

      proof

        reconsider I = {} as Relation of n, n by RELSET_1: 12;

        set R = RelStr (# n, I #);

        reconsider R as NatRelStr of n by Def7;

        R is irreflexive;

        hence thesis;

      end;

    end

    definition

      let n be Nat;

      :: MYCIELSK:def8

      func CompleteRelStr n -> NatRelStr of n means

      : Def8: the InternalRel of it = ( [:n, n:] \ ( id n));

      existence

      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;

        thus the InternalRel of R = ( [:n, n:] \ ( id n));

      end;

      uniqueness

      proof

        let C1,C2 be NatRelStr of n;

        the carrier of C1 = n & the carrier of C2 = n by Def7;

        hence thesis;

      end;

    end

    theorem :: MYCIELSK:32

    

     Th32: for n be Nat, x,y be 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, x,y be set;

      assume

       A1: x in n & y in n;

      hereby

        assume [x, y] in the InternalRel of ( CompleteRelStr n);

        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;

      end;

      assume x <> y;

      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;

    end;

    registration

      let n be Nat;

      cluster ( CompleteRelStr n) -> irreflexive symmetric;

      coherence

      proof

        set R = ( CompleteRelStr n);

        set cR = the carrier of R, iR = the InternalRel of R;

        

         A1: cR = n by Def7;

        thus R is irreflexive by A1, Th32;

        thus R is symmetric

        proof

          let x,y be object;

          assume x in cR & y in cR;

          then

           A2: x in n & y in n by Def7;

          assume [x, y] in iR;

          hence thesis by A2, Th32;

        end;

      end;

    end

    registration

      let n be Nat;

      cluster ( [#] ( CompleteRelStr n)) -> clique;

      coherence

      proof

        set R = ( CompleteRelStr n);

        set iR = the InternalRel of R;

        let x,y be object;

        assume x in ( [#] R) & y in ( [#] R);

        then

         A1: x in n & y in n by Def7;

        assume x <> y;

        hence [x, y] in iR or [y, x] in iR by A1, Th32;

      end;

    end

    theorem :: MYCIELSK:33

    

     Th33: for n be Nat holds ( clique# ( CompleteRelStr n)) = n

    proof

      let n be Nat;

      set R = ( CompleteRelStr n);

      

       A1: ( card ( card n)) = ( card n);

      ( [#] R) = n by Def7;

      then

       A2: ex C be finite Clique of R st ( card C) = n by A1;

      for T be finite Clique of R holds ( card T) <= n

      proof

        let T be finite Clique of R;

        ( card n) = n;

        then

         A3: ( card the carrier of R) = n by Def7;

        

         A4: ( card T) <= ( clique# R) by DILWORTH:def 4;

        ( clique# R) <= n by A3, Th11;

        hence thesis by A4, XXREAL_0: 2;

      end;

      hence ( clique# R) = n by A2, DILWORTH:def 4;

    end;

    theorem :: MYCIELSK:34

    for n be non zero Nat holds ( stability# ( CompleteRelStr n)) = 1

    proof

      let n be non zero Nat;

      set R = ( CompleteRelStr n);

      ( [#] R) is Clique of R;

      hence ( stability# ( CompleteRelStr n)) = 1 by DILWORTH: 20;

    end;

    theorem :: MYCIELSK:35

    

     Th35: for n be Nat holds ( chromatic# ( CompleteRelStr n)) = n

    proof

      let n be Nat;

      set R = ( CompleteRelStr n);

      ( clique# R) = n by Th33;

      then

       A1: n <= ( chromatic# R) by Th15;

      

       A2: ( chromatic# R) <= ( card the carrier of R) by Th13;

      ( card n) = n;

      then ( card the carrier of R) = n by Def7;

      hence ( chromatic# ( CompleteRelStr n)) = n by A1, A2, XXREAL_0: 1;

    end;

    theorem :: MYCIELSK:36

    for n be non zero Nat holds ( cliquecover# ( CompleteRelStr n)) = 1

    proof

      let n be non zero Nat;

      set R = ( CompleteRelStr n);

      set cR = the carrier of R;

      reconsider C = {cR} as a_partition of cR by EQREL_1: 39;

       A1:

      now

        let x be set;

        assume x in C;

        then x = ( [#] R) by TARSKI:def 1;

        hence x is Clique of R;

      end;

       A2:

      now

        take C;

        thus C is finite;

        thus C is Clique-partition of R by A1, DILWORTH:def 11;

        thus ( card C) = 1 by CARD_1: 30;

      end;

      now

        let C be finite Clique-partition of R;

        ( 0 + 1) <= ( card C) by NAT_1: 13;

        hence 1 <= ( card C);

      end;

      hence ( cliquecover# ( CompleteRelStr n)) = 1 by A2, Def5;

    end;

    begin

    definition

      let n be Nat, R be NatRelStr of n;

      :: MYCIELSK:def9

      func Mycielskian R -> NatRelStr of ((2 * n) + 1) means

      : Def9: the InternalRel of it = ((((the InternalRel of R \/ { [x, (y + n)] where x,y be Element of NAT : [x, y] in the InternalRel of R }) \/ { [(x + n), y] where x,y be Element of NAT : [x, y] in the InternalRel of R }) \/ [: {(2 * n)}, ((2 * n) \ n):]) \/ [:((2 * n) \ n), {(2 * n)}:]);

      existence

      proof

        set cR = the carrier of R, iR = the InternalRel of R;

        set cMR = ((2 * n) + 1);

        set iMR = ((((iR \/ { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR }) \/ { [(x + n), y] where x,y be Element of NAT : [x, y] in iR }) \/ [: {(2 * n)}, ((2 * n) \ n):]) \/ [:((2 * n) \ n), {(2 * n)}:]);

        

         A1: cR = n by Def7;

        n <= (n + n) by NAT_1: 11;

        then

         A2: n < ((2 * n) + 1) by NAT_1: 13;

        iMR c= [:cMR, cMR:]

        proof

          let z be object;

          assume

           A3: z in iMR;

          per cases by A3, Th4;

            suppose z in iR;

            then

            consider c,d be object such that

             A4: c in ( Segm n) and

             A5: d in ( Segm n) and

             A6: z = [c, d] by ZFMISC_1:def 2, A1;

            reconsider c, d as Nat by A4, A5;

            c < n & d < n by A4, A5, NAT_1: 44;

            then c < cMR & d < cMR by A2, XXREAL_0: 2;

            then c in ( Segm cMR) & d in ( Segm cMR) by NAT_1: 44;

            hence z in [:cMR, cMR:] by A6, ZFMISC_1:def 2;

          end;

            suppose z in { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR };

            then

            consider x,y be Element of NAT such that

             A7: z = [x, (y + n)] and

             A8: [x, y] in iR;

            x in ( Segm n) by A1, A8, ZFMISC_1: 87;

            then x < n by NAT_1: 44;

            then x < cMR by A2, XXREAL_0: 2;

            then

             A9: x in ( Segm cMR) by NAT_1: 44;

            y in ( Segm n) by A1, A8, ZFMISC_1: 87;

            then y < n by 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 ( Segm cMR) by NAT_1: 44;

            hence z in [:cMR, cMR:] by A7, A9, ZFMISC_1:def 2;

          end;

            suppose z in { [(x + n), y] where x,y be Element of NAT : [x, y] in iR };

            then

            consider x,y be Element of NAT such that

             A10: z = [(x + n), y] and

             A11: [x, y] in iR;

            y in ( Segm n) by A1, A11, ZFMISC_1: 87;

            then y < n by NAT_1: 44;

            then y < cMR by A2, XXREAL_0: 2;

            then

             A12: y in ( Segm cMR) by NAT_1: 44;

            x in ( Segm n) by A1, A11, ZFMISC_1: 87;

            then x < n by 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 ( Segm cMR) by NAT_1: 44;

            hence z in [:cMR, cMR:] by A10, A12, ZFMISC_1:def 2;

          end;

            suppose z in [: {(2 * n)}, ((2 * n) \ n):];

            then

            consider c,d be object such that

             A13: c in {(2 * n)} and

             A14: d in (( Segm (2 * n)) \ ( Segm n)) and

             A15: z = [c, d] by ZFMISC_1:def 2;

            

             A16: c = (2 * n) by A13, TARSKI:def 1;

            reconsider c as Nat by A13, TARSKI:def 1;

            c < ((2 * n) + 1) by A16, NAT_1: 13;

            then

             A17: c in ( Segm cMR) by NAT_1: 44;

            reconsider d as Nat by A14;

            d < (2 * n) by A14, Th2;

            then d < cMR by NAT_1: 13;

            then d in ( Segm cMR) by NAT_1: 44;

            hence z in [:cMR, cMR:] by A17, A15, ZFMISC_1:def 2;

          end;

            suppose z in [:((2 * n) \ n), {(2 * n)}:];

            then

            consider c,d be object such that

             A18: c in (( Segm (2 * n)) \ ( Segm 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 as Nat by A19, TARSKI:def 1;

            d < ((2 * n) + 1) by A21, NAT_1: 13;

            then

             A22: d in ( Segm cMR) by NAT_1: 44;

            reconsider c as Nat by A18;

            c < (2 * n) by A18, Th2;

            then c < cMR by NAT_1: 13;

            then c in ( Segm cMR) by NAT_1: 44;

            hence z in [:cMR, cMR:] by A22, A20, ZFMISC_1:def 2;

          end;

        end;

        then

        reconsider iMR as Relation of cMR;

        set MR = RelStr (# cMR, iMR #);

        take MR;

        thus the carrier of MR = ((2 * n) + 1);

        thus the InternalRel of MR = ((((iR \/ { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR }) \/ { [(x + n), y] where x,y be Element of NAT : [x, y] in iR }) \/ [: {(2 * n)}, ((2 * n) \ n):]) \/ [:((2 * n) \ n), {(2 * n)}:]);

      end;

      uniqueness

      proof

        let A,B be NatRelStr of ((2 * n) + 1);

        the carrier of A = ((2 * n) + 1) & the carrier of B = ((2 * n) + 1) by Def7;

        hence thesis;

      end;

    end

    theorem :: MYCIELSK:37

    

     Th37: for n be Nat, R be NatRelStr of n holds the carrier of R c= the carrier of ( Mycielskian R)

    proof

      let n be Nat, R be NatRelStr of n;

      

       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 ( Segm n) c= ( Segm ((2 * n) + 1)) by NAT_1: 39;

      hence the carrier of R c= the carrier of ( Mycielskian R) by A1, Def7;

    end;

    theorem :: MYCIELSK:38

    

     Th38: for n be Nat, R be NatRelStr of n, x,y be Nat st [x, y] in the InternalRel of ( Mycielskian R) holds 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, R be NatRelStr of n, a,b be Nat;

      set cR = the carrier of R, iR = the InternalRel of R;

      defpred LHS[] means [a, b] in the InternalRel of ( Mycielskian R);

      defpred RHS[] 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) = ((((iR \/ { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR }) \/ { [(x + n), y] where x,y be Element of NAT : [x, y] in iR }) \/ [: {(2 * n)}, ((2 * n) \ n):]) \/ [:((2 * n) \ n), {(2 * n)}:]) by Def9;

      assume

       A2: LHS[];

      per cases by A2, A1, Th4;

        suppose [a, b] in iR;

        then a in cR & b in cR by ZFMISC_1: 87;

        then a in ( Segm n) & b in ( Segm n) by Def7;

        hence RHS[] by NAT_1: 44;

      end;

        suppose [a, b] in { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR };

        then

        consider x,y be Element of NAT such that

         A3: [x, (y + n)] = [a, b] and

         A4: [x, y] in iR;

        y in cR by A4, ZFMISC_1: 87;

        then y in ( Segm n) by Def7;

        then y < n by NAT_1: 44;

        then

         A5: (y + n) < (n + n) by XREAL_1: 6;

        x in cR by A4, ZFMISC_1: 87;

        then x in ( Segm n) by Def7;

        then x < n by NAT_1: 44;

        hence RHS[] by A5, A3, XTUPLE_0: 1;

      end;

        suppose [a, b] in { [(x + n), y] where x,y be Element of NAT : [x, y] in iR };

        then

        consider x,y be Element of NAT such that

         A6: [(x + n), y] = [a, b] and

         A7: [x, y] in iR;

        x in cR by A7, ZFMISC_1: 87;

        then x in ( Segm n) by Def7;

        then x < n by NAT_1: 44;

        then

         A8: (x + n) < (n + n) by XREAL_1: 6;

        y in cR by A7, ZFMISC_1: 87;

        then y in ( Segm n) by Def7;

        then y < n by NAT_1: 44;

        hence RHS[] by A8, A6, XTUPLE_0: 1;

      end;

        suppose

         A9: [a, b] in [: {(2 * n)}, ((2 * n) \ n):];

        

         A10: b in (( Segm (2 * n)) \ ( Segm n)) by A9, ZFMISC_1: 87;

        a in {(2 * n)} by A9, ZFMISC_1: 87;

        hence RHS[] by A10, Th2, TARSKI:def 1;

      end;

        suppose

         A11: [a, b] in [:((2 * n) \ n), {(2 * n)}:];

        

         A12: a in (( Segm (2 * n)) \ ( Segm n)) by A11, ZFMISC_1: 87;

        b in {(2 * n)} by A11, ZFMISC_1: 87;

        hence RHS[] by A12, Th2, TARSKI:def 1;

      end;

    end;

    theorem :: MYCIELSK:39

    

     Th39: for n be Nat, R be NatRelStr of n holds the InternalRel of R c= the InternalRel of ( Mycielskian R)

    proof

      let n be Nat, R be NatRelStr of n;

      set iR = the InternalRel of R;

      set MR = ( Mycielskian R);

      set iMR = the InternalRel of MR;

      iMR = ((((iR \/ { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR }) \/ { [(x + n), y] where x,y be Element of NAT : [x, y] in iR }) \/ [: {(2 * n)}, ((2 * n) \ n):]) \/ [:((2 * n) \ n), {(2 * n)}:]) by Def9;

      hence iR c= iMR by Th3;

    end;

    theorem :: MYCIELSK:40

    

     Th40: for n be Nat, R be NatRelStr of n, x,y be set st x in ( Segm n) & y in ( Segm n) & [x, y] in the InternalRel of ( Mycielskian R) holds [x, y] in the InternalRel of R

    proof

      let n be Nat, R be NatRelStr of n, a,b be set such that

       A1: a in ( Segm n) and

       A2: b in ( Segm n) and

       A3: [a, b] in the InternalRel of ( Mycielskian R);

      set iR = the InternalRel of R;

      set MR = ( Mycielskian R);

      set iMR = the InternalRel of MR;

      

       A4: iMR = ((((iR \/ { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR }) \/ { [(x + n), y] where x,y be Element of NAT : [x, y] in iR }) \/ [: {(2 * n)}, ((2 * n) \ n):]) \/ [:((2 * n) \ n), {(2 * n)}:]) by Def9;

      per cases by A3, A4, Th4;

        suppose [a, b] in iR;

        hence [a, b] in iR;

      end;

        suppose [a, b] in { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR };

        then

        consider x,y be Element of NAT such that

         A5: [a, b] = [x, (y + n)] and [x, y] in iR;

        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 iR;

      end;

        suppose [a, b] in { [(x + n), y] where x,y be Element of NAT : [x, y] in iR };

        then

        consider x,y be Element of NAT such that

         A6: [a, b] = [(x + n), y] and [x, y] in iR;

        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 iR;

      end;

        suppose [a, b] in [: {(2 * n)}, ((2 * n) \ n):];

        then

        consider c,d be object 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 iR;

      end;

        suppose [a, b] in [:((2 * n) \ n), {(2 * n)}:];

        then

        consider c,d be object 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 iR;

      end;

    end;

    theorem :: MYCIELSK:41

    

     Th41: for n be Nat, R be NatRelStr of n, x,y be 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, R be NatRelStr of n, a,b be Nat such that

       A1: [a, b] in the InternalRel of R;

      set iR = the InternalRel of R;

      set MR = ( Mycielskian R);

      set iMR = the InternalRel of MR;

      

       A2: iMR = ((((iR \/ { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR }) \/ { [(x + n), y] where x,y be Element of NAT : [x, y] in iR }) \/ [: {(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 be Element of NAT : [x, y] in iR } by A1;

      hence [a, (b + n)] in iMR by A2, Th4;

       [(ap1 + n), bp1] in { [(x + n), y] where x,y be Element of NAT : [x, y] in iR } by A1;

      hence [(a + n), b] in iMR by A2, Th4;

    end;

    theorem :: MYCIELSK:42

    

     Th42: for n be Nat, R be NatRelStr of n, x,y be Nat st x in ( Segm n) & [x, (y + n)] in the InternalRel of ( Mycielskian R) holds [x, y] in the InternalRel of R

    proof

      let n be Nat, R be NatRelStr of n, a,b be Nat;

      set cR = the carrier of R, iR = the InternalRel of R;

      set MR = ( Mycielskian R);

      set iMR = the InternalRel of MR;

      assume that

       A1: a in ( Segm n) and

       A2: [a, (b + n)] in iMR;

      

       A3: iMR = ((((iR \/ { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR }) \/ { [(x + n), y] where x,y be Element of NAT : [x, y] in iR }) \/ [: {(2 * n)}, ((2 * n) \ n):]) \/ [:((2 * n) \ n), {(2 * n)}:]) by Def9;

      per cases by A2, A3, Th4;

        suppose [a, (b + n)] in iR;

        then (b + n) in cR by ZFMISC_1: 87;

        then (b + n) in ( Segm 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 iR;

      end;

        suppose [a, (b + n)] in { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR };

        then

        consider x,y be Element of NAT such that

         A4: [a, (b + n)] = [x, (y + n)] and

         A5: [x, y] in iR;

        (b + n) = (y + n) by A4, XTUPLE_0: 1;

        hence [a, b] in iR by A5, A4, XTUPLE_0: 1;

      end;

        suppose [a, (b + n)] in { [(x + n), y] where x,y be Element of NAT : [x, y] in iR };

        then

        consider x,y be Element of NAT such that

         A6: [a, (b + n)] = [(x + n), y] and

         A7: [x, y] in iR;

        (b + n) = y by A6, XTUPLE_0: 1;

        then (b + n) in cR by A7, ZFMISC_1: 87;

        then (b + n) in ( Segm 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 iR;

      end;

        suppose [a, (b + n)] in [: {(2 * n)}, ((2 * n) \ n):];

        then

        consider c,d be object 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 iR;

      end;

        suppose [a, (b + n)] in [:((2 * n) \ n), {(2 * n)}:];

        then

        consider c,d be object such that

         A12: c in (( Segm (2 * n)) \ ( Segm 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 iR by A1, NAT_1: 44;

      end;

    end;

    theorem :: MYCIELSK:43

    

     Th43: for n be Nat, R be NatRelStr of n, x,y be Nat st y in ( Segm n) & [(x + n), y] in the InternalRel of ( Mycielskian R) holds [x, y] in the InternalRel of R

    proof

      let n be Nat, R be NatRelStr of n, a,b be Nat;

      set cR = the carrier of R, iR = the InternalRel of R;

      set MR = ( Mycielskian R);

      set iMR = the InternalRel of MR;

      assume that

       A1: b in ( Segm n) and

       A2: [(a + n), b] in iMR;

      

       A3: iMR = ((((iR \/ { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR }) \/ { [(x + n), y] where x,y be Element of NAT : [x, y] in iR }) \/ [: {(2 * n)}, ((2 * n) \ n):]) \/ [:((2 * n) \ n), {(2 * n)}:]) by Def9;

      per cases by A2, A3, Th4;

        suppose [(a + n), b] in iR;

        then (a + n) in cR by ZFMISC_1: 87;

        then (a + n) in ( Segm 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 iR;

      end;

        suppose [(a + n), b] in { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR };

        then

        consider x,y be Element of NAT such that

         A4: [(a + n), b] = [x, (y + n)] and

         A5: [x, y] in iR;

        (a + n) = x by A4, XTUPLE_0: 1;

        then (a + n) in cR by A5, ZFMISC_1: 87;

        then (a + n) in ( Segm 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 iR;

      end;

        suppose [(a + n), b] in { [(x + n), y] where x,y be Element of NAT : [x, y] in iR };

        then

        consider x,y be Element of NAT such that

         A6: [(a + n), b] = [(x + n), y] and

         A7: [x, y] in iR;

        (a + n) = (x + n) by A6, XTUPLE_0: 1;

        hence [a, b] in iR by A7, A6, XTUPLE_0: 1;

      end;

        suppose [(a + n), b] in [: {(2 * n)}, ((2 * n) \ n):];

        then

        consider c,d be object such that c in {(2 * n)} and

         A8: d in (( Segm (2 * n)) \ ( Segm 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 iR by A1, NAT_1: 44;

      end;

        suppose [(a + n), b] in [:((2 * n) \ n), {(2 * n)}:];

        then

        consider c,d be object 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 iR;

      end;

    end;

    theorem :: MYCIELSK:44

    

     Th44: for n be Nat, R be NatRelStr of n, m be 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, R be NatRelStr of n, m be Nat such that

       A1: n <= m and

       A2: m < (2 * n);

      set iR = the InternalRel of R;

      set MR = ( Mycielskian R);

      set iMR = the InternalRel of MR;

      

       A3: iMR = ((((iR \/ { [x, (y + n)] where x,y be Element of NAT : [x, y] in iR }) \/ { [(x + n), y] where x,y be Element of NAT : [x, y] in iR }) \/ [: {(2 * n)}, ((2 * n) \ n):]) \/ [:((2 * n) \ n), {(2 * n)}:]) by Def9;

      

       A4: m in (( Segm (2 * n)) \ ( Segm 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 iMR by A3, XBOOLE_0:def 3;

       [(2 * n), m] in [: {(2 * n)}, ((2 * n) \ n):] by A4, A5, ZFMISC_1:def 2;

      hence [(2 * n), m] in iMR by A3, Th4;

    end;

    theorem :: MYCIELSK:45

    

     Th45: for n be Nat, R be NatRelStr of n, S be Subset of ( Mycielskian R) st S = n holds R = ( subrelstr S)

    proof

      let n be Nat, R be NatRelStr of n, S be Subset of ( Mycielskian R) such that

       A1: S = n;

      set cR = the carrier of R, iR = the InternalRel of R;

      set sS = ( subrelstr S);

      set csS = the carrier of sS;

      set isS = the InternalRel of sS;

      set MR = ( Mycielskian R);

      set cMR = the carrier of MR, iMR = the InternalRel of MR;

      

       A2: cR = n by Def7;

      

       A3: csS = n by A1, YELLOW_0:def 15;

      

       A4: iR = isS

      proof

        thus iR c= isS

        proof

          let z be object;

          assume

           A5: z in iR;

          then

          consider x,y be object such that

           A6: x in cR and

           A7: y in cR and

           A8: z = [x, y] by ZFMISC_1:def 2;

          cR c= cMR by Th37;

          then

          reconsider xMR = x, yMR = y as Element of MR by A6, A7;

          reconsider xsS = x, ysS = y as Element of sS by A6, A7, Def7, A3;

          iR c= iMR 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 isS by A8, ORDERS_2:def 5;

        end;

        thus isS c= iR

        proof

          let z be object;

          assume

           A9: z in isS;

          then

          consider x,y be object such that

           A10: x in ( Segm n) and

           A11: y in ( Segm n) and

           A12: z = [x, y] by ZFMISC_1:def 2, A3;

          cR c= cMR by Th37;

          then

          reconsider xMR = x, yMR = y as Element of MR by A10, A11, A2;

          reconsider xsS = x, ysS = y as Element of sS by A10, A11, A3;

          xsS <= ysS by A9, A12, ORDERS_2:def 5;

          then xMR <= yMR by YELLOW_0: 59;

          then z in iMR by A12, ORDERS_2:def 5;

          hence z in iR by A10, A11, A12, Th40;

        end;

      end;

      thus R = ( subrelstr S) by Def7, A3, A4;

    end;

    theorem :: MYCIELSK:46

    

     Th46: for n be Nat, R be irreflexive NatRelStr of n st 2 <= ( clique# R) holds ( clique# R) = ( clique# ( Mycielskian R))

    proof

      let n be Nat, R be irreflexive NatRelStr of n such that

       A1: 2 <= ( clique# R) and

       A2: ( clique# R) <> ( clique# ( Mycielskian R));

      set cR = the carrier of R;

      set iR = the InternalRel of R;

      set MR = ( Mycielskian R);

      set cMR = the carrier of MR;

      set iMR = the InternalRel of MR;

      set cnMR = ( clique# MR);

      

       A3: cR = n by Def7;

      

       A4: cR c= cMR by Th37;

      consider C be 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 ( Segm n) c= ( Segm ((2 * n) + 1)) by NAT_1: 39;

      then

      reconsider S = n as Subset of MR by Def7;

      

       A6: R = ( subrelstr S) by Th45;

      then C is Clique of MR by DILWORTH: 28;

      then ( card C) <= cnMR by DILWORTH:def 4;

      then

       A7: ( clique# R) < cnMR by A2, A5, XXREAL_0: 1;

      then 2 < cnMR by A1, XXREAL_0: 2;

      then

       A8: (2 + 1) <= cnMR by NAT_1: 13;

      consider D be finite Clique of MR such that

       A9: ( card D) = cnMR by DILWORTH:def 4;

      per cases ;

        suppose

         A10: D c= n;

        (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;

      end;

        suppose not D c= n;

        then

        consider x be object such that

         A11: x in D and

         A12: not x in ( Segm n);

        x in cMR by A11;

        then

         A13: x in ( Segm ((2 * n) + 1)) by Def7;

        reconsider x as Nat by A13;

        reconsider xp1 = x as Element of MR 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 be set st y in D & x <> y holds y in ( Segm n)

        proof

          let y be set such that

           A17: y in D and

           A18: x <> y and

           A19: not y in ( Segm n);

          y in cMR by A17;

          then

           A20: y in ( Segm ((2 * n) + 1)) by Def7;

          reconsider y as Nat by A20;

          reconsider yp1 = y as Element of MR 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 DD) = (( card D) - ( card {x, y})) by CARD_2: 44;

          ((1 + 2) - 2) <= (( card D) - 2) by A8, A9, XREAL_1: 9;

          then 1 <= ( card DD) by A23, A18, CARD_2: 57;

          then

          consider z be object such that

           A24: z in DD by CARD_1: 27, XBOOLE_0:def 1;

          

           A25: z in D by A24, XBOOLE_0:def 5;

          

           A26: z in cMR by A24;

          reconsider zp1 = z as Element of MR by A24;

          

           A27: z in ( Segm ((2 * n) + 1)) by A26, Def7;

          reconsider z as Nat by A27;

          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;

          per cases by A15, A22, XXREAL_0: 1;

            suppose

             A30: x < (2 * n) & y < (2 * n);

            xp1 <= yp1 or yp1 <= xp1 by A11, A17, A18, DILWORTH: 6;

            then [x, y] in iMR or [y, x] in iMR by ORDERS_2:def 5;

            hence contradiction by A14, A30, A21, Th38;

          end;

            suppose

             A31: x < (2 * n) & y = (2 * n);

            xp1 <= zp1 or zp1 <= xp1 by A28, A25, A11, DILWORTH: 6;

            then

             A32: [x, z] in iMR or [z, x] in iMR by ORDERS_2:def 5;

            yp1 <= zp1 or zp1 <= yp1 by A29, A25, A17, DILWORTH: 6;

            then [y, z] in iMR or [z, y] in iMR by ORDERS_2:def 5;

            then n <= z & z < (2 * n) by A31, A21, Th38;

            hence contradiction by A32, A31, A14, Th38;

          end;

            suppose

             A33: x = (2 * n) & y < (2 * n);

            yp1 <= zp1 or zp1 <= yp1 by A29, A25, A17, DILWORTH: 6;

            then

             A34: [y, z] in iMR or [z, y] in iMR by ORDERS_2:def 5;

            xp1 <= zp1 or zp1 <= xp1 by A28, A25, A11, DILWORTH: 6;

            then [x, z] in iMR or [z, x] in iMR by ORDERS_2:def 5;

            then n <= z & z < (2 * n) by A33, A14, Th38;

            hence contradiction by A34, A33, A21, Th38;

          end;

            suppose x = (2 * n) & y = (2 * n);

            hence contradiction by A18;

          end;

        end;

        

         A35: ( card (D \ {x})) = (( card D) - ( card {x})) by A11, EULER_1: 4

        .= (( card D) - 1) by CARD_1: 30;

        per cases by A15, XXREAL_0: 1;

          suppose

           A36: x < (2 * n);

          consider xx be 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 ( Segm n) by NAT_1: 44;

          reconsider xxp1 = xx as Element of MR by A39, A4, A3;

           A40:

          now

            assume xx in D;

            then xp1 <= xxp1 or xxp1 <= xp1 by A11, A38, A14, DILWORTH: 6;

            then [x, xx] in iMR or [xx, x] in iMR by ORDERS_2:def 5;

            then [xx, xx] in iR or [xx, xx] in iR by A39, A37, Th42, Th43;

            hence contradiction by A39, A3, NECKLACE:def 5;

          end;

          set DD = ((D \ {x}) \/ {xx});

          DD c= cR

          proof

            let a be object;

            assume a in DD;

            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 cR by A38, A16, A3, NAT_1: 44;

          end;

          then

          reconsider DD as Subset of R;

          now

            let a,b be Element of R such that

             A41: a in DD and

             A42: b in DD and

             A43: a <> b;

            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 cR & b in cR by A41;

            then a in ( Segm n) & b in ( Segm n) by A3;

            then

            reconsider an = a, bn = b as Nat;

            reconsider ap1 = a, bp1 = b as Element of MR by A46, A4;

            per cases by A43, A44, A45, TARSKI:def 1;

              suppose

               A47: a in D & a <> x & b in D & b <> x;

              ap1 <= bp1 or bp1 <= ap1 by A47, A43, DILWORTH: 6;

              hence a <= b or b <= a by A6, A41, YELLOW_0: 60;

            end;

              suppose

               A48: a in D & a <> x & b = xx;

              ap1 <= xp1 or xp1 <= ap1 by A48, A11, DILWORTH: 6;

              then [ap1, x] in iMR or [x, ap1] in iMR by ORDERS_2:def 5;

              then [an, xx] in iR or [xx, an] in iR by A3, A37, Th42, Th43, A39;

              hence a <= b or b <= a by A48, ORDERS_2:def 5;

            end;

              suppose

               A49: a = xx & b in D & b <> x;

              bp1 <= xp1 or xp1 <= bp1 by A49, A11, DILWORTH: 6;

              then [bp1, x] in iMR or [x, bp1] in iMR by ORDERS_2:def 5;

              then [bn, xx] in iR or [xx, bn] in iR by A3, A37, Th42, Th43, A39;

              hence a <= b or b <= a by A49, ORDERS_2:def 5;

            end;

          end;

          then

          reconsider 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;

        end;

          suppose

           A51: x = (2 * n);

          ((2 + 1) - 1) <= (( card D) - 1) by A9, A8, XREAL_1: 9;

          then ( Segm 2) c= ( Segm ( card (D \ {x}))) by A35, NAT_1: 39;

          then

          consider y,z be object 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 MR by A52;

          then y in ( Segm ((2 * n) + 1)) by Def7;

          then

          reconsider y as Nat;

          reconsider yp1 = y as Element of MR by A52;

          yp1 <= xp1 or xp1 <= yp1 by A54, A53, A11, DILWORTH: 6;

          then

           A55: [y, x] in iMR or [x, y] in iMR by ORDERS_2:def 5;

          y in ( Segm 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;

        end;

      end;

    end;

    theorem :: MYCIELSK:47

    

     Th47: for R be with_finite_chromatic# RelStr, S be Subset of R holds ( chromatic# R) >= ( chromatic# ( subrelstr S))

    proof

      let R be with_finite_chromatic# RelStr, S be Subset of R;

      consider C be 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;

    end;

    theorem :: MYCIELSK:48

    

     Th48: for n be Nat, R be irreflexive NatRelStr of n holds ( chromatic# ( Mycielskian R)) = (1 + ( chromatic# R))

    proof

      let n be Nat, R be irreflexive NatRelStr of n;

      set cR = the carrier of R, iR = the InternalRel of R;

      set cnR = ( chromatic# R);

      set MR = ( Mycielskian R);

      set cnMR = ( chromatic# MR);

      set cMR = the carrier of MR, iMR = the InternalRel of MR;

      

       A1: cR = ( Segm n) by Def7;

      

       A2: ex C be finite Coloring of MR st ( card C) = (1 + cnR)

      proof

        consider C be finite Coloring of R such that

         A3: ( card C) = cnR by Def3;

        defpred P[ object, object] means ex D1 be set st D1 = $1 & $2 = { (m + n) where m be Element of NAT : m in D1 };

        

         A4: for e be object st e in C holds ex u be object st P[e, u]

        proof

          let e be object such that e in C;

          reconsider ee = e as set by TARSKI: 1;

          take u = { (m + n) where m be Element of NAT : m in ee };

          thus thesis;

        end;

        consider r be Function such that ( dom r) = C and

         A5: for e be object st e in C holds P[e, (r . e)] from CLASSES1:sch 1( A4);

        set D = { (d \/ (r . d)) where d be Element of C : d in C };

        

         A6: ( card D) = ( card C)

        proof

          per cases ;

            suppose

             A7: D is empty;

            now

              assume C is non empty;

              then

              consider c be object such that

               A8: c in C;

              reconsider c as set by TARSKI: 1;

              (c \/ (r . c)) in D by A8;

              hence contradiction by A7;

            end;

            hence thesis by A7;

          end;

            suppose

             A9: D is non empty;

            defpred R[ object, object] means ex D1 be set st D1 = $1 & $2 = (D1 \/ (r . $1));

            

             A10: for e be object st e in C holds ex u be object st R[e, u]

            proof

              let e be object such that e in C;

              reconsider ee = e as set by TARSKI: 1;

              take u = (ee \/ (r . e));

              thus thesis;

            end;

            consider s be Function such that

             A11: ( dom s) = C and

             A12: for e be object st e in C holds R[e, (s . e)] from CLASSES1:sch 1( A10);

            

             A13: ( rng s) c= D

            proof

              let y be object;

              assume y in ( rng s);

              then

              consider x be object such that

               A14: x in ( dom s) and

               A15: y = (s . x) by FUNCT_1:def 3;

              reconsider x as set by TARSKI: 1;

               R[x, (s . x)] by A14, A11, A12;

              then y = (x \/ (r . x)) by A15;

              hence y in D by A14, A11;

            end;

            then

            reconsider s as Function of C, D by A11, FUNCT_2: 2;

            D c= ( rng s)

            proof

              let x be object;

              assume x in D;

              then

              consider c be Element of C such that

               A16: x = (c \/ (r . c)) and

               A17: c in C;

               R[c, (s . c)] by A17, A12;

              then x = (s . c) by A16;

              hence x in ( rng s) by A17, A11, FUNCT_1:def 3;

            end;

            then ( rng s) = D by A13;

            then

             A18: s is onto by FUNCT_2:def 3;

            s is one-to-one

            proof

              let x1,x2 be object such that

               A19: x1 in ( dom s) and

               A20: x2 in ( dom s) and

               A21: (s . x1) = (s . x2);

              reconsider x1, x2 as set by TARSKI: 1;

               R[x1, (s . x1)] by A19, A12;

              then

               A22: (s . x1) = (x1 \/ (r . x1));

               R[x2, (s . x2)] by A20, A12;

              then

               A23: (s . x2) = (x2 \/ (r . x2));

              

               A24: x1 c= x2

              proof

                let x be object;

                assume

                 A25: x in x1;

                

                 A26: x in (s . x1) by A22, A25, XBOOLE_0:def 3;

                per cases by A26, A21, A23, XBOOLE_0:def 3;

                  suppose x in x2;

                  hence thesis;

                end;

                  suppose

                   A27: x in (r . x2);

                   P[x2, (r . x2)] by A5, A20;

                  then x in { (m + n) where m be Element of NAT : m in x2 } by A27;

                  then

                  consider m be Element of NAT such that

                   A28: x = (m + n) and m in x2;

                  (m + n) in ( Segm ( 0 + n)) by A25, A28, A19, A11, A1;

                  then (m + n) < ( 0 + n) by NAT_1: 44;

                  hence thesis by XREAL_1: 6;

                end;

              end;

              x2 c= x1

              proof

                let x be object;

                assume

                 A29: x in x2;

                

                 A30: x in (s . x2) by A23, A29, XBOOLE_0:def 3;

                per cases by A30, A21, A22, XBOOLE_0:def 3;

                  suppose x in x1;

                  hence thesis;

                end;

                  suppose

                   A31: x in (r . x1);

                   P[x1, (r . x1)] by A5, A19;

                  then x in { (m + n) where m be Element of NAT : m in x1 } by A31;

                  then

                  consider m be Element of NAT such that

                   A32: x = (m + n) and m in x1;

                  (m + n) in ( Segm ( 0 + n)) by A29, A32, A20, A11, A1;

                  then (m + n) < ( 0 + n) by NAT_1: 44;

                  hence thesis by XREAL_1: 6;

                end;

              end;

              hence thesis by A24, XBOOLE_0:def 10;

            end;

            hence thesis by A18, A9, EULER_1: 11;

          end;

        end;

        then

         A33: D is finite;

        set E = (D \/ { {(2 * n)}});

        

         A34: ( union E) c= cMR

        proof

          let x be object;

          assume x in ( union E);

          then

          consider Y be set such that

           A35: x in Y and

           A36: Y in E by TARSKI:def 4;

          per cases by A36, XBOOLE_0:def 3;

            suppose Y in D;

            then

            consider d be Element of C such that

             A37: Y = (d \/ (r . d)) and

             A38: d in C;

             P[d, (r . d)] by A38, A5;

            then

             A39: (r . d) = { (m + n) where m be Element of NAT : m in d };

            per cases by A35, A37, XBOOLE_0:def 3;

              suppose

               A40: x in d;

              then x in ( Segm n) by A38, A1;

              then

              reconsider a = x as Nat;

              a in ( Segm n) by A40, A38, A1;

              then a < n by NAT_1: 44;

              then (a + 0 ) < (n + n) by XREAL_1: 8;

              then a < ((2 * n) + 1) by NAT_1: 13;

              then a in ( Segm ((2 * n) + 1)) by NAT_1: 44;

              hence x in cMR by Def7;

            end;

              suppose x in (r . d);

              then

              consider m be Element of NAT such that

               A41: x = (m + n) and

               A42: m in d by A39;

              m in ( Segm n) by A42, A38, A1;

              then m < n by 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 ( Segm ((2 * n) + 1)) by A41, NAT_1: 44;

              hence x in cMR by Def7;

            end;

          end;

            suppose Y in { {(2 * n)}};

            then Y = {(2 * n)} by TARSKI:def 1;

            then

             A43: x = (2 * n) by A35, TARSKI:def 1;

            (2 * n) < ((2 * n) + 1) by NAT_1: 13;

            then (2 * n) in ( Segm ((2 * n) + 1)) by NAT_1: 44;

            hence x in cMR by A43, Def7;

          end;

        end;

        

         A44: E c= ( bool cMR)

        proof

          let X be object;

          reconsider XX = X as set by TARSKI: 1;

          assume

           A45: X in E;

          XX c= cMR

          proof

            let x be object;

            assume x in XX;

            then x in ( union E) by A45, TARSKI:def 4;

            hence x in cMR by A34;

          end;

          hence X in ( bool cMR);

        end;

        

         A46: ( union E) = cMR

        proof

          thus ( union E) c= cMR by A34;

          thus cMR c= ( union E)

          proof

            let x be object;

            assume x in cMR;

            then

             A47: x in ( Segm ((2 * n) + 1)) by Def7;

            then

            reconsider a = x as Nat;

            a < ((2 * n) + 1) by A47, NAT_1: 44;

            then

             A48: a <= (2 * n) by NAT_1: 13;

            per cases ;

              suppose a < n;

              then a in ( Segm n) by NAT_1: 44;

              then a in ( union C) by A1, EQREL_1:def 4;

              then

              consider c be set such that

               A49: a in c and

               A50: c in C by TARSKI:def 4;

              

               A51: x in (c \/ (r . c)) by A49, XBOOLE_0:def 3;

              (c \/ (r . c)) in D by A50;

              then (c \/ (r . c)) in E by XBOOLE_0:def 3;

              hence x in ( union E) by A51, TARSKI:def 4;

            end;

              suppose

               A52: a >= n;

              per cases by A48, XXREAL_0: 1;

                suppose

                 A53: a < (n + n);

                consider b be Nat such that

                 A54: a = (n + b) by A52, NAT_1: 10;

                reconsider b as Element of NAT by ORDINAL1:def 12;

                b < n by A54, A53, XREAL_1: 6;

                then b in ( Segm n) by NAT_1: 44;

                then b in ( union C) by EQREL_1:def 4, A1;

                then

                consider c be set such that

                 A55: b in c and

                 A56: c in C by TARSKI:def 4;

                 P[c, (r . c)] by A56, A5;

                then (r . c) = { (m + n) where m be Element of NAT : m in c };

                then a in (r . c) by A55, A54;

                then

                 A57: x in (c \/ (r . c)) by XBOOLE_0:def 3;

                (c \/ (r . c)) in D by A56;

                then (c \/ (r . c)) in E by XBOOLE_0:def 3;

                hence x in ( union E) by A57, TARSKI:def 4;

              end;

                suppose a = (2 * n);

                then

                 A58: a in {(2 * n)} by TARSKI:def 1;

                 {(2 * n)} in { {(2 * n)}} by TARSKI:def 1;

                then {(2 * n)} in E by XBOOLE_0:def 3;

                hence x in ( union E) by A58, TARSKI:def 4;

              end;

            end;

          end;

        end;

        now

          let A be Subset of cMR such that

           A59: A in E;

          thus A <> {}

          proof

            per cases by A59, XBOOLE_0:def 3;

              suppose A in D;

              then

              consider d be Element of C such that

               A60: A = (d \/ (r . d)) and

               A61: d in C;

              d <> {} by A61;

              hence thesis by A60;

            end;

              suppose A in { {(2 * n)}};

              hence thesis by TARSKI:def 1;

            end;

          end;

          let B be Subset of cMR such that

           A62: B in E;

          assume

           A63: A <> B;

          assume A meets B;

          then

          consider x be object such that

           A64: x in A and

           A65: x in B by XBOOLE_0: 3;

          per cases by A59, A62, XBOOLE_0:def 3;

            suppose that

             A66: A in D and

             A67: B in D;

            consider d be Element of C such that

             A68: A = (d \/ (r . d)) and

             A69: d in C by A66;

            consider e be Element of C such that

             A70: B = (e \/ (r . e)) and

             A71: e in C by A67;

            per cases by A68, A70, A64, A65, XBOOLE_0:def 3;

              suppose x in d & x in e;

              then d meets e by XBOOLE_0: 3;

              then d = e by A69, A71, EQREL_1:def 4;

              hence contradiction by A68, A70, A63;

            end;

              suppose that

               A72: x in d and

               A73: x in (r . e);

               P[e, (r . e)] by A71, A5;

              then x in { (m + n) where m be Element of NAT : m in e } by A73;

              then

              consider mb be Element of NAT such that

               A74: x = (mb + n) and mb in e;

              (mb + n) in ( Segm (n + 0 )) by A74, A72, A69, A1;

              then (mb + n) < (n + 0 ) by NAT_1: 44;

              hence contradiction by XREAL_1: 6;

            end;

              suppose that

               A75: x in (r . d) and

               A76: x in e;

               P[d, (r . d)] by A69, A5;

              then x in { (m + n) where m be Element of NAT : m in d } by A75;

              then

              consider ma be Element of NAT such that

               A77: x = (ma + n) and ma in d;

              (ma + n) in ( Segm (n + 0 )) by A77, A76, A71, A1;

              then (ma + n) < (n + 0 ) by NAT_1: 44;

              hence contradiction by XREAL_1: 6;

            end;

              suppose that

               A78: x in (r . d) and

               A79: x in (r . e);

               P[d, (r . d)] by A69, A5;

              then x in { (m + n) where m be Element of NAT : m in d } by A78;

              then

              consider ma be Element of NAT such that

               A80: x = (ma + n) and

               A81: ma in d;

               P[e, (r . e)] by A71, A5;

              then x in { (m + n) where m be Element of NAT : m in e } by A79;

              then

              consider mb be Element of NAT such that

               A82: x = (mb + n) and

               A83: mb in e;

              d meets e by A80, A82, A81, A83, XBOOLE_0: 3;

              then d = e by A69, A71, EQREL_1:def 4;

              hence contradiction by A68, A70, A63;

            end;

          end;

            suppose that

             A84: A in D and

             A85: B in { {(2 * n)}};

            B = {(2 * n)} by A85, TARSKI:def 1;

            then

             A86: x = (2 * n) by A65, TARSKI:def 1;

            consider d be Element of C such that

             A87: A = (d \/ (r . d)) and

             A88: d in C by A84;

            per cases by A87, A64, XBOOLE_0:def 3;

              suppose x in d;

              then (n + n) in ( Segm n) by A88, A1, A86;

              then (n + n) < n by NAT_1: 44;

              hence contradiction by NAT_1: 11;

            end;

              suppose

               A89: x in (r . d);

               P[d, (r . d)] by A88, A5;

              then x in { (m + n) where m be Element of NAT : m in d } by A89;

              then

              consider m be Element of NAT such that

               A90: x = (m + n) and

               A91: m in d;

              m in n by A91, A88, A1;

              hence contradiction by A90, A86;

            end;

          end;

            suppose that

             A92: A in { {(2 * n)}} and

             A93: B in D;

            A = {(2 * n)} by A92, TARSKI:def 1;

            then

             A94: x = (2 * n) by A64, TARSKI:def 1;

            consider d be Element of C such that

             A95: B = (d \/ (r . d)) and

             A96: d in C by A93;

            per cases by A95, A65, XBOOLE_0:def 3;

              suppose x in d;

              then (n + n) in ( Segm n) by A96, A1, A94;

              then (n + n) < n by NAT_1: 44;

              hence contradiction by NAT_1: 11;

            end;

              suppose

               A97: x in (r . d);

               P[d, (r . d)] by A96, A5;

              then x in { (m + n) where m be Element of NAT : m in d } by A97;

              then

              consider m be Element of NAT such that

               A98: x = (m + n) and

               A99: m in d;

              m in n by A99, A96, A1;

              hence contradiction by A98, A94;

            end;

          end;

            suppose A in { {(2 * n)}} & B in { {(2 * n)}};

            then A = {(2 * n)} & B = {(2 * n)} by TARSKI:def 1;

            hence contradiction by A63;

          end;

        end;

        then

        reconsider E as a_partition of cMR by A44, A46, EQREL_1:def 4;

        now

          let x be set;

          assume

           A100: x in E;

          per cases by A100, XBOOLE_0:def 3;

            suppose x in D;

            then

            consider d be Element of C such that

             A101: x = (d \/ (r . d)) and

             A102: d in C;

            reconsider d as Subset of R by A102;

             P[d, (r . d)] by A102, A5;

            then

             A103: (r . d) = { (m + n) where m be Element of NAT : m in d };

            

             A104: x c= cMR

            proof

              let a be object;

              assume

               A105: a in x;

              per cases by A101, A105, XBOOLE_0:def 3;

                suppose

                 A106: a in d;

                then a in ( Segm n) by A1;

                then

                reconsider ap1 = a as Nat;

                ap1 in ( Segm n) by A106, A1;

                then

                 A107: ap1 < n by NAT_1: 44;

                n <= (n + n) by NAT_1: 12;

                then ap1 < (n + n) by A107, XXREAL_0: 2;

                then ap1 < ((2 * n) + 1) by NAT_1: 13;

                then a in ( Segm ((2 * n) + 1)) by NAT_1: 44;

                hence a in cMR by Def7;

              end;

                suppose a in (r . d);

                then

                consider am be Element of NAT such that

                 A108: a = (am + n) and

                 A109: am in d by A103;

                am in ( Segm n) by A109, A1;

                then am < n by 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 ( Segm ((2 * n) + 1)) by A108, NAT_1: 44;

                hence a in cMR by Def7;

              end;

            end;

             A110:

            now

              let x be Nat;

              assume x in (r . d);

              then

              consider m be Element of NAT such that

               A111: x = (m + n) and

               A112: m in d by A103;

              thus n <= x by A111, NAT_1: 11;

              m in ( Segm n) by A112, A1;

              then m < n by NAT_1: 44;

              then (m + n) < (n + n) by XREAL_1: 6;

              hence x < (2 * n) by A111;

            end;

            

             A113: d is stable by DILWORTH:def 12;

            now

              let a,b be Element of MR such that

               A114: a in x and

               A115: b in x and

               A116: a <> b and

               A117: a <= b or b <= a;

              

               A118: [a, b] in iMR or [b, a] in iMR by A117, ORDERS_2:def 5;

              per cases by A114, A115, A101, XBOOLE_0:def 3;

                suppose

                 A119: a in d & b in d;

                then

                 A120: [a, b] in iR or [b, a] in iR by A1, A118, Th40;

                reconsider a, b as Element of R by A119;

                a <= b or b <= a by A120, ORDERS_2:def 5;

                hence contradiction by A119, A116, A113;

              end;

                suppose that

                 A121: a in d and

                 A122: b in (r . d);

                consider bm be Element of NAT such that

                 A123: b = (bm + n) and

                 A124: bm in d by A122, A103;

                a in ( Segm n) by A121, A1;

                then

                reconsider ap1 = a as Nat;

                

                 A125: [ap1, bm] in iR or [bm, ap1] in iR by A118, Th42, Th43, A123, A121, A1;

                reconsider bmp1 = bm, a as Element of R by A124, A121;

                

                 A126: bmp1 <= a or a <= bmp1 by A125, ORDERS_2:def 5;

                bmp1 <> a by A125, A121, NECKLACE:def 5;

                hence contradiction by A126, A124, A121, A113;

              end;

                suppose that

                 A127: a in (r . d) and

                 A128: b in d;

                consider am be Element of NAT such that

                 A129: a = (am + n) and

                 A130: am in d by A127, A103;

                b in ( Segm n) by A128, A1;

                then

                reconsider bp1 = b as Nat;

                

                 A131: [am, bp1] in iR or [bp1, am] in iR by A118, Th42, Th43, A129, A128, A1;

                reconsider amp1 = am, b as Element of R by A130, A128;

                

                 A132: amp1 <= b or b <= amp1 by A131, ORDERS_2:def 5;

                amp1 <> b by A131, A128, NECKLACE:def 5;

                hence contradiction by A132, A130, A128, A113;

              end;

                suppose that

                 A133: a in (r . d) and

                 A134: b in (r . d);

                consider am be Element of NAT such that

                 A135: a = (am + n) and am in d by A133, A103;

                consider bm be Element of NAT such that

                 A136: b = (bm + n) and bm in d by A134, A103;

                n <= (am + n) & (am + n) < (2 * n) & n <= (bm + n) & (bm + n) < (2 * n) by A133, A134, A135, A136, A110;

                hence contradiction by A135, A136, A118, Th38;

              end;

            end;

            hence x is StableSet of MR by A104, DILWORTH:def 2;

          end;

            suppose x in { {(2 * n)}};

            then

             A137: x = {(2 * n)} by TARSKI:def 1;

            (2 * n) < ((2 * n) + 1) by NAT_1: 13;

            then (2 * n) in ( Segm ((2 * n) + 1)) by NAT_1: 44;

            then

             A138: (2 * n) in cMR by Def7;

            x is Subset of MR by A137, A138, SUBSET_1: 33;

            hence x is StableSet of MR by A137;

          end;

        end;

        then

        reconsider E as Coloring of MR by DILWORTH:def 12;

        take E;

        now

          assume {(2 * n)} in D;

          then

          consider d be Element of C such that

           A139: {(2 * n)} = (d \/ (r . d)) and

           A140: d in C;

          

           A141: (2 * n) in (d \/ (r . d)) by A139, TARSKI:def 1;

          per cases by A141, XBOOLE_0:def 3;

            suppose (2 * n) in d;

            then (2 * n) in cR by A140;

            then (2 * n) in ( Segm n) by Def7;

            then (n + n) < n by NAT_1: 44;

            hence contradiction by NAT_1: 11;

          end;

            suppose

             A142: (2 * n) in (r . d);

             P[d, (r . d)] by A140, A5;

            then (2 * n) in { (m + n) where m be Element of NAT : m in d } by A142;

            then

            consider m be Element of NAT such that

             A143: (2 * n) = (m + n) and

             A144: m in d;

            m in cR by A140, A144;

            then m in n by Def7;

            hence contradiction by A143;

          end;

        end;

        hence ( card E) = (1 + cnR) by A6, A33, A3, CARD_2: 41;

      end;

      for C be finite Coloring of MR holds (1 + cnR) <= ( card C)

      proof

        let E be finite Coloring of MR;

        assume (1 + cnR) > ( card E);

        then

         A145: cnR >= ( card E) by NAT_1: 13;

        

         A146: cnMR <= ( card E) by Def3;

        then

         A147: cnMR <= cnR by A145, XXREAL_0: 2;

        n <= (n + n) by NAT_1: 11;

        then n < ((2 * n) + 1) by NAT_1: 13;

        then ( Segm n) c= ( Segm ((2 * n) + 1)) by NAT_1: 39;

        then

        reconsider S = n as Subset of MR by Def7;

        

         A148: R = ( subrelstr S) by Th45;

        then cnR <= cnMR by Th47;

        then cnR = cnMR by A147, XXREAL_0: 1;

        then

         A149: ( card E) = cnR by A145, A146, XXREAL_0: 1;

        reconsider C = (E | S) as Coloring of R by A148, Th10;

        

         A150: ( card C) >= cnR by Def3;

        

         A151: ( card C) <= ( card E) by Th8;

        then

         A152: ( card C) = cnR by A149, A150, XXREAL_0: 1;

        (2 * n) < ((2 * n) + 1) by NAT_1: 13;

        then (2 * n) in ( Segm ((2 * n) + 1)) by NAT_1: 44;

        then (2 * n) in cMR by Def7;

        then (2 * n) in ( union E) by EQREL_1:def 4;

        then

        consider e be set such that

         A153: (2 * n) in e and

         A154: e in E by TARSKI:def 4;

        reconsider e as Subset of MR by A154;

        reconsider n2 = (2 * n) as Element of MR by A153, A154;

        set se = (e /\ S);

        e meets S by A149, A152, A154, Th9;

        then

         A155: se in C by A154;

        then

        consider mp1 be Element of R such that

         A156: mp1 in se and

         A157: for d be Element of C st d <> se holds ex w be Element of R st w in ( Adjacent mp1) & w in d by A151, A149, A150, Th31, XXREAL_0: 1;

        mp1 in ( Segm n) by A156, A155;

        then

        reconsider m = mp1 as Nat;

        set mn = (m + n);

        

         A158: ( 0 + n) <= mn by XREAL_1: 6;

        m in ( Segm n) by A156, A155;

        then m < n by NAT_1: 44;

        then

         A159: mn < (n + n) by XREAL_1: 6;

        then mn < ((2 * n) + 1) by NAT_1: 13;

        then

         A160: mn in ( Segm ((2 * n) + 1)) by NAT_1: 44;

        then mn in cMR by Def7;

        then mn in ( union E) by EQREL_1:def 4;

        then

        consider f be set such that

         A161: mn in f and

         A162: f in E by TARSKI:def 4;

        reconsider f as Subset of MR by A162;

        reconsider mnp1 = mn as Element of MR by A160, Def7;

         A163:

        now

          assume

           A164: e <> f;

          set sf = (f /\ S);

          f meets S by A149, A152, A162, Th9;

          then

           A165: sf in C by A162;

          

           A166: sf c= f by XBOOLE_1: 17;

          now

            assume

             A167: sf = se;

            sf <> {} by A165;

            then

            consider x be object such that

             A168: x in sf by XBOOLE_0:def 1;

            se c= e by XBOOLE_1: 17;

            then e meets f by A167, A168, A166, XBOOLE_0: 3;

            hence contradiction by A164, A162, A154, EQREL_1:def 4;

          end;

          then

          consider wp1 be Element of R such that

           A169: wp1 in ( Adjacent mp1) and

           A170: wp1 in sf by A165, A157;

          wp1 in ( Segm n) by A170, A165;

          then

          reconsider w = wp1 as Nat;

          w in ( Segm n) by A170, A165;

          then

           A171: w < n by NAT_1: 44;

          mp1 < wp1 or wp1 < mp1 by A169, Def6;

          then mp1 <= wp1 or wp1 <= mp1 by ORDERS_2:def 6;

          then [m, w] in iR or [w, m] in iR by ORDERS_2:def 5;

          then

           A172: [(m + n), w] in iMR or [w, (m + n)] in iMR by Th41;

          reconsider wp2 = wp1 as Element of MR by A170;

          f is stable by A162, DILWORTH:def 12;

          then not wp2 <= mnp1 & not mnp1 <= wp2 by A171, A158, A170, A166, A161;

          hence contradiction by A172, ORDERS_2:def 5;

        end;

        

         A173: [mn, (2 * n)] in iMR by A159, A158, Th44;

        e is stable by A154, DILWORTH:def 12;

        then not mnp1 <= n2 & not n2 <= mnp1 by A153, A161, A163, A159;

        hence contradiction by A173, ORDERS_2:def 5;

      end;

      hence ( chromatic# ( Mycielskian R)) = (1 + ( chromatic# R)) by A2, Def3;

    end;

     Lm1:

    now

      let myc1,myc2 be Function such that

       A1: ( dom myc1) = NAT and

       A2: (myc1 . 0 ) = ( CompleteRelStr 2) and

       A3: for k be Nat, R be 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 be Nat, R be NatRelStr of ((3 * (2 |^ k)) -' 1) st R = (myc2 . k) holds (myc2 . (k + 1)) = ( Mycielskian R);

      defpred P2[ 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: P2[ 0 ] by A2, A5;

      

       A8: for k be Nat st P2[k] holds P2[(k + 1)]

      proof

        let k be Nat such that

         A9: P2[k];

        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 P2[(k + 1)] by A10, A9, A6;

      end;

      for n be Nat holds P2[n] from NAT_1:sch 2( A7, A8);

      then for x be object st x in ( dom myc1) holds (myc1 . x) = (myc2 . x) by A1;

      hence myc1 = myc2 by A1, A4;

    end;

    definition

      let n be Nat;

      :: MYCIELSK:def10

      func Mycielskian n -> NatRelStr of ((3 * (2 |^ n)) -' 1) means

      : Def10: ex myc be Function st it = (myc . n) & ( dom myc) = NAT & (myc . 0 ) = ( CompleteRelStr 2) & for k be Nat, R be NatRelStr of ((3 * (2 |^ k)) -' 1) st R = (myc . k) holds (myc . (k + 1)) = ( Mycielskian R);

      existence

      proof

        defpred P[ Nat, object, object] means ($2 is NatRelStr of ((3 * (2 |^ $1)) -' 1) implies ex R be NatRelStr of ((3 * (2 |^ $1)) -' 1) st $2 = R & $3 = ( Mycielskian R)) & ( not $2 is NatRelStr of ((3 * (2 |^ $1)) -' 1) implies $3 = $2);

        

         A1: for n be Nat holds for x be set holds ex y be set st P[n, x, y]

        proof

          let n be Nat, x be set;

          per cases ;

            suppose x is NatRelStr of ((3 * (2 |^ n)) -' 1);

            then

            reconsider R = x as NatRelStr of ((3 * (2 |^ n)) -' 1);

            ( Mycielskian R) = ( Mycielskian R);

            then

            consider y be object such that

             A2: P[n, x, y];

            y is set by TARSKI: 1;

            hence thesis by A2;

          end;

            suppose not x is NatRelStr of ((3 * (2 |^ n)) -' 1);

            hence thesis;

          end;

        end;

        consider f be Function such that

         A3: ( dom f) = NAT and

         A4: (f . 0 ) = ( CompleteRelStr 2) and

         A5: for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 1( A1);

        defpred P2[ 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

         A6: P2[ 0 ] by A4;

        

         A7: for k be Nat st P2[k] holds P2[(k + 1)]

        proof

          let k be Nat such that

           A8: P2[k];

          consider R be NatRelStr of ((3 * (2 |^ k)) -' 1) such that (f . k) = R and

           A9: (f . (k + 1)) = ( Mycielskian R) by A8, A5;

          

           A10: (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

           A11: (3 * (2 |^ k)) >= 1 by A10, XXREAL_0: 2;

          then

           A12: ((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 A11, XXREAL_0: 2;

          then

           A13: ((3 * (2 |^ (k + 1))) - 1) >= (1 - 1) by XREAL_1: 9;

          ((2 * ((3 * (2 |^ k)) -' 1)) + 1) = ((2 * ((3 * (2 |^ k)) - 1)) + 1) by A12, 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 A13, XREAL_0:def 2;

          hence P2[(k + 1)] by A9;

        end;

        

         A14: for n be Nat holds P2[n] from NAT_1:sch 2( A6, A7);

        reconsider IT = (f . n) as NatRelStr of ((3 * (2 |^ n)) -' 1) by A14;

        take IT;

        take myc = f;

        thus IT = (myc . n);

        thus ( dom myc) = NAT by A3;

        thus (myc . 0 ) = ( CompleteRelStr 2) by A4;

        let k be Nat;

        let R be NatRelStr of ((3 * (2 |^ k)) -' 1);

        assume

         A15: R = (myc . k);

        then

        consider RR be NatRelStr of ((3 * (2 |^ k)) -' 1) such that

         A16: (f . k) = RR and

         A17: (f . (k + 1)) = ( Mycielskian RR) by A5;

        thus (myc . (k + 1)) = ( Mycielskian R) by A17, A15, A16;

      end;

      uniqueness by Lm1;

    end

    theorem :: MYCIELSK:49

    

     Th49: ( Mycielskian 0 ) = ( CompleteRelStr 2) & for k be Nat holds ( Mycielskian (k + 1)) = ( Mycielskian ( Mycielskian k))

    proof

      consider myc be Function such that

       A1: ( Mycielskian 0 ) = (myc . 0 ) and ( dom myc) = NAT and

       A2: (myc . 0 ) = ( CompleteRelStr 2) and for k be Nat, R be 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;

      let k be Nat;

      consider myc1 be Function such that

       A3: ( Mycielskian k) = (myc1 . k) and

       A4: ( dom myc1) = NAT & (myc1 . 0 ) = ( CompleteRelStr 2) & for k be Nat, R be NatRelStr of ((3 * (2 |^ k)) -' 1) st R = (myc1 . k) holds (myc1 . (k + 1)) = ( Mycielskian R) by Def10;

      consider myc2 be Function such that

       A5: ( Mycielskian (k + 1)) = (myc2 . (k + 1)) and

       A6: ( dom myc2) = NAT & (myc2 . 0 ) = ( CompleteRelStr 2) and

       A7: for k be Nat, R be 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 thesis by A3, A7, A5;

    end;

    registration

      let n be Nat;

      cluster ( Mycielskian n) -> irreflexive;

      coherence

      proof

        defpred P[ Nat] means ( Mycielskian $1) is irreflexive;

        

         A1: P[ 0 ] by Th49;

        

         A2: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          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: P[n];

          assume not P[(n + 1)];

          then

          consider x be set such that

           A4: x in cMRn1 and

           A5: [x, x] in iMRn1 by NECKLACE:def 5;

          

           A6: ( Mycielskian (n + 1)) = ( Mycielskian ( Mycielskian n)) by Th49;

          set N = ((3 * (2 |^ n)) -' 1);

          

           A7: cMRn1 = ((2 * N) + 1) by A6, Def7;

          

           A8: cMRn = N by Def7;

          x in ( Segm ((2 * N) + 1)) by A7, A4;

          then

          reconsider x as Nat;

          x < N & x < N or x < N & N <= x & x < (2 * N) or N <= x & x < (2 * N) & x < N or x = (2 * N) & N <= x & x < (2 * N) or N <= x & x < (2 * N) & x = (2 * N) by A6, A5, Th38;

          then

           A9: x in ( Segm N) by NAT_1: 44;

          then [x, x] in iMRn by A5, A6, Th40;

          hence contradiction by A3, A8, A9, NECKLACE:def 5;

        end;

        for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

        hence thesis;

      end;

    end

    registration

      let n be Nat;

      cluster ( Mycielskian n) -> symmetric;

      coherence

      proof

        defpred P[ Nat] means ( Mycielskian $1) is symmetric;

        

         A1: P[ 0 ] by Th49;

        

         A2: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          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: P[n];

          

           A4: ( Mycielskian (n + 1)) = ( Mycielskian ( Mycielskian n)) by Th49;

          set N = ((3 * (2 |^ n)) -' 1);

          

           A5: cMRn1 = ((2 * N) + 1) by A4, Def7;

          

           A6: cMRn = N by Def7;

          let x,y be object such that

           A7: x in cMRn1 and

           A8: y in cMRn1 and

           A9: [x, y] in iMRn1;

          x in ( Segm ((2 * N) + 1)) & y in ( Segm ((2 * N) + 1)) by A5, A7, A8;

          then

          reconsider xp1 = x, yp1 = y as Nat;

          

           A10: [xp1, yp1] in iMRn1 by A9;

          per cases by A10, A4, Th38;

            suppose xp1 < N & yp1 < N;

            then xp1 in ( Segm N) & yp1 in ( Segm N) by NAT_1: 44;

            then

             A11: [yp1, xp1] in iMRn by A3, A6, Th5, A9, A4, Th40;

            iMRn c= iMRn1 by A4, Th39;

            hence [y, x] in iMRn1 by A11;

          end;

            suppose that

             A12: xp1 < N and

             A13: N <= yp1 and

             A14: yp1 < (2 * N);

            consider yy be Nat such that

             A15: yp1 = (N + yy) by A13, NAT_1: 10;

            

             A16: xp1 in ( Segm N) by A12, NAT_1: 44;

            (yy + N) < (N + N) by A14, A15;

            then yy < N by XREAL_1: 6;

            then

             A17: yy in ( Segm N) by NAT_1: 44;

             [x, yy] in iMRn by A9, A16, A15, A4, Th42;

            then [yy, x] in iMRn by A17, A16, A6, A3, Th5;

            hence [y, x] in iMRn1 by A4, A10, A15, Th41;

          end;

            suppose that

             A18: N <= xp1 and

             A19: xp1 < (2 * N) and

             A20: yp1 < N;

            consider xx be Nat such that

             A21: xp1 = (N + xx) by A18, NAT_1: 10;

            

             A22: yp1 in ( Segm N) by A20, NAT_1: 44;

            (xx + N) < (N + N) by A21, A19;

            then xx < N by XREAL_1: 6;

            then

             A23: xx in ( Segm N) by NAT_1: 44;

             [xx, y] in iMRn by A22, A9, A4, A21, Th43;

            then [y, xx] in iMRn by A23, A22, A6, A3, Th5;

            hence [y, x] in iMRn1 by A4, A10, A21, Th41;

          end;

            suppose xp1 = (2 * N) & N <= yp1 & yp1 < (2 * N);

            hence [y, x] in iMRn1 by A4, Th44;

          end;

            suppose N <= xp1 & xp1 < (2 * N) & yp1 = (2 * N);

            hence [y, x] in iMRn1 by A4, Th44;

          end;

        end;

        for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

        hence thesis;

      end;

    end

    theorem :: MYCIELSK:50

    

     Th50: for n be Nat holds ( clique# ( Mycielskian n)) = 2 & ( chromatic# ( Mycielskian n)) = (n + 2)

    proof

      defpred P[ 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: P[ 0 ] by A1;

      

       A3: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A4: ( clique# ( Mycielskian n)) = 2 and

         A5: ( chromatic# ( Mycielskian n)) = (n + 2);

        

         A6: ( Mycielskian (n + 1)) = ( Mycielskian ( Mycielskian n)) by Th49;

        thus ( clique# ( Mycielskian (n + 1))) = 2 by A4, A6, Th46;

        

        thus ( chromatic# ( Mycielskian (n + 1))) = (1 + ( chromatic# ( Mycielskian n))) by A6, Th48

        .= ((n + 1) + 2) by A5;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A2, A3);

      hence thesis;

    end;

    theorem :: MYCIELSK:51

    for n be Nat holds ex R be finite RelStr st ( clique# R) = 2 & ( chromatic# R) > n

    proof

      let n be Nat;

      take ( Mycielskian n);

      ((n + 1) + 1) > (n + 1) & (n + 1) > n by NAT_1: 13;

      then (n + 2) > n by XXREAL_0: 2;

      hence thesis by Th50;

    end;

    theorem :: MYCIELSK:52

    for n be Nat holds ex R be finite RelStr st ( stability# R) = 2 & ( cliquecover# R) > n

    proof

      let n be Nat;

      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# R) = 2 & ( chromatic# R) > n by Th50;

      take S = ( ComplRelStr R);

      thus ( stability# S) = 2 by A1, Th23;

      thus ( cliquecover# S) > n by A1, Th29;

    end;