dilworth.miz



    begin

    scheme :: DILWORTH:sch1

    FraenkelFinCard1 { A() -> finite non empty set , P[ set], Y() -> finite set , F( set) -> set } :

( card Y()) <= ( card A())

      provided

       A1: Y() = { F(w) where w be Element of A() : P[w] };

      

       A2: A() is finite;

      set Z = { F(w) where w be Element of A() : w in A() };

      Z is finite from FRAENKEL:sch 21( A2);

      then

      reconsider Z as finite set;

      

       A3: Z = { F(w) where w be Element of A() : w in A() };

      

       A4: ( card Z) <= ( card A()) from TREES_2:sch 3( A3);

      Y() c= Z

      proof

        let x be object;

        assume x in Y();

        then ex w be Element of A() st x = F(w) & P[w] by A1;

        hence x in Z;

      end;

      then ( card Y()) <= ( card Z) by NAT_1: 43;

      hence ( card Y()) <= ( card A()) by A4, XXREAL_0: 2;

    end;

    theorem :: DILWORTH:1

    

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

    proof

      let X,Y,x be set;

      assume not x in X;

      then

       A1: not x in (X \ Y);

      

      thus (X \ (Y \/ {x})) = ((X \ Y) \ {x}) by XBOOLE_1: 41

      .= (X \ Y) by A1, ZFMISC_1: 57;

    end;

    theorem :: DILWORTH:2

    

     Th2: for X,Y be set, F be Subset-Family of X, G be Subset-Family of Y holds (F \/ G) is Subset-Family of (X \/ Y)

    proof

      let X,Y be set, F be Subset-Family of X, G be Subset-Family of Y;

      

       A1: (F \/ G) c= (( bool X) \/ ( bool Y)) by XBOOLE_1: 13;

      (( bool X) \/ ( bool Y)) c= ( bool (X \/ Y)) by ZFMISC_1: 69;

      hence (F \/ G) is Subset-Family of (X \/ Y) by A1, XBOOLE_1: 1;

    end;

    theorem :: DILWORTH:3

    

     Th3: for X,Y be set, F be a_partition of X, G be a_partition of Y st X misses Y holds (F \/ G) is a_partition of (X \/ Y)

    proof

      let X,Y be set, F be a_partition of X, G be a_partition of Y such that

       A1: X misses Y;

      set PR = (F \/ G);

      set XY = (X \/ Y);

      

       A2: PR is Subset-Family of XY by Th2;

      

       A3: ( union PR) = (( union F) \/ ( union G)) by ZFMISC_1: 78

      .= (X \/ ( union G)) by EQREL_1:def 4

      .= (X \/ Y) by EQREL_1:def 4;

      now

        let A be Subset of XY such that

         A4: A in PR;

        A in F or A in G by A4, XBOOLE_0:def 3;

        hence A <> {} ;

        let B be Subset of XY such that

         A5: B in PR;

        per cases by A4, A5, XBOOLE_0:def 3;

          suppose A in F & B in F or A in G & B in G;

          hence A = B or A misses B by EQREL_1:def 4;

        end;

          suppose A in F & B in G or A in G & B in F;

          hence A = B or A misses B by A1, XBOOLE_1: 64;

        end;

      end;

      hence (F \/ G) is a_partition of (X \/ Y) by A2, A3, EQREL_1:def 4;

    end;

    theorem :: DILWORTH:4

    

     Th4: for X,Y be set, F be a_partition of Y st Y c< X holds (F \/ {(X \ Y)}) is a_partition of X

    proof

      let X,Y be set, F be a_partition of Y;

      assume

       A1: Y c< X;

      then

       A2: (X \ Y) <> {} by XBOOLE_1: 105;

      Y c= X by A1;

      then

       A3: (Y \/ (X \ Y)) = X by XBOOLE_1: 45;

       {(X \ Y)} is a_partition of (X \ Y) by A2, EQREL_1: 39;

      hence (F \/ {(X \ Y)}) is a_partition of X by A3, Th3, XBOOLE_1: 79;

    end;

    theorem :: DILWORTH:5

    

     Th5: for X be infinite set, n be Nat holds ex Y be finite Subset of X st ( card Y) > n

    proof

      let X be infinite set, n be Nat;

      consider f be sequence of X such that

       A1: f is one-to-one by DICKSON: 3;

      set Sn = ( Seg (n + 1));

      reconsider ff = (f | Sn) as Function of Sn, X by FUNCT_2: 32;

      ff is one-to-one by A1, FUNCT_1: 52;

      then ( card ff) = ( card ( rng ff)) by PRE_POLY: 19;

      then

       A2: ( card ( dom ff)) = ( card ( rng ff)) by CARD_1: 62;

      reconsider Y = ( rng ff) as finite Subset of X by RELAT_1:def 19;

      take Y;

      ( dom ff) = Sn by FUNCT_2:def 1;

      then ( card ( dom ff)) = (n + 1) by FINSEQ_1: 57;

      hence ( card Y) > n by A2, NAT_1: 13;

    end;

    begin

    definition

      let R be RelStr, S be Subset of R;

      :: DILWORTH:def1

      attr S is connected means

      : Def1: the InternalRel of R is_connected_in S;

    end

    notation

      let R be RelStr, S be Subset of R;

      synonym S is clique for S is connected;

    end

    registration

      let R be RelStr;

      cluster trivial -> clique for Subset of R;

      coherence

      proof

        let S be Subset of R;

        assume

         A1: S is trivial;

        let x1,x2 be object;

        thus thesis by A1, ZFMISC_1:def 10;

      end;

    end

    registration

      let R be RelStr;

      cluster clique for Subset of R;

      existence

      proof

        take ( {} R);

        let x1,x2 be object;

        thus thesis;

      end;

    end

    definition

      let R be RelStr;

      mode Clique of R is clique Subset of R;

    end

    theorem :: DILWORTH:6

    

     Th6: for R be RelStr, S be Subset of R holds S is Clique of R iff for a,b be Element of R st a in S & b in S & a <> b holds a <= b or b <= a

    proof

      let R be RelStr, S be Subset of R;

      set RR = the InternalRel of R;

      hereby

        assume S is Clique of R;

        then

         A1: RR is_connected_in S by Def1;

        let a,b be Element of R;

        assume a in S & b in S & a <> b;

        then [a, b] in RR or [b, a] in RR by A1;

        hence a <= b or b <= a;

      end;

      assume

       A2: for a,b be Element of R st a in S & b in S & a <> b holds a <= b or b <= a;

      RR is_connected_in S

      proof

        let x,y be object;

        assume

         A3: x in S & y in S & x <> y;

        then

        reconsider x9 = x, y9 = y as Element of R;

        x9 <= y9 or y9 <= x9 by A3, A2;

        hence [x, y] in RR or [y, x] in RR;

      end;

      hence S is Clique of R by Def1;

    end;

    registration

      let R be RelStr;

      cluster finite for Clique of R;

      existence

      proof

        take ( {} R);

        thus thesis;

      end;

    end

    registration

      let R be reflexive RelStr;

      cluster connected -> strongly_connected for Subset of R;

      coherence

      proof

        let C be Subset of R;

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

        assume C is clique;

        then

         A1: iR is_connected_in C;

        

         A2: iR is_reflexive_in cR by ORDERS_2:def 2;

        thus C is strongly_connected

        proof

          let x,y be object such that

           A3: x in C and

           A4: y in C;

          per cases ;

            suppose x = y;

            hence [x, y] in the InternalRel of R or [y, x] in the InternalRel of R by A3, A2;

          end;

            suppose x <> y;

            hence [x, y] in the InternalRel of R or [y, x] in the InternalRel of R by A3, A4, A1;

          end;

        end;

      end;

    end

    registration

      let R be non empty RelStr;

      cluster finite non empty for Clique of R;

      existence

      proof

         { the Element of R} is clique;

        hence thesis;

      end;

    end

    theorem :: DILWORTH:7

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

    proof

      let R be non empty RelStr, a1,a2 be Element of R;

      assume

       A1: a1 <> a2;

      

       A2: a1 in {a1, a2} & a2 in {a1, a2} by TARSKI:def 2;

      assume {a1, a2} is Clique of R;

      hence thesis by A2, A1, Th6;

    end;

    theorem :: DILWORTH:8

    

     Th8: for R be non empty RelStr, a1,a2 be Element of R st a1 <= a2 or a2 <= a1 holds {a1, a2} is Clique of R

    proof

      let R be non empty RelStr, a1,a2 be Element of R;

      assume

       A1: a1 <= a2 or a2 <= a1;

      now

        let x,y be Element of R;

        assume x in {a1, a2} & y in {a1, a2};

        then

         A2: (x = a1 or x = a2) & (y = a1 or y = a2) by TARSKI:def 2;

        assume x <> y;

        hence x <= y or y <= x by A1, A2;

      end;

      hence thesis by Th6;

    end;

    theorem :: DILWORTH:9

    

     Th9: for R be RelStr, C be Clique of R, S be Subset of C holds S is Clique of R

    proof

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

      set iR = the InternalRel of R;

      

       A1: iR is_connected_in C by Def1;

      iR is_connected_in S by A1;

      hence thesis by Def1, XBOOLE_1: 1;

    end;

    theorem :: DILWORTH:10

    for R be RelStr, C be finite Clique of R, n be Nat st n <= ( card C) holds ex B be finite Clique of R st B c= C & ( card B) = n

    proof

      let R be RelStr, C be finite Clique of R, n be Nat such that

       A1: n <= ( card C);

      consider BB be finite Subset of C such that

       A2: ( card BB) = n by A1, FINSEQ_4: 72;

      reconsider BB as finite Clique of R by Th9;

      take BB;

      thus thesis by A2;

    end;

    theorem :: DILWORTH:11

    

     Th11: for R be transitive RelStr, C be Clique of R, x,y be Element of R st x is_maximal_in C & x <= y holds (C \/ {y}) is Clique of R

    proof

      let R be transitive RelStr, C be Clique of R, x,y be Element of R such that

       A1: x is_maximal_in C and

       A2: x <= y;

      

       A3: x in C by A1, WAYBEL_4: 55;

      

       A4: the carrier of R is non empty by A1, WAYBEL_4: 55;

      set Cb = (C \/ {y});

      

       A5: Cb c= the carrier of R

      proof

        let x be object;

        assume

         A6: x in Cb;

        per cases by A6, XBOOLE_0:def 3;

          suppose x in C;

          hence x in the carrier of R;

        end;

          suppose x in {y};

          then x = y by TARSKI:def 1;

          hence x in the carrier of R by A4;

        end;

      end;

      now

        let a,b be Element of R such that

         A7: a in Cb & b in Cb and

         A8: a <> b;

        per cases by A7, XBOOLE_0:def 3;

          suppose a in C & b in C;

          hence a <= b or b <= a by A8, Th6;

        end;

          suppose that

           A9: a in C and

           A10: b in {y};

          

           A11: b = y by A10, TARSKI:def 1;

          

           A12: not x < a by A1, A9, WAYBEL_4: 55;

          per cases ;

            suppose x <> a;

            then a <= x or x <= a by A9, A3, Th6;

            hence a <= b or b <= a by A2, A11, A12, ORDERS_2: 3;

          end;

            suppose x = a;

            hence a <= b or b <= a by A2, A10, TARSKI:def 1;

          end;

        end;

          suppose that

           A13: a in {y} and

           A14: b in C;

          

           A15: a = y by A13, TARSKI:def 1;

          

           A16: not x < b by A1, A14, WAYBEL_4: 55;

          per cases ;

            suppose x <> b;

            then b <= x or x <= b by A14, A3, Th6;

            hence a <= b or b <= a by A2, A15, A16, ORDERS_2: 3;

          end;

            suppose x = b;

            hence a <= b or b <= a by A2, A13, TARSKI:def 1;

          end;

        end;

          suppose a in {y} & b in {y};

          then a = y & b = y by TARSKI:def 1;

          hence a <= b or b <= a by A8;

        end;

      end;

      hence (C \/ {y}) is Clique of R by A5, Th6;

    end;

    theorem :: DILWORTH:12

    

     Th12: for R be transitive RelStr, C be Clique of R, x,y be Element of R st x is_minimal_in C & y <= x holds (C \/ {y}) is Clique of R

    proof

      let R be transitive RelStr, C be Clique of R, x,y be Element of R such that

       A1: x is_minimal_in C and

       A2: y <= x;

      

       A3: x in C by A1, WAYBEL_4: 56;

      

       A4: the carrier of R is non empty by A1, WAYBEL_4: 56;

      set Cb = (C \/ {y});

      

       A5: Cb c= the carrier of R

      proof

        let x be object;

        assume

         A6: x in Cb;

        per cases by A6, XBOOLE_0:def 3;

          suppose x in C;

          hence x in the carrier of R;

        end;

          suppose x in {y};

          then x = y by TARSKI:def 1;

          hence x in the carrier of R by A4;

        end;

      end;

      now

        let a,b be Element of R such that

         A7: a in Cb & b in Cb and

         A8: a <> b;

        per cases by A7, XBOOLE_0:def 3;

          suppose a in C & b in C;

          hence a <= b or b <= a by A8, Th6;

        end;

          suppose that

           A9: a in C and

           A10: b in {y};

          

           A11: b = y by A10, TARSKI:def 1;

          

           A12: not a < x by A1, A9, WAYBEL_4: 56;

          per cases ;

            suppose

             A13: a <> x;

            then not a <= x by A12;

            then x <= a by A9, A3, A13, Th6;

            hence a <= b or b <= a by A2, A11, ORDERS_2: 3;

          end;

            suppose x = a;

            hence a <= b or b <= a by A2, A10, TARSKI:def 1;

          end;

        end;

          suppose that

           A14: a in {y} and

           A15: b in C;

          

           A16: a = y by A14, TARSKI:def 1;

          

           A17: not b < x by A1, A15, WAYBEL_4: 56;

          per cases ;

            suppose

             A18: b <> x;

            then not b <= x by A17;

            then x <= b by A15, A3, A18, Th6;

            hence a <= b or b <= a by A2, A16, ORDERS_2: 3;

          end;

            suppose x = b;

            hence a <= b or b <= a by A2, A14, TARSKI:def 1;

          end;

        end;

          suppose a in {y} & b in {y};

          then a = y & b = y by TARSKI:def 1;

          hence a <= b or b <= a by A8;

        end;

      end;

      hence (C \/ {y}) is Clique of R by A5, Th6;

    end;

    definition

      let R be RelStr, S be Subset of R;

      :: DILWORTH:def2

      attr S is stable means

      : Def2: for x,y be Element of R st x in S & y in S & x <> y holds not x <= y & not y <= x;

    end

    registration

      let R be RelStr;

      cluster trivial -> stable for Subset of R;

      coherence by ZFMISC_1:def 10;

    end

    registration

      let R be RelStr;

      cluster stable for Subset of R;

      existence

      proof

        reconsider A = {} as Subset of R by XBOOLE_1: 2;

        take A;

        let x,y be Element of R;

        thus thesis;

      end;

    end

    definition

      let R be RelStr;

      mode StableSet of R is stable Subset of R;

    end

    registration

      let R be RelStr;

      cluster finite for StableSet of R;

      existence

      proof

        take ( {} R);

        thus thesis;

      end;

    end

    registration

      let R be non empty RelStr;

      cluster finite non empty for StableSet of R;

      existence

      proof

         { the Element of R} is stable;

        hence thesis;

      end;

    end

    theorem :: DILWORTH:13

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

    proof

      let R be non empty RelStr, a1,a2 be Element of R;

      assume

       A1: a1 <> a2;

      

       A2: a1 in {a1, a2} & a2 in {a1, a2} by TARSKI:def 2;

      assume {a1, a2} is StableSet of R;

      hence thesis by A2, A1, Def2;

    end;

    theorem :: DILWORTH:14

    

     Th14: for R be non empty RelStr, a1,a2 be Element of R st not (a1 <= a2 or a2 <= a1) holds {a1, a2} is StableSet of R

    proof

      let R be non empty RelStr, a1,a2 be Element of R;

      assume

       A1: not (a1 <= a2 or a2 <= a1);

      set S = {a1, a2};

      S is stable

      proof

        let x,y be Element of R such that

         A2: x in S & y in S & x <> y;

        (x = a1 or x = a2) & (y = a1 or y = a2) by A2, TARSKI:def 2;

        hence thesis by A1, A2;

      end;

      hence thesis;

    end;

    theorem :: DILWORTH:15

    

     Th15: for R be RelStr, C be Clique of R, A be StableSet of R, a,b be set st a in A & b in A & a in C & b in C holds a = b

    proof

      let R be RelStr, C be Clique of R, A be StableSet of R, a,b be set such that

       A1: a in A & b in A and

       A2: a in C & b in C;

      assume

       A3: a <> b;

      reconsider a9 = a, b9 = b as Element of R by A1;

       not a9 <= b9 & not b9 <= a9 by A1, A3, Def2;

      hence contradiction by A2, A3, Th6;

    end;

    theorem :: DILWORTH:16

    

     Th16: for R be RelStr, A be StableSet of R, B be Subset of A holds B is StableSet of R

    proof

      let R be RelStr, A be StableSet of R, B be Subset of A;

      reconsider BB = B as Subset of R by XBOOLE_1: 1;

      BB is stable by Def2;

      hence thesis;

    end;

    theorem :: DILWORTH:17

    

     Th17: for R be RelStr, A be finite StableSet of R, n be Nat st n <= ( card A) holds ex B be finite StableSet of R st ( card B) = n

    proof

      let R be RelStr, A be finite StableSet of R, n be Nat such that

       A1: n <= ( card A);

      consider BB be finite Subset of A such that

       A2: ( card BB) = n by A1, FINSEQ_4: 72;

      reconsider BB as finite StableSet of R by Th16;

      take BB;

      thus ( card BB) = n by A2;

    end;

    begin

    definition

      let R be RelStr;

      :: DILWORTH:def3

      attr R is with_finite_clique# means

      : Def3: ex C be finite Clique of R st for D be finite Clique of R holds ( card D) <= ( card C);

    end

    registration

      cluster finite -> with_finite_clique# for RelStr;

      coherence

      proof

        let R be RelStr;

        assume R is finite;

        then

        reconsider R9 = R as finite RelStr;

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

        

         A1: for k be Nat st P[k] holds k <= ( card R9) by NAT_1: 43;

        ( card ( {} R)) = 0 ;

        then

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

        consider k be Nat such that

         A3: P[k] and

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

        consider c be finite Clique of R such that

         A5: ( card c) = k by A3;

        for D be finite Clique of R holds ( card D) <= ( card c) by A5, A4;

        hence R is with_finite_clique#;

      end;

    end

    registration

      let R be with_finite_clique# RelStr;

      cluster -> finite for Clique of R;

      coherence

      proof

        let D be Clique of R;

        consider C be finite Clique of R such that

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

        assume D is infinite;

        then

        consider Y be finite Subset of D such that

         A2: ( card Y) > ( card C) by Th5;

        Y is Clique of R by Th9;

        hence contradiction by A2, A1;

      end;

    end

    definition

      let R be with_finite_clique# RelStr;

      :: DILWORTH:def4

      func clique# R -> Nat means

      : Def4: (ex C be finite Clique of R st ( card C) = it ) & for T be finite Clique of R holds ( card T) <= it ;

      existence

      proof

        consider A be finite Clique of R such that

         A1: for B be finite Clique of R holds ( card B) <= ( card A) by Def3;

        take itt = ( card A);

        thus ex A be finite Clique of R st ( card A) = itt;

        let T be finite Clique of R;

        thus ( card T) <= itt by A1;

      end;

      uniqueness

      proof

        let it1,it2 be Nat such that

         A2: ex S1 be finite Clique of R st ( card S1) = it1 and

         A3: for T be finite Clique of R holds ( card T) <= it1 and

         A4: ex S2 be finite Clique of R st ( card S2) = it2 and

         A5: for T be finite Clique of R holds ( card T) <= it2;

        consider S1 be finite Clique of R such that

         A6: ( card S1) = it1 by A2;

        consider S2 be finite Clique of R such that

         A7: ( card S2) = it2 by A4;

        it1 <= it2 & it2 <= it1 by A6, A7, A3, A5;

        hence it1 = it2 by XXREAL_0: 1;

      end;

    end

    registration

      let R be empty RelStr;

      cluster ( clique# R) -> empty;

      coherence

      proof

        for T be Clique of R holds ( card T) <= ( card ( {} R));

        hence thesis by Def4;

      end;

    end

    registration

      let R be with_finite_clique# non empty RelStr;

      cluster ( clique# R) -> positive;

      coherence

      proof

        ( card { the Element of R}) <= ( clique# R) by Def4;

        hence thesis;

      end;

    end

    theorem :: DILWORTH:18

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

    proof

      let R be with_finite_clique# non empty RelStr;

      assume

       A1: ( [#] R) is StableSet of R;

      

       A2: ( clique# R) >= ( 0 + 1) by NAT_1: 13;

      consider A be finite Clique of R such that

       A3: ( card A) = ( clique# R) by Def4;

      assume ( clique# R) <> 1;

      then ( card A) > 1 by A2, A3, XXREAL_0: 1;

      then

      consider a,b be set such that

       A4: a in A and

       A5: b in A and

       A6: a <> b by NAT_1: 59;

      thus thesis by A4, A5, A6, A1, Th15;

    end;

    theorem :: DILWORTH:19

    

     Th19: for R be with_finite_clique# RelStr st ( clique# R) = 1 holds ( [#] R) is StableSet of R

    proof

      let R be with_finite_clique# RelStr;

      assume

       A1: ( clique# R) = 1;

      set cR = the carrier of R;

      

       A2: R is non empty by A1;

      now

        let a,b be Element of R such that a in cR and b in cR and

         A3: a <> b;

        assume a <= b or b <= a;

        then

         A4: {a, b} is Clique of R by A2, Th8;

        ( card {a, b}) = 2 by A3, CARD_2: 57;

        hence contradiction by A4, A1, Def4;

      end;

      hence ( [#] R) is StableSet of R by Def2;

    end;

    definition

      let R be RelStr;

      :: DILWORTH:def5

      attr R is with_finite_stability# means

      : Def5: ex A be finite StableSet of R st for B be finite StableSet of R holds ( card B) <= ( card A);

    end

    registration

      cluster finite -> with_finite_stability# for RelStr;

      coherence

      proof

        let R be RelStr;

        assume R is finite;

        then

        reconsider R9 = R as finite RelStr;

        defpred P[ Nat] means ex A be finite StableSet of R9 st ( card A) = $1;

        

         A1: for k be Nat st P[k] holds k <= ( card R9) by NAT_1: 43;

        ( {} R) is StableSet of R & ( card {} ) = 0 ;

        then

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

        consider k be Nat such that

         A3: P[k] and

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

        consider S be finite StableSet of R such that

         A5: ( card S) = k by A3;

        take S;

        let T be finite StableSet of R;

        thus ( card T) <= ( card S) by A5, A4;

      end;

    end

    registration

      let R be with_finite_stability# RelStr;

      cluster -> finite for StableSet of R;

      coherence

      proof

        consider A be finite StableSet of R such that

         A1: for B be finite StableSet of R holds ( card A) >= ( card B) by Def5;

        given B be StableSet of R such that

         A2: B is infinite;

        consider C be finite Subset of B such that

         A3: ( card C) > ( card A) by A2, Th5;

        C is StableSet of R by Th16;

        hence contradiction by A1, A3;

      end;

    end

    definition

      let R be with_finite_stability# RelStr;

      :: DILWORTH:def6

      func stability# R -> Nat means

      : Def6: (ex A be finite StableSet of R st ( card A) = it ) & for T be finite StableSet of R holds ( card T) <= it ;

      existence

      proof

        consider A be finite StableSet of R such that

         A1: for B be finite StableSet of R holds ( card A) >= ( card B) by Def5;

        take itt = ( card A);

        thus ex A be finite StableSet of R st ( card A) = itt;

        let T be finite StableSet of R;

        thus ( card T) <= itt by A1;

      end;

      uniqueness

      proof

        let it1,it2 be Nat such that

         A2: ex S1 be finite StableSet of R st ( card S1) = it1 and

         A3: for T be finite StableSet of R holds ( card T) <= it1 and

         A4: ex S2 be finite StableSet of R st ( card S2) = it2 and

         A5: for T be finite StableSet of R holds ( card T) <= it2;

        consider S1 be finite StableSet of R such that

         A6: ( card S1) = it1 by A2;

        consider S2 be finite StableSet of R such that

         A7: ( card S2) = it2 by A4;

        it1 <= it2 & it2 <= it1 by A3, A5, A6, A7;

        hence it1 = it2 by XXREAL_0: 1;

      end;

    end

    registration

      let R be empty RelStr;

      cluster ( stability# R) -> empty;

      coherence

      proof

        for T be StableSet of R holds ( card T) <= ( card ( {} R));

        hence thesis by Def6;

      end;

    end

    registration

      let R be with_finite_stability# non empty RelStr;

      cluster ( stability# R) -> positive;

      coherence

      proof

        ( card { the Element of R}) <= ( stability# R) by Def6;

        hence thesis;

      end;

    end

    theorem :: DILWORTH:20

    

     Th20: for R be with_finite_stability# non empty RelStr st ( [#] R) is Clique of R holds ( stability# R) = 1

    proof

      let R be with_finite_stability# non empty RelStr;

      assume

       A1: ( [#] R) is Clique of R;

      

       A2: ( stability# R) >= ( 0 + 1) by NAT_1: 13;

      consider A be finite StableSet of R such that

       A3: ( card A) = ( stability# R) by Def6;

      assume ( stability# R) <> 1;

      then ( card A) > 1 by A2, A3, XXREAL_0: 1;

      then

      consider a,b be set such that

       A4: a in A and

       A5: b in A and

       A6: a <> b by NAT_1: 59;

      thus thesis by A4, A5, A6, A1, Th15;

    end;

    theorem :: DILWORTH:21

    

     Th21: for R be with_finite_stability# RelStr st ( stability# R) = 1 holds ( [#] R) is Clique of R

    proof

      let R be with_finite_stability# RelStr;

      assume

       A1: ( stability# R) = 1;

      set cR = the carrier of R;

      now

        let a,b be Element of R such that

         A2: a in cR and b in cR and

         A3: a <> b;

        

         A4: R is non empty by A2;

        assume not (a <= b or b <= a);

        then

         A5: {a, b} is StableSet of R by A4, Th14;

        ( card {a, b}) = 2 by A3, CARD_2: 57;

        hence contradiction by A1, Def6, A5;

      end;

      hence ( [#] R) is Clique of R by Th6;

    end;

    registration

      cluster with_finite_clique# with_finite_stability# -> finite for RelStr;

      coherence

      proof

        let R be RelStr;

        assume

         A1: R is with_finite_clique#;

        assume

         A2: R is with_finite_stability#;

        assume

         A3: R is infinite;

        reconsider R as with_finite_clique# with_finite_stability# RelStr by A1, A2;

        consider C be finite Clique of R such that

         A4: ( card C) = ( clique# R) by Def4;

        consider An be finite StableSet of R such that

         A5: ( card An) = ( stability# R) by Def6;

        set h = ( clique# R), w = ( stability# R);

        

         A6: ( 0 + 1) <= h by A3, NAT_1: 13;

        

         A7: ( 0 + 1) <= w by A3, NAT_1: 13;

        set cR = the carrier of R;

        

         A8: cR = ( [#] R);

        per cases by A6, A7, XXREAL_0: 1;

          suppose h = 1;

          then

           A9: cR is StableSet of R by A8, Th19;

          consider Y be finite Subset of cR such that

           A10: ( card Y) > w by A3, Th5;

          Y is StableSet of R by A9, Th16;

          hence thesis by A10, Def6;

        end;

          suppose w = 1;

          then

           A11: cR is Clique of R by A8, Th21;

          consider Y be finite Subset of cR such that

           A12: ( card Y) > h by A3, Th5;

          Y is Clique of R by A11, Th9;

          hence thesis by A12, Def4;

        end;

          suppose

           A13: h > 1 & w > 1;

          set m = (( max (( clique# R),( stability# R))) + 1);

          reconsider m as Nat;

          consider r be Nat such that

           A14: for X be finite set, P be a_partition of ( the_subsets_of_card (2,X)) st ( card X) >= r & ( card P) = 2 holds ex S be Subset of X st ( card S) >= m & S is_homogeneous_for P by RAMSEY_1: 17;

          consider Y be finite Subset of R such that

           A15: ( card Y) > r by A3, Th5;

          set X = ((Y \/ An) \/ C);

          reconsider X as finite Subset of R;

          Y c= (Y \/ An) & (Y \/ An) c= ((Y \/ An) \/ C) by XBOOLE_1: 7;

          then

           A16: ( card Y) <= ( card X) by NAT_1: 43, XBOOLE_1: 1;

          set A = { {x, y} where x,y be Element of R : x <> y & x in X & y in X & (x <= y or y <= x) };

          set B = { {x, y} where x,y be Element of R : x <> y & x in X & y in X & not (x <= y or y <= x) };

          set E = ( the_subsets_of_card (2,X));

          set P = {A, B};

          

           A17: A c= E

          proof

            let x be object;

            reconsider x1 = x as set by TARSKI: 1;

            assume x in A;

            then

            consider xx,yy be Element of R such that

             A18: {xx, yy} = x and

             A19: xx <> yy and

             A20: xx in X and

             A21: yy in X and xx <= yy or yy <= xx;

            x is Subset of X & ( card x1) = 2 by A18, A19, A20, A21, CARD_2: 57, ZFMISC_1: 32;

            hence thesis;

          end;

          

           A22: B c= E

          proof

            let x be object;

            reconsider x1 = x as set by TARSKI: 1;

            assume x in B;

            then

            consider xx,yy be Element of R such that

             A23: {xx, yy} = x and

             A24: xx <> yy and

             A25: xx in X and

             A26: yy in X and not (xx <= yy or yy <= xx);

            x is Subset of X & ( card x1) = 2 by A23, A24, A25, A26, CARD_2: 57, ZFMISC_1: 32;

            hence thesis;

          end;

          

           A27: A in P & B in P by TARSKI:def 2;

           A28:

          now

            assume

             A29: A = B;

            consider a,b be set such that

             A30: a in An and

             A31: b in An and

             A32: a <> b by A13, A5, NAT_1: 59;

            reconsider a, b as Element of R by A30, A31;

            

             A33: not (a <= b or b <= a) by A30, A31, A32, Def2;

            a in (Y \/ An) & b in (Y \/ An) by A30, A31, XBOOLE_0:def 3;

            then a in X & b in X by XBOOLE_0:def 3;

            then {a, b} in B by A33, A32;

            then

            consider aa,bb be Element of R such that

             A34: {a, b} = {aa, bb} and aa <> bb & aa in X & bb in X and

             A35: aa <= bb or bb <= aa by A29;

            a = aa & b = bb or a = bb & b = aa by A34, ZFMISC_1: 6;

            hence contradiction by A35, A30, A31, A32, Def2;

          end;

          

           A36: P c= ( bool E)

          proof

            let x be object;

            reconsider xx = x as set by TARSKI: 1;

            assume x in P;

            then xx c= E by A17, A22, TARSKI:def 2;

            hence thesis;

          end;

          

           A37: ( union P) = E

          proof

            thus ( union P) c= E

            proof

              let x be object;

              assume x in ( union P);

              then

              consider Y be set such that

               A38: x in Y and

               A39: Y in P by TARSKI:def 4;

              Y = A or Y = B by A39, TARSKI:def 2;

              hence thesis by A38, A17, A22;

            end;

            thus E c= ( union P)

            proof

              let x be object;

              assume x in E;

              then

              consider xx be Subset of X such that

               A40: x = xx and

               A41: ( card xx) = 2;

              consider a,b be object such that

               A42: a <> b and

               A43: xx = {a, b} by A41, CARD_2: 60;

              a in xx & b in xx by A43, TARSKI:def 2;

              then a in X & b in X;

              then

              reconsider a, b as Element of R;

              

               A44: a in xx & b in xx by A43, TARSKI:def 2;

               not (a <= b or b <= a) or (a <= b or b <= a);

              then {a, b} in A or {a, b} in B by A44, A42;

              hence x in ( union P) by A40, A43, A27, TARSKI:def 4;

            end;

          end;

          for a be Subset of E st a in P holds a <> {} & for b be Subset of E st b in P holds a = b or a misses b

          proof

            let a be Subset of E such that

             A45: a in P;

            thus a <> {}

            proof

              per cases by A45, TARSKI:def 2;

                suppose

                 A46: a = A;

                consider aa,bb be set such that

                 A47: aa in C and

                 A48: bb in C and

                 A49: aa <> bb by A13, A4, NAT_1: 59;

                reconsider aa, bb as Element of R by A47, A48;

                

                 A50: aa <= bb or bb <= aa by A47, A48, A49, Th6;

                aa in ((Y \/ An) \/ C) & bb in ((Y \/ An) \/ C) by A47, A48, XBOOLE_0:def 3;

                then {aa, bb} in A by A50, A49;

                hence thesis by A46;

              end;

                suppose

                 A51: a = B;

                consider aa,bb be set such that

                 A52: aa in An and

                 A53: bb in An and

                 A54: aa <> bb by A13, A5, NAT_1: 59;

                reconsider aa, bb as Element of R by A52, A53;

                

                 A55: not (aa <= bb or bb <= aa) by A52, A53, A54, Def2;

                aa in (Y \/ An) & bb in (Y \/ An) by A52, A53, XBOOLE_0:def 3;

                then aa in X & bb in X by XBOOLE_0:def 3;

                then {aa, bb} in B by A55, A54;

                hence thesis by A51;

              end;

            end;

            let b be Subset of E such that

             A56: b in P;

            assume

             A57: a <> b;

            assume

             A58: a meets b;

            (a = A or a = B) & (b = A or b = B) by A45, A56, TARSKI:def 2;

            then (A /\ B) <> {} by A57, A58;

            then

            consider x be object such that

             A59: x in (A /\ B) by XBOOLE_0:def 1;

            x in A by A59, XBOOLE_0:def 4;

            then

            consider xx,yy be Element of R such that

             A60: {xx, yy} = x and xx <> yy & xx in X & yy in X and

             A61: xx <= yy or yy <= xx;

            x in B by A59, XBOOLE_0:def 4;

            then

            consider x2,y2 be Element of R such that

             A62: {x2, y2} = x and x2 <> y2 & x2 in X & y2 in X and

             A63: not (x2 <= y2 or y2 <= x2);

            xx = x2 & yy = y2 or xx = y2 & yy = x2 by A60, A62, ZFMISC_1: 6;

            hence contradiction by A61, A63;

          end;

          then

          reconsider P as a_partition of E by A37, A36, EQREL_1:def 4;

          ( card P) = 2 by A28, CARD_2: 57;

          then

          consider S be Subset of X such that

           A64: ( card S) >= m and

           A65: S is_homogeneous_for P by A16, A14, A15, XXREAL_0: 2;

          reconsider S as finite Subset of R by XBOOLE_1: 1;

          ( max (( clique# R),( stability# R))) >= ( clique# R) by XXREAL_0: 25;

          then m > ( clique# R) by NAT_1: 13;

          then

           A66: ( card S) > ( clique# R) by A64, XXREAL_0: 2;

          ( max (( clique# R),( stability# R))) >= ( stability# R) by XXREAL_0: 25;

          then m > ( stability# R) by NAT_1: 13;

          then

           A67: ( card S) > ( stability# R) by A64, XXREAL_0: 2;

          consider p be Element of P such that

           A68: ( the_subsets_of_card (2,S)) c= p by A65, RAMSEY_1:def 1;

          per cases by TARSKI:def 2;

            suppose

             A69: p = A;

            now

              let x,y be Element of R such that

               A70: x in S and

               A71: y in S and

               A72: x <> y;

               {x, y} is Subset of S & ( card {x, y}) = 2 by A70, A71, A72, CARD_2: 57, ZFMISC_1: 32;

              then {x, y} in ( the_subsets_of_card (2,S));

              then {x, y} in A by A69, A68;

              then

              consider xx,yy be Element of R such that

               A73: {xx, yy} = {x, y} and xx <> yy & xx in X & yy in X and

               A74: xx <= yy or yy <= xx;

              xx = x & yy = y or xx = y & yy = x by A73, ZFMISC_1: 6;

              hence x <= y or y <= x by A74;

            end;

            then S is Clique of R by Th6;

            hence contradiction by A66, Def4;

          end;

            suppose

             A75: p = B;

            S is stable

            proof

              let x,y be Element of R such that

               A76: x in S and

               A77: y in S and

               A78: x <> y;

               {x, y} is Subset of S & ( card {x, y}) = 2 by A76, A77, A78, CARD_2: 57, ZFMISC_1: 32;

              then {x, y} in ( the_subsets_of_card (2,S));

              then {x, y} in B by A75, A68;

              then

              consider xx,yy be Element of R such that

               A79: {xx, yy} = {x, y} and xx <> yy & xx in X & yy in X and

               A80: not (xx <= yy or yy <= xx);

              xx = x & yy = y or xx = y & yy = x by A79, ZFMISC_1: 6;

              hence not x <= y & not y <= x by A80;

            end;

            hence contradiction by A67, Def6;

          end;

        end;

      end;

    end

    begin

    definition

      let R be RelStr, X be Subset of R;

      :: DILWORTH:def7

      func Lower X -> Subset of R equals (X \/ ( downarrow X));

      coherence ;

      :: DILWORTH:def8

      func Upper X -> Subset of R equals (X \/ ( uparrow X));

      coherence ;

    end

    theorem :: DILWORTH:22

    

     Th22: for R be antisymmetric transitive RelStr, A be StableSet of R, z be set st z in ( Upper A) & z in ( Lower A) holds z in A

    proof

      let R be antisymmetric transitive RelStr, A be StableSet of R, z be set such that

       A1: z in ( Upper A) and

       A2: z in ( Lower A);

      per cases ;

        suppose z in A;

        hence thesis;

      end;

        suppose

         A3: not z in A;

        then

         A4: z in ( uparrow A) by A1, XBOOLE_0:def 3;

        

         A5: z in ( downarrow A) by A2, A3, XBOOLE_0:def 3;

        reconsider y = z as Element of R by A1;

        consider x be Element of R such that

         A6: x <= y and

         A7: x in A by A4, WAYBEL_0:def 16;

        reconsider x9 = z as Element of R by A2;

        consider y9 be Element of R such that

         A8: x9 <= y9 and

         A9: y9 in A by A5, WAYBEL_0:def 15;

        x <= y9 by A6, A8, YELLOW_0:def 2;

        then x = y9 by A7, A9, Def2;

        hence z in A by A6, A7, A8, YELLOW_0:def 3;

      end;

    end;

    theorem :: DILWORTH:23

    

     Th23: for R be with_finite_stability# RelStr, A be StableSet of R st ( card A) = ( stability# R) holds (( Upper A) \/ ( Lower A)) = ( [#] R)

    proof

      let R be with_finite_stability# RelStr, A be StableSet of R such that

       A1: ( card A) = ( stability# R);

      set cP = the carrier of R;

      cP c= (( Upper A) \/ ( Lower A))

      proof

        let x be object;

        assume

         A2: x in cP;

        assume

         A3: not x in (( Upper A) \/ ( Lower A));

        reconsider x as Element of cP by A2;

        

         A4: not x in ( Upper A) by A3, XBOOLE_0:def 3;

        then

         A5: not x in A by XBOOLE_0:def 3;

        

         A6: not x in ( uparrow A) by A4, XBOOLE_0:def 3;

         not x in ( Lower A) by A3, XBOOLE_0:def 3;

        then

         A7: not x in ( downarrow A) by XBOOLE_0:def 3;

        set Ax = (A \/ {x});

        

         A8: {x} c= the carrier of R by A2, ZFMISC_1: 31;

        now

          let a,b be Element of R such that

           A9: a in Ax and

           A10: b in Ax and

           A11: a <> b;

          per cases by A9, A10, XBOOLE_0:def 3;

            suppose a in A & b in A;

            hence not a <= b & not b <= a by A11, Def2;

          end;

            suppose

             A12: a in A & b in {x};

            then b = x by TARSKI:def 1;

            hence not a <= b & not b <= a by A6, A7, A12, WAYBEL_0:def 15, WAYBEL_0:def 16;

          end;

            suppose

             A13: a in {x} & b in A;

            then a = x by TARSKI:def 1;

            hence not a <= b & not b <= a by A6, A7, A13, WAYBEL_0:def 15, WAYBEL_0:def 16;

          end;

            suppose a in {x} & b in {x};

            then a = x & b = x by TARSKI:def 1;

            hence not a <= b & not b <= a by A11;

          end;

        end;

        then

         A14: Ax is StableSet of R by A8, Def2, XBOOLE_1: 8;

        ( card Ax) = (( card A) + 1) by A5, CARD_2: 41;

        then ( card Ax) > ( card A) by NAT_1: 13;

        hence contradiction by Def6, A1, A14;

      end;

      hence (( Upper A) \/ ( Lower A)) = ( [#] R);

    end;

    theorem :: DILWORTH:24

    

     Th24: for R be transitive RelStr, x be Element of R, S be Subset of R st x is_minimal_in ( Lower S) holds x is_minimal_in ( [#] R)

    proof

      let R be transitive RelStr, x be Element of R, S be Subset of R such that

       A1: x is_minimal_in ( Lower S);

      set cR = the carrier of R;

      

       A2: x in ( Lower S) by A1, WAYBEL_4: 56;

      assume not x is_minimal_in ( [#] R);

      then

      consider y be Element of R such that y in cR and

       A3: y < x by A2, WAYBEL_4: 56;

      per cases by A2, XBOOLE_0:def 3;

        suppose

         A4: x in S;

        y <= x by A3;

        then y in ( downarrow S) by A4, WAYBEL_0:def 15;

        then y in ( Lower S) by XBOOLE_0:def 3;

        hence thesis by A1, A3, WAYBEL_4: 56;

      end;

        suppose x in ( downarrow S);

        then

        consider x99 be Element of R such that

         A5: x <= x99 and

         A6: x99 in S by WAYBEL_0:def 15;

        y <= x by A3;

        then y <= x99 by A5, YELLOW_0:def 2;

        then y in ( downarrow S) by A6, WAYBEL_0:def 15;

        then y in ( Lower S) by XBOOLE_0:def 3;

        hence contradiction by A1, A3, WAYBEL_4: 56;

      end;

    end;

    theorem :: DILWORTH:25

    

     Th25: for R be transitive RelStr, x be Element of R, S be Subset of R st x is_maximal_in ( Upper S) holds x is_maximal_in ( [#] R)

    proof

      let R be transitive RelStr, x be Element of R, S be Subset of R such that

       A1: x is_maximal_in ( Upper S);

      set cR = the carrier of R;

      

       A2: x in ( Upper S) by A1, WAYBEL_4: 55;

      assume not x is_maximal_in ( [#] R);

      then

      consider y be Element of R such that y in cR and

       A3: x < y by A2, WAYBEL_4: 55;

      per cases by A2, XBOOLE_0:def 3;

        suppose

         A4: x in S;

        x <= y by A3;

        then y in ( uparrow S) by A4, WAYBEL_0:def 16;

        then y in ( Upper S) by XBOOLE_0:def 3;

        hence thesis by A1, A3, WAYBEL_4: 55;

      end;

        suppose x in ( uparrow S);

        then

        consider x99 be Element of R such that

         A5: x99 <= x and

         A6: x99 in S by WAYBEL_0:def 16;

        x <= y by A3;

        then x99 <= y by A5, YELLOW_0:def 2;

        then y in ( uparrow S) by A6, WAYBEL_0:def 16;

        then y in ( Upper S) by XBOOLE_0:def 3;

        hence contradiction by A1, A3, WAYBEL_4: 55;

      end;

    end;

    definition

      let R be RelStr;

      set cR = the carrier of R;

      :: DILWORTH:def9

      func minimals R -> Subset of R means

      : Def9: for x be Element of R holds x in it iff x is_minimal_in ( [#] R) if R is non empty

      otherwise it = {} ;

      consistency ;

      existence

      proof

        defpred P[ object] means ex a be Element of R st a = $1 & a is_minimal_in cR;

        consider X be set such that

         A1: for x be object holds x in X iff x in cR & P[x] from XBOOLE_0:sch 1;

         A2:

        now

          assume

           A3: cR is non empty;

          for x be object st x in X holds x in cR by A1;

          then

          reconsider X as Subset of R by TARSKI:def 3;

          take X;

          let x be Element of R;

          x in X implies P[x] by A1;

          hence x in X iff x is_minimal_in cR by A1, A3;

        end;

        now

          reconsider X = {} as Subset of R by XBOOLE_1: 2;

          take X;

          thus X = {} ;

        end;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let it1,it2 be Subset of R;

        now

          assume that R is non empty and

           A4: for x be Element of R holds x in it1 iff x is_minimal_in cR and

           A5: for x be Element of R holds x in it2 iff x is_minimal_in cR;

          for x be object holds x in it1 iff x in it2 by A4, A5;

          hence it1 = it2 by TARSKI: 2;

        end;

        hence thesis;

      end;

      :: DILWORTH:def10

      func maximals R -> Subset of R means

      : Def10: for x be Element of R holds x in it iff x is_maximal_in ( [#] R) if R is non empty

      otherwise it = {} ;

      consistency ;

      existence

      proof

        defpred P[ object] means ex a be Element of R st a = $1 & a is_maximal_in cR;

        consider X be set such that

         A6: for x be object holds x in X iff x in cR & P[x] from XBOOLE_0:sch 1;

         A7:

        now

          assume

           A8: cR is non empty;

          for x be object st x in X holds x in cR by A6;

          then

          reconsider X as Subset of R by TARSKI:def 3;

          take X;

          let x be Element of R;

          x in X implies P[x] by A6;

          hence x in X iff x is_maximal_in cR by A6, A8;

        end;

        now

          reconsider X = {} as Subset of R by XBOOLE_1: 2;

          take X;

          thus X = {} ;

        end;

        hence thesis by A7;

      end;

      uniqueness

      proof

        let it1,it2 be Subset of R;

        now

          assume that R is non empty and

           A9: for x be Element of R holds x in it1 iff x is_maximal_in cR and

           A10: for x be Element of R holds x in it2 iff x is_maximal_in cR;

          for x be object holds x in it1 iff x in it2 by A9, A10;

          hence it1 = it2 by TARSKI: 2;

        end;

        hence thesis;

      end;

    end

    registration

      let R be with_finite_clique# non empty antisymmetric transitive RelStr;

      cluster ( maximals R) -> non empty;

      coherence

      proof

        set cP = the carrier of R, iP = the InternalRel of R;

        consider CL be finite Clique of R such that

         A1: for D be finite Clique of R holds ( card D) <= ( card CL) by Def3;

        ( card { the Element of R}) <= ( card CL) by A1;

        then CL <> {} ;

        then

        consider y be Element of R such that y in CL and

         A2: y is_maximal_wrt (CL,iP) by BAGORDER: 6;

        

         A3: y is_maximal_in CL by A2, WAYBEL_4:def 24;

        

         A4: cP = ( [#] R);

        now

          assume not y is_maximal_in cP;

          then

          consider z be Element of R such that z in cP and

           A5: y < z by WAYBEL_4: 55;

          

           A6: y <= z by A5;

          set C = (CL \/ {z});

          reconsider C as finite Clique of R by A6, A3, Th11;

           not z in CL by A3, A5, WAYBEL_4: 55;

          then ( card C) = (( card CL) + 1) by CARD_2: 41;

          then (( card CL) + 1) <= (( card CL) + 0 ) by A1;

          hence contradiction by XREAL_1: 6;

        end;

        hence thesis by A4, Def10;

      end;

      cluster ( minimals R) -> non empty;

      coherence

      proof

        set cP = the carrier of R, iP = the InternalRel of R;

        consider CL be finite Clique of R such that

         A7: for D be finite Clique of R holds ( card D) <= ( card CL) by Def3;

        ( card { the Element of R}) <= ( card CL) by A7;

        then CL <> {} ;

        then

        consider y be Element of R such that y in CL and

         A8: y is_minimal_wrt (CL,iP) by BAGORDER: 7;

        

         A9: y is_minimal_in CL by A8, WAYBEL_4:def 26;

        

         A10: cP = ( [#] R);

        now

          assume not y is_minimal_in cP;

          then

          consider z be Element of R such that z in cP and

           A11: z < y by WAYBEL_4: 56;

          

           A12: z <= y by A11;

          set C = (CL \/ {z});

          reconsider C as finite Clique of R by A12, A9, Th12;

           not z in CL by A9, A11, WAYBEL_4: 56;

          then ( card C) = (( card CL) + 1) by CARD_2: 41;

          then (( card CL) + 1) <= (( card CL) + 0 ) by A7;

          hence contradiction by XREAL_1: 6;

        end;

        hence thesis by A10, Def9;

      end;

    end

    registration

      let R be RelStr;

      cluster ( minimals R) -> stable;

      coherence

      proof

        set mR = ( minimals R);

        let x,y be Element of R such that

         A1: x in mR and

         A2: y in mR and

         A3: x <> y;

        

         A4: R is non empty by A1;

        then y is_minimal_in ( [#] R) by A2, Def9;

        then not y > x by A1, WAYBEL_4: 56;

        hence not x <= y by A3;

        x is_minimal_in ( [#] R) by A1, A4, Def9;

        then not x > y by A2, WAYBEL_4: 56;

        hence not y <= x by A3;

      end;

      cluster ( maximals R) -> stable;

      coherence

      proof

        set mR = ( maximals R);

        let x,y be Element of R such that

         A5: x in mR and

         A6: y in mR and

         A7: x <> y;

        

         A8: R is non empty by A5;

        then x is_maximal_in ( [#] R) by A5, Def10;

        then not y > x by A6, WAYBEL_4: 55;

        hence not x <= y by A7;

        y is_maximal_in ( [#] R) by A6, A8, Def10;

        then not x > y by A5, WAYBEL_4: 55;

        hence not y <= x by A7;

      end;

    end

    theorem :: DILWORTH:26

    

     Th26: for R be RelStr, A be StableSet of R st not ( minimals R) c= A holds not ( minimals R) c= ( Upper A)

    proof

      let R be RelStr, A be StableSet of R;

      assume not ( minimals R) c= A;

      then

      consider x be object such that

       A1: x in ( minimals R) and

       A2: not x in A;

      assume

       A3: ( minimals R) c= ( Upper A);

      reconsider x9 = x as Element of R by A1;

      R is non empty by A1;

      then

       A4: x9 is_minimal_in ( [#] R) by A1, Def9;

      x9 in ( uparrow A) by A2, A1, A3, XBOOLE_0:def 3;

      then

      consider x99 be Element of R such that

       A5: x99 <= x9 and

       A6: x99 in A by WAYBEL_0:def 16;

      now

        assume x99 <> x9;

        then x99 < x9 by A5;

        hence contradiction by A1, A4, WAYBEL_4: 56;

      end;

      hence contradiction by A6, A2;

    end;

    theorem :: DILWORTH:27

    

     Th27: for R be RelStr, A be StableSet of R st not ( maximals R) c= A holds not ( maximals R) c= ( Lower A)

    proof

      let R be RelStr, A be StableSet of R such that

       A1: not ( maximals R) c= A;

      consider x be object such that

       A2: x in ( maximals R) and

       A3: not x in A by A1;

      assume

       A4: ( maximals R) c= ( Lower A);

      reconsider x9 = x as Element of R by A2;

      R is non empty by A2;

      then

       A5: x9 is_maximal_in ( [#] R) by A2, Def10;

      x9 in ( downarrow A) by A3, A2, A4, XBOOLE_0:def 3;

      then

      consider x99 be Element of R such that

       A6: x9 <= x99 and

       A7: x99 in A by WAYBEL_0:def 15;

      now

        assume x99 <> x9;

        then x9 < x99 by A6;

        hence contradiction by A2, A5, WAYBEL_4: 55;

      end;

      hence contradiction by A7, A3;

    end;

    begin

    registration

      let R be RelStr, X be finite Subset of R;

      cluster ( subrelstr X) -> finite;

      coherence by YELLOW_0:def 15;

    end

    theorem :: DILWORTH:28

    

     Th28: for R be RelStr, S be Subset of R, C be Clique of ( subrelstr S) holds C is Clique of R

    proof

      let R be RelStr, S be Subset of R, C be Clique of ( subrelstr S);

      

       A1: the carrier of ( subrelstr S) = S by YELLOW_0:def 15;

      now

        let a,b be Element of R such that

         A2: a in C and

         A3: b in C and

         A4: a <> b;

        reconsider a9 = a, b9 = b as Element of ( subrelstr S) by A2, A3;

        a9 <= b9 or b9 <= a9 by A2, A3, A4, Th6;

        hence a <= b or b <= a by YELLOW_0: 59;

      end;

      hence C is Clique of R by A1, Th6, XBOOLE_1: 1;

    end;

    theorem :: DILWORTH:29

    

     Th29: for R be RelStr, S be Subset of R, C be Clique of R holds (C /\ S) is Clique of ( subrelstr S)

    proof

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

      set sS = ( subrelstr S), CS = (C /\ S);

      

       A1: CS c= S by XBOOLE_1: 17;

      

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

      now

        let a,b be Element of sS;

        assume

         A3: a in CS;

        assume

         A4: b in CS;

        assume

         A5: a <> b;

        

         A6: a in S & b in S by A3, A4, XBOOLE_0:def 4;

        

         A7: S is non empty by A3;

        R is non empty by A3;

        then

        reconsider a9 = a, b9 = b as Element of R by A7, YELLOW_0: 58;

        a9 in C & b9 in C by A3, A4, XBOOLE_0:def 4;

        then a9 <= b9 or b9 <= a9 by A5, Th6;

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

      end;

      hence (C /\ S) is Clique of ( subrelstr S) by Th6, A1, YELLOW_0:def 15;

    end;

    theorem :: DILWORTH:30

    

     Th30: for R be RelStr, S be Subset of R, A be StableSet of ( subrelstr S) holds A is StableSet of R

    proof

      let R be RelStr, S be Subset of R, A be StableSet of ( subrelstr S);

      set sS = ( subrelstr S);

      per cases ;

        suppose R is empty;

        then the carrier of sS = {} by YELLOW_0:def 15;

        then A = ( {} R);

        hence A is StableSet of R;

      end;

        suppose

         A1: R is non empty;

        per cases ;

          suppose S is empty;

          then the carrier of sS = {} by YELLOW_0:def 15;

          then A = ( {} R);

          hence A is StableSet of R;

        end;

          suppose

           A2: S is non empty;

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

          then

          reconsider A as Subset of R by XBOOLE_1: 1;

          A is stable

          proof

            let x,y be Element of R such that

             A3: x in A and

             A4: y in A and

             A5: x <> y;

            reconsider x9 = x, y9 = y as Element of sS by A3, A4;

             not x9 <= y9 & not y9 <= x9 by A3, A4, A5, Def2;

            hence not x <= y & not y <= x by A1, A2, YELLOW_0: 60;

          end;

          hence thesis;

        end;

      end;

    end;

    theorem :: DILWORTH:31

    

     Th31: for R be RelStr, S be Subset of R, A be StableSet of R holds (A /\ S) is StableSet of ( subrelstr S)

    proof

      let R be RelStr, S be Subset of R, A be StableSet of R;

      set sS = ( subrelstr S), AS = (A /\ S);

      per cases ;

        suppose R is empty;

        then (A /\ S) = ( {} sS);

        hence (A /\ S) is StableSet of sS;

      end;

        suppose

         A1: R is non empty;

        per cases ;

          suppose S is empty;

          then (A /\ S) = ( {} sS);

          hence (A /\ S) is StableSet of sS;

        end;

          suppose

           A2: S is non empty;

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

          then

          reconsider AS as Subset of sS by XBOOLE_1: 17;

          AS is stable

          proof

            let x,y be Element of sS such that

             A3: x in AS and

             A4: y in AS and

             A5: x <> y;

            reconsider x9 = x, y9 = y as Element of R by A1, A2, YELLOW_0: 58;

            

             A6: x9 in A by A3, XBOOLE_0:def 4;

            y9 in A by A4, XBOOLE_0:def 4;

            then not x9 <= y9 & not y9 <= x9 by A6, A5, Def2;

            hence not x <= y & not y <= x by YELLOW_0: 59;

          end;

          hence (A /\ S) is StableSet of sS;

        end;

      end;

    end;

    theorem :: DILWORTH:32

    

     Th32: for R be RelStr, S be Subset of R, B be Subset of ( subrelstr S), x be Element of ( subrelstr S), y be Element of R st x = y & x is_maximal_in B holds y is_maximal_in B

    proof

      let R be RelStr, S be Subset of R, B be Subset of ( subrelstr S), x be Element of ( subrelstr S), y be Element of R such that

       A1: x = y and

       A2: x is_maximal_in B;

      

       A3: x in B by A2, WAYBEL_4: 55;

      assume not y is_maximal_in B;

      then

      consider z be Element of R such that

       A4: z in B and

       A5: y < z by A1, A3, WAYBEL_4: 55;

      

       A6: y <= z by A5;

      reconsider z9 = z as Element of ( subrelstr S) by A4;

      x <= z9 by A4, A6, A1, YELLOW_0: 60;

      then x < z9 by A5, A1;

      hence contradiction by A4, A2, WAYBEL_4: 55;

    end;

    theorem :: DILWORTH:33

    

     Th33: for R be RelStr, S be Subset of R, B be Subset of ( subrelstr S), x be Element of ( subrelstr S), y be Element of R st x = y & x is_minimal_in B holds y is_minimal_in B

    proof

      let R be RelStr, S be Subset of R, B be Subset of ( subrelstr S), x be Element of ( subrelstr S), y be Element of R such that

       A1: x = y and

       A2: x is_minimal_in B;

      

       A3: x in B by A2, WAYBEL_4: 56;

      assume not y is_minimal_in B;

      then

      consider z be Element of R such that

       A4: z in B and

       A5: z < y by A1, A3, WAYBEL_4: 56;

      

       A6: z <= y by A5;

      reconsider z9 = z as Element of ( subrelstr S) by A4;

      z9 <= x by A4, A6, A1, YELLOW_0: 60;

      then z9 < x by A5, A1;

      hence contradiction by A4, A2, WAYBEL_4: 56;

    end;

    theorem :: DILWORTH:34

    

     Th34: for R be transitive RelStr, A be StableSet of R, C be Clique of ( subrelstr ( Lower A)), a,b be Element of R st a in A & a in C & b in C holds a = b or b <= a

    proof

      let R be transitive RelStr, A be StableSet of R, C be Clique of ( subrelstr ( Lower A)), a,b be Element of R such that

       A1: a in A and

       A2: a in C and

       A3: b in C;

      set ap = ( subrelstr ( Lower A));

      reconsider a9 = a as Element of ap by A2;

      

       A4: b in the carrier of ap by A3;

      reconsider b9 = b as Element of ap by A3;

      

       A5: b9 in ( Lower A) by A4, YELLOW_0:def 15;

      

       A6: C is Clique of R by Th28;

      per cases by A5, XBOOLE_0:def 3;

        suppose b9 in A;

        hence thesis by A1, A2, A3, A6, Th15;

      end;

        suppose b9 in ( downarrow A);

        then

        consider c be Element of R such that

         A7: b <= c and

         A8: c in A by WAYBEL_0:def 15;

        per cases ;

          suppose

           A9: a <> b;

          per cases by A9, A2, A3, Th6;

            suppose a9 <= b9;

            then a <= b by YELLOW_0: 59;

            then a <= c by A7, YELLOW_0:def 2;

            hence thesis by A8, A7, A1, Def2;

          end;

            suppose b9 <= a9;

            hence thesis by YELLOW_0: 59;

          end;

        end;

          suppose a = b;

          hence thesis;

        end;

      end;

    end;

    theorem :: DILWORTH:35

    

     Th35: for R be transitive RelStr, A be StableSet of R, C be Clique of ( subrelstr ( Upper A)), a,b be Element of R st a in A & a in C & b in C holds a = b or a <= b

    proof

      let R be transitive RelStr, A be StableSet of R, C be Clique of ( subrelstr ( Upper A)), a,b be Element of R such that

       A1: a in A and

       A2: a in C and

       A3: b in C;

      set ap = ( subrelstr ( Upper A));

      reconsider a9 = a as Element of ap by A2;

      

       A4: b in the carrier of ap by A3;

      reconsider b9 = b as Element of ap by A3;

      

       A5: b9 in ( Upper A) by A4, YELLOW_0:def 15;

      

       A6: C is Clique of R by Th28;

      per cases by A5, XBOOLE_0:def 3;

        suppose b9 in A;

        hence thesis by A1, A2, A3, A6, Th15;

      end;

        suppose b9 in ( uparrow A);

        then

        consider c be Element of R such that

         A7: c <= b and

         A8: c in A by WAYBEL_0:def 16;

        per cases ;

          suppose

           A9: a <> b;

          per cases by A9, A2, A3, Th6;

            suppose a9 <= b9;

            hence thesis by YELLOW_0: 59;

          end;

            suppose b9 <= a9;

            then b <= a by YELLOW_0: 59;

            then c <= a by A7, YELLOW_0:def 2;

            hence thesis by A8, A7, A1, Def2;

          end;

        end;

          suppose a = b;

          hence thesis;

        end;

      end;

    end;

    registration

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

      cluster ( subrelstr S) -> with_finite_clique#;

      coherence

      proof

        consider C be finite Clique of R such that

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

        set sS = ( subrelstr S);

        defpred P[ Nat] means ex c be finite Clique of sS st ( card c) = $1;

        

         A2: for k be Nat st P[k] holds k <= ( card C)

        proof

          let k be Nat;

          assume P[k];

          then

          consider c be finite Clique of sS such that

           A3: ( card c) = k;

          c is finite Clique of R by Th28;

          hence thesis by A3, A1;

        end;

        ( card ( {} sS)) = 0 ;

        then

         A4: ex k be Nat st P[k];

        consider k be Nat such that

         A5: P[k] and

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

        consider c be finite Clique of sS such that

         A7: ( card c) = k by A5;

        for D be finite Clique of sS holds ( card D) <= ( card c) by A7, A6;

        hence sS is with_finite_clique#;

      end;

    end

    registration

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

      cluster ( subrelstr S) -> with_finite_stability#;

      coherence

      proof

        consider A be finite StableSet of R such that

         A1: for B be finite StableSet of R holds ( card A) >= ( card B) by Def5;

        assume

         A2: not ( subrelstr S) is with_finite_stability#;

        defpred P[ Nat] means ex C be finite StableSet of ( subrelstr S) st ( card C) = $1 & ex B be finite StableSet of ( subrelstr S) st $1 < ( card B);

        

         A3: P[ 0 ]

        proof

          reconsider C = ( {} ( subrelstr S)) as finite StableSet of ( subrelstr S);

          take C;

          thus ( card C) = 0 ;

          hence thesis by A2;

        end;

        

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

        proof

          let n be Nat;

          given C be finite StableSet of ( subrelstr S) such that ( card C) = n and

           A5: ex B be finite StableSet of ( subrelstr S) st n < ( card B);

          consider B be finite Subset of ( subrelstr S) such that

           A6: n < ( card B) & B is StableSet of ( subrelstr S) by A5;

          (n + 1) <= ( card B) by A6, NAT_1: 13;

          then

          consider BB be finite StableSet of ( subrelstr S) such that

           A7: ( card BB) = (n + 1) by A6, Th17;

          take BB;

          thus ( card BB) = (n + 1) by A7;

          consider Bb be finite StableSet of ( subrelstr S) such that

           A8: ( card BB) < ( card Bb) by A2;

          take Bb;

          thus (n + 1) < ( card Bb) by A8, A7;

        end;

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

        then

        consider C be finite StableSet of ( subrelstr S) such that ( card C) = ( card A) and

         A9: ex B be finite StableSet of ( subrelstr S) st ( card A) < ( card B);

        consider B be finite StableSet of ( subrelstr S) such that

         A10: ( card A) < ( card B) by A9;

        B is StableSet of R by Th30;

        hence contradiction by A1, A10;

      end;

    end

    theorem :: DILWORTH:36

    

     Th36: for R be with_finite_clique# non empty antisymmetric transitive RelStr, x be Element of R holds ex y be Element of R st y is_minimal_in ( [#] R) & (y = x or y < x)

    proof

      let R be with_finite_clique# non empty antisymmetric transitive RelStr, x be Element of R;

      set sx = ( Lower {x});

      set sL = ( subrelstr sx);

      reconsider sL as with_finite_clique# non empty antisymmetric transitive RelStr;

      consider y be object such that

       A1: y in ( minimals sL) by XBOOLE_0:def 1;

      reconsider y as Element of sL by A1;

      

       A2: ( [#] sL) = sx by YELLOW_0:def 15;

      then

       A3: y is_minimal_in sx by A1, Def9;

      reconsider y9 = y as Element of R by YELLOW_0: 58;

      take y9;

      sx c= the carrier of sL by YELLOW_0:def 15;

      hence y9 is_minimal_in ( [#] R) by A3, Th33, Th24;

      per cases ;

        suppose y9 = x;

        hence thesis;

      end;

        suppose y9 <> x;

        then not y9 in {x} by TARSKI:def 1;

        then y9 in ( downarrow x) by A2, XBOOLE_0:def 3;

        then y9 <= x by WAYBEL_0: 17;

        hence thesis;

      end;

    end;

    theorem :: DILWORTH:37

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

    proof

      let R be with_finite_clique# antisymmetric transitive RelStr;

      set ap = ( Upper ( minimals R));

      set cR = the carrier of R;

      cR c= ap

      proof

        let x be object;

        assume

         A1: x in cR;

        then

        reconsider x9 = x as Element of R;

        

         A2: R is non empty by A1;

        then

        consider y be Element of R such that

         A3: y is_minimal_in ( [#] R) and

         A4: y = x9 or y < x9 by Th36;

        

         A5: y in ( minimals R) by A3, A2, Def9;

        per cases by A4;

          suppose x9 = y;

          hence thesis by A5, XBOOLE_0:def 3;

        end;

          suppose y < x9;

          then y <= x9;

          then x in ( uparrow ( minimals R)) by A5, WAYBEL_0:def 16;

          hence x in ap by XBOOLE_0:def 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: DILWORTH:38

    

     Th38: for R be with_finite_clique# non empty antisymmetric transitive RelStr, x be Element of R holds ex y be Element of R st y is_maximal_in ( [#] R) & (y = x or x < y)

    proof

      let R be with_finite_clique# non empty antisymmetric transitive RelStr, x be Element of R;

      set ax = ( Upper {x});

      set sU = ( subrelstr ax);

      reconsider sU as with_finite_clique# non empty antisymmetric transitive RelStr;

      consider y be object such that

       A1: y in ( maximals sU) by XBOOLE_0:def 1;

      reconsider y as Element of sU by A1;

      

       A2: ( [#] sU) = ax by YELLOW_0:def 15;

      then

       A3: y is_maximal_in ax by A1, Def10;

      reconsider y9 = y as Element of R by YELLOW_0: 58;

      take y9;

      ax c= the carrier of sU by YELLOW_0:def 15;

      hence y9 is_maximal_in ( [#] R) by A3, Th32, Th25;

      per cases ;

        suppose y9 = x;

        hence thesis;

      end;

        suppose y9 <> x;

        then not y9 in {x} by TARSKI:def 1;

        then y9 in ( uparrow x) by A2, XBOOLE_0:def 3;

        then x <= y9 by WAYBEL_0: 18;

        hence thesis;

      end;

    end;

    theorem :: DILWORTH:39

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

    proof

      let P be with_finite_clique# antisymmetric transitive RelStr;

      set ap = ( Lower ( maximals P));

      set cP = the carrier of P;

      cP c= ap

      proof

        let x be object;

        assume

         A1: x in cP;

        then

        reconsider x9 = x as Element of P;

        

         A2: P is non empty by A1;

        then

        consider y be Element of P such that

         A3: y is_maximal_in ( [#] P) and

         A4: y = x9 or y > x9 by Th38;

        

         A5: y in ( maximals P) by A3, A2, Def10;

        per cases by A4;

          suppose x9 = y;

          hence thesis by A5, XBOOLE_0:def 3;

        end;

          suppose y > x9;

          then x9 <= y;

          then x in ( downarrow ( maximals P)) by A5, WAYBEL_0:def 15;

          hence x in ap by XBOOLE_0:def 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: DILWORTH:40

    

     Th40: for R be with_finite_clique# antisymmetric transitive RelStr, A be StableSet of R st ( minimals R) c= A holds A = ( minimals R)

    proof

      let R be with_finite_clique# antisymmetric transitive RelStr, A be StableSet of R such that

       A1: ( minimals R) c= A;

      A c= ( minimals R)

      proof

        let x be object;

        assume

         A2: x in A;

        then

         A3: R is non empty;

        reconsider x9 = x as Element of R by A2;

        consider y be Element of R such that

         A4: y is_minimal_in ( [#] R) and

         A5: y = x9 or y < x9 by A3, Th36;

        

         A6: y = x9 or y <= x9 by A5;

        y in ( minimals R) by A3, A4, Def9;

        hence x in ( minimals R) by A1, A2, A6, Def2;

      end;

      hence A = ( minimals R) by A1;

    end;

    theorem :: DILWORTH:41

    

     Th41: for R be with_finite_clique# antisymmetric transitive RelStr, A be StableSet of R st ( maximals R) c= A holds A = ( maximals R)

    proof

      let R be with_finite_clique# antisymmetric transitive RelStr, A be StableSet of R such that

       A1: ( maximals R) c= A;

      A c= ( maximals R)

      proof

        let x be object;

        assume

         A2: x in A;

        then

         A3: R is non empty;

        reconsider x9 = x as Element of R by A2;

        consider y be Element of R such that

         A4: y is_maximal_in ( [#] R) and

         A5: y = x9 or x9 < y by A3, Th38;

        

         A6: y = x9 or x9 <= y by A5;

        y in ( maximals R) by A3, A4, Def10;

        hence x in ( maximals R) by A1, A2, A6, Def2;

      end;

      hence A = ( maximals R) by A1;

    end;

    theorem :: DILWORTH:42

    

     Th42: for R be with_finite_clique# RelStr, S be Subset of R holds ( clique# ( subrelstr S)) <= ( clique# R)

    proof

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

      set s = ( subrelstr S);

      consider c be finite Clique of s such that

       A1: ( card c) = ( clique# s) by Def4;

      c is Clique of R by Th28;

      hence ( clique# ( subrelstr S)) <= ( clique# R) by Def4, A1;

    end;

    theorem :: DILWORTH:43

    for R be with_finite_clique# RelStr, C be Clique of R, S be Subset of R st ( card C) = ( clique# R) & C c= S holds ( clique# ( subrelstr S)) = ( clique# R)

    proof

      let R be with_finite_clique# RelStr, C be Clique of R, S be Subset of R such that

       A1: ( card C) = ( clique# R) and

       A2: C c= S;

      C = (C /\ S) by A2, XBOOLE_1: 28;

      then

       A3: C is Clique of ( subrelstr S) by Th29;

      consider Cs be Clique of ( subrelstr S) such that

       A4: ( card Cs) = ( clique# ( subrelstr S)) by Def4;

      

       A5: ( card C) <= ( card Cs) by A3, A4, Def4;

      ( clique# ( subrelstr S)) <= ( clique# R) by Th42;

      hence ( clique# ( subrelstr S)) = ( clique# R) by A4, A1, A5, XXREAL_0: 1;

    end;

    theorem :: DILWORTH:44

    

     Th44: for R be with_finite_stability# RelStr, S be Subset of R holds ( stability# ( subrelstr S)) <= ( stability# R)

    proof

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

      consider As be StableSet of ( subrelstr S) such that

       A1: ( card As) = ( stability# ( subrelstr S)) by Def6;

      As is StableSet of R by Th30;

      hence ( stability# ( subrelstr S)) <= ( stability# R) by A1, Def6;

    end;

    theorem :: DILWORTH:45

    

     Th45: for R be with_finite_stability# RelStr, A be StableSet of R, S be Subset of R st ( card A) = ( stability# R) & A c= S holds ( stability# ( subrelstr S)) = ( stability# R)

    proof

      let R be with_finite_stability# RelStr, A be StableSet of R, S be Subset of R such that

       A1: ( card A) = ( stability# R) and

       A2: A c= S;

      A = (A /\ S) by A2, XBOOLE_1: 28;

      then

       A3: A is StableSet of ( subrelstr S) by Th31;

      consider As be StableSet of ( subrelstr S) such that

       A4: ( card As) = ( stability# ( subrelstr S)) by Def6;

      

       A5: ( card A) <= ( card As) by A3, A4, Def6;

      ( stability# ( subrelstr S)) <= ( stability# R) by Th44;

      hence ( stability# ( subrelstr S)) = ( stability# R) by A4, A1, A5, XXREAL_0: 1;

    end;

    begin

    definition

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

      :: DILWORTH:def11

      attr P is Clique-wise means

      : Def11: for x be set st x in P holds x is Clique of R;

    end

    registration

      let R be RelStr;

      cluster Clique-wise for a_partition of the carrier of R;

      existence

      proof

        set cR = the carrier of R;

        per cases ;

          suppose R is empty;

          then

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

          take S;

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

        end;

          suppose

           A1: R is non empty;

          take S = ( SmallestPartition cR);

          let z be set;

          assume

           A2: z in S;

          S = the set of all {x} where x be Element of cR by A1, EQREL_1: 37;

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

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

        end;

      end;

    end

    definition

      let R be RelStr;

      mode Clique-partition of R is Clique-wise a_partition of the carrier of R;

    end

    registration

      let R be empty RelStr;

      cluster empty -> Clique-wise for a_partition of the carrier of R;

      coherence ;

    end

    theorem :: DILWORTH:46

    

     Th46: for R be finite RelStr, C be Clique-partition of R holds ( card C) >= ( stability# R)

    proof

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

      assume

       A1: ( card C) < ( stability# R);

      consider A be StableSet of R such that

       A2: ( card A) = ( stability# R) by Def6;

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

      then

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

      set cR = the carrier of R;

      per cases ;

        suppose R is empty;

        hence contradiction by A1;

      end;

        suppose

         A4: R is non empty;

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

        

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

           A6: x in A;

          reconsider x9 = x as Element of R by A6;

          cR is non empty by A4;

          then x9 in cR;

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

          then

          consider y be set such that

           A7: x in y and

           A8: y in C by TARSKI:def 4;

          take y;

          thus thesis by A6, A7, A8;

        end;

        consider f be Function of A, C such that

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

        consider x,y be object such that

         A10: x in A and

         A11: y in A and

         A12: x <> y and

         A13: (f . x) = (f . y) by A4, A3, FINSEQ_4: 65;

        (f . x) in C by A10, FUNCT_2: 5;

        then

         A14: (f . x) is Clique of R by Def11;

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

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

        hence contradiction by A14, A10, A11, A12, Th15;

      end;

    end;

    theorem :: DILWORTH:47

    

     Th47: for R be with_finite_stability# RelStr, A be StableSet of R, C be Clique-partition of R st ( card C) = ( card A) holds ex f be Function of A, C st f is bijective & for x be set st x in A holds x in (f . x)

    proof

      let R be with_finite_stability# RelStr, A be StableSet of R, C be Clique-partition of R;

      assume that

       A1: ( card C) = ( card A);

      set cR = the carrier of R;

      per cases ;

        suppose

         A2: R is empty;

        then the carrier of R is empty;

        then

         A3: C = {} ;

        set f = the Function of A, C;

        ( dom f) = {} by A2;

        then

        reconsider f = {} as Function of A, C by RELAT_1: 41;

        

         A4: f is onto by A3, FUNCT_2:def 3, RELAT_1: 38;

        take f;

        thus f is bijective by A4;

        thus thesis;

      end;

        suppose

         A5: R is non empty;

        defpred P[ 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 x9 = x as Element of R;

          cR is non empty by A5;

          then x9 in cR;

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

          then

          consider y 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);

        take f;

        

         A11: f is one-to-one

        proof

          let x1,x2 be object such that

           A12: x1 in ( dom f) and

           A13: x2 in ( dom f) and

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

           P[x1, (f . x1)] by A12, A10;

          then

           A15: x1 in (f . x1);

           P[x2, (f . x2)] by A13, A10;

          then

           A16: x2 in (f . x2);

          (f . x1) in C by A5, A12, FUNCT_2: 5;

          then (f . x1) is Clique of R by Def11;

          hence x1 = x2 by A12, A13, A15, A16, A14, Th15;

        end;

        C is finite by A1;

        then f is onto by A1, A11, FINSEQ_4: 63;

        hence f is bijective by A11;

        let x be set;

        assume x in A;

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

        hence x in (f . x);

      end;

    end;

    theorem :: DILWORTH:48

    

     Th48: for R be finite RelStr, A be StableSet of R, C be Clique-partition of R st ( card C) = ( card A) holds for c be set st c in C holds ex a be Element of A st (c /\ A) = {a}

    proof

      let R be finite RelStr, A be StableSet of R, C be Clique-partition of R such that

       A1: ( card C) = ( card A);

      consider f be Function of A, C such that

       A2: f is bijective and

       A3: for x be set st x in A holds x in (f . x) by A1, Th47;

      let c be set such that

       A4: c in C;

      ( rng f) = C by A2, FUNCT_2:def 3;

      then

      consider x be object such that

       A5: x in ( dom f) and

       A6: c = (f . x) by A4, FUNCT_1:def 3;

      

       A7: x in c by A5, A6, A3;

      reconsider a = x as Element of A by A5;

      take a;

      now

        let z be object;

        hereby

          assume z in (c /\ A);

          then

           A8: z in c & z in A by XBOOLE_0:def 4;

          c is Clique of R by A4, Def11;

          hence z = a by A8, A7, Th15;

        end;

        assume z = a;

        hence z in (c /\ A) by A7, A5, XBOOLE_0:def 4;

      end;

      hence (c /\ A) = {a} by TARSKI:def 1;

    end;

    theorem :: DILWORTH:49

    

     Th49: for R be with_finite_stability# antisymmetric transitive non empty RelStr, A be StableSet of R, U be Clique-partition of ( subrelstr ( Upper A)), L be Clique-partition of ( subrelstr ( Lower A)) st ( card A) = ( stability# R) & ( card U) = ( stability# R) & ( card L) = ( stability# R) holds ex C be Clique-partition of R st ( card C) = ( stability# R)

    proof

      let R be with_finite_stability# antisymmetric transitive non empty RelStr, A be StableSet of R, U be Clique-partition of ( subrelstr ( Upper A)), L be Clique-partition of ( subrelstr ( Lower A)) such that

       A1: ( card A) = ( stability# R) and

       A2: ( card U) = ( stability# R) and

       A3: ( card L) = ( stability# R);

      

       A4: A is non empty by A1;

      set aA = ( Upper A), bA = ( Lower A);

      set cR = the carrier of R, Pa = ( subrelstr aA), Pb = ( subrelstr bA);

      

       A5: aA = the carrier of Pa by YELLOW_0:def 15;

      

       A6: bA = the carrier of Pb by YELLOW_0:def 15;

      reconsider Pa = ( subrelstr ( Upper A)) as with_finite_stability# antisymmetric transitive non empty RelStr by A4;

      (A /\ ( Upper A)) = A by XBOOLE_1: 21;

      then A is StableSet of Pa by Th31;

      then

      consider f be Function of A, U such that

       A7: f is bijective and

       A8: for x be set st x in A holds x in (f . x) by A1, A2, Th47;

      

       A9: ( dom f) = A by A4, FUNCT_2:def 1;

      

       A10: ( rng f) = U by A7, FUNCT_2:def 3;

      reconsider Pb = ( subrelstr ( Lower A)) as with_finite_stability# antisymmetric transitive non empty RelStr by A4;

      (A /\ ( Lower A)) = A by XBOOLE_1: 21;

      then A is StableSet of Pb by Th31;

      then

      consider g be Function of A, L such that

       A11: g is bijective and

       A12: for x be set st x in A holds x in (g . x) by A1, A3, Th47;

      

       A13: ( dom g) = A by A4, FUNCT_2:def 1;

      

       A14: ( rng g) = L by A11, FUNCT_2:def 3;

      set h = (f .\/ g);

      set C = ( rng h);

      

       A15: ( dom h) = (( dom f) \/ ( dom g)) by LEXBFS:def 2;

      

       A16: C c= ( bool cR)

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in C;

        then

        consider a be object such that

         A17: a in ( dom h) and

         A18: (h . a) = x by FUNCT_1:def 3;

        

         A19: (h . a) = ((f . a) \/ (g . a)) by A17, A15, LEXBFS:def 2;

        (f . a) in U by A17, A15, FUNCT_2: 5;

        then

         A20: (f . a) c= cR by A5, XBOOLE_1: 1;

        (g . a) in L by A17, A15, FUNCT_2: 5;

        then (g . a) c= cR by A6, XBOOLE_1: 1;

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

        hence x in ( bool cR);

      end;

      

       A21: ( union C) = cR

      proof

        now

          let x be object;

          hereby

            assume x in ( union C);

            then

            consider Y be set such that

             A22: x in Y and

             A23: Y in C by TARSKI:def 4;

            consider a be object such that

             A24: a in ( dom h) and

             A25: Y = (h . a) by A23, FUNCT_1:def 3;

            

             A26: x in ((f . a) \/ (g . a)) by A24, A25, A22, A15, LEXBFS:def 2;

            per cases by A26, XBOOLE_0:def 3;

              suppose

               A27: x in (f . a);

              (f . a) in U by A24, A15, FUNCT_2: 5;

              then x in aA by A27, A5;

              hence x in cR;

            end;

              suppose

               A28: x in (g . a);

              (g . a) in L by A24, A15, FUNCT_2: 5;

              then x in bA by A28, A6;

              hence x in cR;

            end;

          end;

          assume x in ( [#] R);

          then

           A29: x in (( Upper A) \/ ( Lower A)) by A1, Th23;

          per cases by A29, XBOOLE_0:def 3;

            suppose x in ( Upper A);

            then x in ( union U) by A5, EQREL_1:def 4;

            then

            consider Y be set such that

             A30: x in Y and

             A31: Y in U by TARSKI:def 4;

            consider a be object such that

             A32: a in ( dom f) and

             A33: Y = (f . a) by A31, A10, FUNCT_1:def 3;

            

             A34: (h . a) in ( rng h) by A32, A15, A9, A13, FUNCT_1: 3;

            (h . a) = ((f . a) \/ (g . a)) by A32, A15, A9, A13, LEXBFS:def 2;

            then x in (h . a) by A30, A33, XBOOLE_0:def 3;

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

          end;

            suppose x in ( Lower A);

            then x in ( union L) by A6, EQREL_1:def 4;

            then

            consider Y be set such that

             A35: x in Y and

             A36: Y in L by TARSKI:def 4;

            consider a be object such that

             A37: a in ( dom g) and

             A38: Y = (g . a) by A36, A14, FUNCT_1:def 3;

            

             A39: (h . a) in ( rng h) by A37, A15, A9, A13, FUNCT_1: 3;

            (h . a) = ((f . a) \/ (g . a)) by A37, A15, A9, A13, LEXBFS:def 2;

            then x in (h . a) by A35, A38, XBOOLE_0:def 3;

            hence x in ( union C) by A39, TARSKI:def 4;

          end;

        end;

        hence thesis by TARSKI: 2;

      end;

       A40:

      now

        let a be Subset of cR;

        assume a in C;

        then

        consider x be object such that

         A41: x in ( dom h) and

         A42: (h . x) = a by FUNCT_1:def 3;

        

         A43: (h . x) = ((f . x) \/ (g . x)) by A41, A15, LEXBFS:def 2;

        set cfx = (f . x), cgx = (g . x);

        

         A44: cfx in U by A41, A15, FUNCT_2: 5;

        then

        reconsider cfx as Subset of Pa;

        

         A45: cgx in L by A41, A15, FUNCT_2: 5;

        then

        reconsider cgx as Subset of Pb;

        cfx <> {} by A44;

        hence a <> {} by A42, A43;

        let b be Subset of cR;

        assume b in C;

        then

        consider y be object such that

         A46: y in ( dom h) and

         A47: (h . y) = b by FUNCT_1:def 3;

        

         A48: (h . y) = ((f . y) \/ (g . y)) by A46, A15, LEXBFS:def 2;

        set cfy = (f . y), cgy = (g . y);

        

         A49: cfy in U by A46, A15, FUNCT_2: 5;

        then

        reconsider cfy as Subset of Pa;

        

         A50: cgy in L by A46, A15, FUNCT_2: 5;

        then

        reconsider cgy as Subset of Pb;

        assume

         A51: a <> b;

        then

         A52: cfx <> cfy by A7, A42, A47, A41, A46, A15, A9, FUNCT_1:def 4;

        

         A53: cgx <> cgy by A11, A51, A42, A47, A41, A46, A15, A13, FUNCT_1:def 4;

        assume a meets b;

        then (a /\ b) <> {} ;

        then

        consider z be object such that

         A54: z in (a /\ b) by XBOOLE_0:def 1;

        

         A55: z in a by A54, XBOOLE_0:def 4;

        

         A56: z in b by A54, XBOOLE_0:def 4;

        set cfz = (f . z), cgz = (g . z);

        per cases by A55, A56, A42, A47, A43, A48, XBOOLE_0:def 3;

          suppose z in cfx & z in cfy;

          then z in (cfx /\ cfy) by XBOOLE_0:def 4;

          then cfx meets cfy;

          hence contradiction by A44, A49, A52, EQREL_1:def 4;

        end;

          suppose

           A57: z in cfx & z in cgy;

          then

           A58: z in A by A5, A6, Th22;

          

           A59: z in (f . z) by A57, A5, A6, Th22, A8;

          

           A60: cfz in U by A57, A5, A6, Th22, FUNCT_2: 5;

          then

          reconsider cfz as Subset of Pa;

          z in (cfx /\ cfz) by A57, A59, XBOOLE_0:def 4;

          then cfz meets cfx;

          then cfz = cfx by A44, A60, EQREL_1:def 4;

          then

           A61: z = x by A7, A41, A58, A15, A9, FUNCT_1:def 4;

          

           A62: z in (g . z) by A57, A5, A6, Th22, A12;

          

           A63: cgz in L by A57, A5, A6, Th22, FUNCT_2: 5;

          then

          reconsider cgz as Subset of Pb;

          z in (cgz /\ cgy) by A57, A62, XBOOLE_0:def 4;

          then cgz meets cgy;

          then cgz = cgy by A50, A63, EQREL_1:def 4;

          hence contradiction by A61, A51, A42, A47, A11, A46, A58, A15, A13, FUNCT_1:def 4;

        end;

          suppose

           A64: z in cgx & z in cfy;

          then

           A65: z in A by A5, A6, Th22;

          

           A66: z in (f . z) by A64, A5, A6, Th22, A8;

          

           A67: cfz in U by A64, A5, A6, Th22, FUNCT_2: 5;

          then

          reconsider cfz as Subset of Pa;

          z in (cfy /\ cfz) by A64, A66, XBOOLE_0:def 4;

          then cfz meets cfy;

          then cfz = cfy by A49, A67, EQREL_1:def 4;

          then

           A68: z = y by A7, A46, A65, A15, A9, FUNCT_1:def 4;

          

           A69: z in (g . z) by A64, A5, A6, Th22, A12;

          

           A70: cgz in L by A64, A5, A6, Th22, FUNCT_2: 5;

          then

          reconsider cgz as Subset of Pb;

          z in (cgz /\ cgx) by A64, A69, XBOOLE_0:def 4;

          then cgz meets cgx;

          then cgz = cgx by A45, A70, EQREL_1:def 4;

          hence contradiction by A68, A51, A42, A47, A11, A41, A65, A15, A13, FUNCT_1:def 4;

        end;

          suppose z in cgx & z in cgy;

          then z in (cgx /\ cgy) by XBOOLE_0:def 4;

          then cgx meets cgy;

          hence contradiction by A45, A50, A53, EQREL_1:def 4;

        end;

      end;

      

       A71: for x be set st x in C holds x is Clique of R

      proof

        let c be set;

        assume c in C;

        then

        consider x be object such that

         A72: x in ( dom h) and

         A73: c = (h . x) by FUNCT_1:def 3;

        

         A74: c = ((f . x) \/ (g . x)) by A72, A73, A15, LEXBFS:def 2;

        set cf = (f . x), cg = (g . x);

        cf in U by A72, A15, FUNCT_2: 5;

        then

         A75: cf is Clique of Pa by Def11;

        then

         A76: cf is Clique of R by Th28;

        cg in L by A72, A15, FUNCT_2: 5;

        then

         A77: cg is Clique of Pb by Def11;

        then

         A78: cg is Clique of R by Th28;

        then

        reconsider c9 = c as Subset of R by A74, A76, XBOOLE_1: 8;

        now

          let a,b be Element of R such that

           A79: a in c9 and

           A80: b in c9 and

           A81: a <> b;

          

           A82: x in cf by A72, A15, A8;

          

           A83: x in cg by A72, A15, A12;

          reconsider x as Element of R by A72, A15, A9, A13;

          per cases by A79, A80, A74, XBOOLE_0:def 3;

            suppose a in (f . x) & b in (f . x);

            hence a <= b or b <= a by A76, A81, Th6;

          end;

            suppose

             A84: a in (f . x) & b in (g . x);

            then

             A85: x = a or x <= a by A82, A72, A15, A75, Th35;

            x = b or b <= x by A83, A84, A72, A15, A77, Th34;

            hence a <= b or b <= a by A81, A85, YELLOW_0:def 2;

          end;

            suppose

             A86: a in (g . x) & b in (f . x);

            then

             A87: x = a or a <= x by A83, A72, A15, A77, Th34;

            x = b or x <= b by A82, A86, A72, A15, A75, Th35;

            hence a <= b or b <= a by A81, A87, YELLOW_0:def 2;

          end;

            suppose a in (g . x) & b in (g . x);

            hence a <= b or b <= a by A78, A81, Th6;

          end;

        end;

        hence c is Clique of R by Th6;

      end;

      

       A88: h is one-to-one

      proof

        let x1,x2 be object such that

         A89: x1 in ( dom h) and

         A90: x2 in ( dom h) and

         A91: (h . x1) = (h . x2);

        

         A92: (h . x1) is Clique of R by A71, A89, FUNCT_1: 3;

        

         A93: (h . x1) = ((f . x1) \/ (g . x1)) by A15, A89, LEXBFS:def 2;

        x1 in (f . x1) & x1 in (g . x1) by A89, A15, A8, A12;

        then

         A94: x1 in (h . x1) by A93, XBOOLE_0:def 3;

        

         A95: (h . x2) = ((f . x2) \/ (g . x2)) by A15, A90, LEXBFS:def 2;

        x2 in (f . x2) & x2 in (g . x2) by A90, A15, A8, A12;

        then x2 in (h . x2) by A95, XBOOLE_0:def 3;

        hence x1 = x2 by A15, A89, A90, A91, A92, A94, Th15;

      end;

      reconsider C as Clique-partition of R by A16, A21, A40, A71, Def11, EQREL_1:def 4;

      take C;

      ( card C) = ( card h) by A88, PRE_POLY: 19

      .= ( card A) by A15, A9, A13, CARD_1: 62;

      hence ( card C) = ( stability# R) by A1;

    end;

    definition

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

      :: DILWORTH:def12

      attr P is StableSet-wise means

      : Def12: for x be set st x in P holds x is StableSet of R;

    end

    registration

      let R be RelStr;

      cluster StableSet-wise for a_partition of the carrier of R;

      existence

      proof

        set cR = the carrier of R;

        per cases ;

          suppose R is empty;

          then

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

          take S;

          let x be set;

          thus thesis;

        end;

          suppose

           A1: R is non empty;

          then

          reconsider RR = R as non empty RelStr;

          take S = ( SmallestPartition cR);

          let z be set;

          assume

           A2: z in S;

          S = the set of all {x} where x be Element of cR by A1, EQREL_1: 37;

          then

          consider x be Element of RR such that

           A3: z = {x} by A2;

          thus z is StableSet of R by A3;

        end;

      end;

    end

    definition

      let R be RelStr;

      mode Coloring of R is StableSet-wise a_partition of the carrier of R;

    end

    registration

      let R be empty RelStr;

      cluster -> StableSet-wise for a_partition of the carrier of R;

      coherence ;

    end

    theorem :: DILWORTH:50

    for R be finite RelStr, C be Coloring of R holds ( card C) >= ( clique# R)

    proof

      let R be finite RelStr, C be Coloring of R;

      assume

       A1: ( card C) < ( clique# R);

      consider A be Clique of R such that

       A2: ( card A) = ( clique# R) by Def4;

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

      then

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

      set cR = the carrier of R;

      per cases ;

        suppose R is empty;

        hence contradiction by A1;

      end;

        suppose

         A4: R is non empty;

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

        

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

           A6: x in A;

          reconsider x9 = x as Element of R by A6;

          cR is non empty by A4;

          then x9 in cR;

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

          then

          consider y be set such that

           A7: x in y and

           A8: y in C by TARSKI:def 4;

          take y;

          thus thesis by A6, A7, A8;

        end;

        consider f be Function of A, C such that

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

        consider x,y be object such that

         A10: x in A and

         A11: y in A and

         A12: x <> y and

         A13: (f . x) = (f . y) by A4, A3, FINSEQ_4: 65;

        (f . x) in C by A10, FUNCT_2: 5;

        then

         A14: (f . x) is StableSet of R by Def12;

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

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

        hence contradiction by A14, A10, A11, A12, Th15;

      end;

    end;

    begin

    ::$Notion-Name

    theorem :: DILWORTH:51

    

     Th51: for R be finite antisymmetric transitive RelStr holds ex C be Clique-partition of R st ( card C) = ( stability# R)

    proof

      defpred P[ Nat] means for P be finite antisymmetric transitive RelStr st ( card P) = $1 holds ex C be Clique-partition of P st ( card C) = ( stability# P);

      

       A1: for n be Nat st for k be Nat st k < n holds P[k] holds P[n]

      proof

        let n be Nat;

        assume

         A2: for k be Nat st k < n holds P[k];

        let P be finite antisymmetric transitive RelStr;

        assume

         A3: ( card P) = n;

        set wP = ( stability# P);

        per cases ;

          suppose

           A4: n = 0 ;

          then P is empty by A3;

          then

          reconsider C = {} as Clique-partition of P by EQREL_1: 45;

          take C;

          P is empty by A3, A4;

          hence ( card C) = ( stability# P);

        end;

          suppose

           A5: n > 0 ;

          per cases ;

            suppose ex A be StableSet of P st ( card A) = ( stability# P) & A <> ( minimals P) & A <> ( maximals P);

            then

            consider A be StableSet of P such that

             A6: ( card A) = ( stability# P) and

             A7: A <> ( minimals P) and

             A8: A <> ( maximals P);

            set aA = ( Upper A), bA = ( Lower A);

            set cP = the carrier of P, Pa = ( subrelstr aA), Pb = ( subrelstr bA);

            reconsider PP = P as finite non empty antisymmetric transitive RelStr by A5, A3;

            

             A9: aA = the carrier of Pa by YELLOW_0:def 15;

            

             A10: bA = the carrier of Pb by YELLOW_0:def 15;

             not ( minimals PP) c= aA by A7, Th40, Th26;

            then

            consider mi be object such that

             A11: mi in ( minimals P) and

             A12: not mi in aA;

             not ( maximals PP) c= bA by A8, Th41, Th27;

            then

            consider ma be object such that

             A13: ma in ( maximals P) and

             A14: not ma in bA;

            reconsider Pa as finite antisymmetric transitive RelStr;

            mi in cP by A11;

            then aA c< cP by A12;

            then ( card Pa) < ( card P) by A9, CARD_2: 48;

            then

            consider Ca be Clique-partition of Pa such that

             A15: ( card Ca) = ( stability# Pa) by A2, A3;

            

             A16: ( stability# Pa) = wP by A6, Th45, XBOOLE_1: 7;

            reconsider Pb as finite antisymmetric transitive RelStr;

            ma in cP by A13;

            then bA c< cP by A14;

            then ( card Pb) < ( card P) by A10, CARD_2: 48;

            then

            consider L be Clique-partition of Pb such that

             A17: ( card L) = ( stability# Pb) by A2, A3;

            ( stability# Pb) = wP by A6, Th45, XBOOLE_1: 7;

            then

            consider C be Clique-partition of P such that

             A18: ( card C) = ( stability# PP) by A6, A15, A16, A17, Th49;

            take C;

            thus ( card C) = ( stability# P) by A18;

          end;

            suppose

             A19: for A be StableSet of P st ( card A) = ( stability# P) holds A = ( minimals P) or A = ( maximals P);

            consider S be StableSet of P such that

             A20: ( card S) = ( stability# P) by Def6;

            reconsider PP = P as finite non empty antisymmetric transitive RelStr by A5, A3;

            set cR = the carrier of PP;

            set a = the Element of ( minimals P);

            

             A21: a in ( minimals PP);

            then

            reconsider a as Element of PP;

            consider b be Element of PP such that

             A22: b is_maximal_in ( [#] PP) and

             A23: a = b or a < b by Th38;

            

             A24: b in ( maximals P) by A22, Def10;

            set cP = the carrier of P;

            set Cn = {a, b};

            set cP9 = (cP \ Cn);

            

             A25: cP = (cP9 \/ Cn) by XBOOLE_1: 45;

            

             A26: cP9 misses {a, b} by XBOOLE_1: 79;

            then

             A27: (cP \ cP9) = {a, b} by A25, XBOOLE_1: 88;

            reconsider cP9 as Subset of cR;

            set P9 = ( subrelstr cP9);

            

             A28: cP9 = the carrier of P9 by YELLOW_0:def 15;

            

             A29: ( card cP9) = ( card P9) by YELLOW_0:def 15;

            ( card cP9) = (( card cP) - ( card {a, b})) by CARD_2: 44;

            then

            consider C be Clique-partition of P9 such that

             A30: ( card C) = ( stability# P9) by A2, A3, A29, XREAL_1: 44;

            

             A31: not {a, b} in C

            proof

              assume

               A32: {a, b} in C;

              a in {a, b} by TARSKI:def 2;

              hence contradiction by A26, A28, A32, ZFMISC_1: 49;

            end;

            set wP = ( stability# PP);

            set wP1 = (wP - 1);

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

            then (( 0 + 1) - 1) <= (wP - 1) by XREAL_1: 9;

            then wP1 in NAT by INT_1: 3;

            then

            reconsider wP1 as Nat;

            set S9 = (S /\ cP9);

            (S /\ cP) = S by XBOOLE_1: 28;

            then

             A33: S9 = (S \ {a, b}) by XBOOLE_1: 49;

            

             A34: {a, b} = ( {a} \/ {b}) by ENUMSET1: 1;

            reconsider S9 as StableSet of P9 by Th31;

            

             A35: ( card S9) = wP1

            proof

              per cases by A19, A20;

                suppose

                 A36: S = ( minimals P);

                S9 = (S \ {a})

                proof

                  per cases ;

                    suppose a = b;

                    hence S9 = (S \ {a}) by A33, ENUMSET1: 29;

                  end;

                    suppose

                     A37: a <> b;

                    now

                      assume b in ( minimals PP);

                      then b is_minimal_in ( [#] PP) by Def9;

                      hence contradiction by A37, A23, WAYBEL_4: 56;

                    end;

                    hence S9 = (S \ {a}) by A33, A34, A36, Th1;

                  end;

                end;

                

                hence ( card S9) = (( card S) - ( card {a})) by A36, EULER_1: 4

                .= wP1 by A20, CARD_1: 30;

              end;

                suppose

                 A38: S = ( maximals PP);

                

                 A39: S9 = (S \ {b})

                proof

                  per cases ;

                    suppose a = b;

                    hence S9 = (S \ {b}) by A33, ENUMSET1: 29;

                  end;

                    suppose

                     A40: a <> b;

                    now

                      assume a in ( maximals PP);

                      then a is_maximal_in ( [#] PP) by Def10;

                      hence contradiction by A40, A23, WAYBEL_4: 55;

                    end;

                    hence S9 = (S \ {b}) by A33, A34, A38, Th1;

                  end;

                end;

                b in S by A38, A22, Def10;

                

                hence ( card S9) = (( card S) - ( card {b})) by A39, EULER_1: 4

                .= wP1 by A20, CARD_1: 30;

              end;

            end;

            for T be StableSet of P9 holds ( card T) <= ( card S9)

            proof

              let T be StableSet of P9;

              assume ( card T) > ( card S9);

              then ( card T) >= (( card S9) + 1) by NAT_1: 13;

              then

              consider V be StableSet of P9 such that

               A41: ( card V) = (( card S9) + 1) by Th17;

              V is StableSet of P by Th30;

              then V = ( minimals P) or V = ( maximals P) by A19, A41, A35;

              hence contradiction by A21, A24, A28, A26, ZFMISC_1: 49;

            end;

            

            then

             A42: (( stability# P9) + 1) = ((wP - 1) + 1) by A35, Def6

            .= wP;

            set CC = (C \/ { {a, b}});

            cP9 <> cP by A27, XBOOLE_1: 37;

            then

             A43: cP9 c< cP;

            now

              let x be set;

              assume

               A44: x in CC;

              per cases by A44, XBOOLE_0:def 3;

                suppose x in C;

                then x is Clique of P9 by Def11;

                hence x is Clique of P by Th28;

              end;

                suppose x in { {a, b}};

                then

                 A45: x = {a, b} by TARSKI:def 1;

                per cases ;

                  suppose a = b;

                  then x = {a} by A45, ENUMSET1: 29;

                  hence x is Clique of P;

                end;

                  suppose a <> b;

                  then a <= b by A23;

                  hence x is Clique of P by A45, Th8;

                end;

              end;

            end;

            then

            reconsider CC as Clique-partition of P by A27, A28, Th4, Def11, A43;

            take CC;

            thus ( card CC) = ( stability# P) by A30, A42, A31, CARD_2: 41;

          end;

        end;

      end;

      

       A46: for n be Nat holds P[n] from NAT_1:sch 4( A1);

      let R be finite antisymmetric transitive RelStr;

      ( card R) = ( card R);

      hence thesis by A46;

    end;

    definition

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

      :: DILWORTH:def13

      attr C is strong-chain means for S be finite non empty Subset of R holds ex P be Clique-partition of ( subrelstr S) st ( card P) <= ( stability# R) & ex c be set st c in P & (S /\ C) c= c & for d be set st d in P & d <> c holds (C /\ d) = {} ;

    end

    registration

      let R be with_finite_stability# non empty RelStr;

      cluster strong-chain -> clique for Subset of R;

      coherence

      proof

        let C be Subset of R;

        assume

         A1: C is strong-chain;

        now

          let a,b be Element of R such that

           A2: a in C and

           A3: b in C and

           A4: a <> b;

          set S = {a, b};

          reconsider S as finite non empty Subset of R;

          consider P be Clique-partition of ( subrelstr S) such that ( card P) <= ( stability# R) and

           A5: ex c be set st c in P & (S /\ C) c= c & for d be set st d in P & d <> c holds (C /\ d) = {} by A1;

          consider c be set such that

           A6: c in P and

           A7: (S /\ C) c= c and for d be set st d in P & d <> c holds (C /\ d) = {} by A5;

          c is Clique of ( subrelstr S) by A6, Def11;

          then

           A8: c is Clique of R by Th28;

          a in S & b in S by TARSKI:def 2;

          then a in (S /\ C) & b in (S /\ C) by A2, A3, XBOOLE_0:def 4;

          hence a <= b or b <= a by A7, A8, A4, Th6;

        end;

        hence C is clique by Th6;

      end;

    end

    registration

      let R be with_finite_stability# antisymmetric transitive non empty RelStr;

      cluster 1 -element -> strong-chain for Subset of R;

      coherence

      proof

        let C be Subset of R;

        assume C is 1 -element;

        then

        consider x be object such that

         A1: C = {x} by ZFMISC_1: 131;

        let S be finite non empty Subset of R;

        consider P be Clique-partition of ( subrelstr S) such that

         A2: ( card P) = ( stability# ( subrelstr S)) by Th51;

        

         A3: S = the carrier of ( subrelstr S) by YELLOW_0:def 15;

        take P;

        thus ( card P) <= ( stability# R) by A2, Th44;

        per cases ;

          suppose x in S;

          then x in ( union P) by A3, EQREL_1:def 4;

          then

          consider c be set such that

           A4: x in c and

           A5: c in P by TARSKI:def 4;

          take c;

          thus c in P by A5;

          thus (S /\ C) c= c

          proof

            let a be object;

            assume a in (S /\ C);

            then a in C by XBOOLE_0:def 4;

            hence thesis by A4, A1, TARSKI:def 1;

          end;

          let d be set such that

           A6: d in P and

           A7: d <> c;

          assume (C /\ d) <> {} ;

          then

          consider a be object such that

           A8: a in (C /\ d) by XBOOLE_0:def 1;

          reconsider d, c as Subset of S by A6, A5, YELLOW_0:def 15;

          a in C by A8, XBOOLE_0:def 4;

          then a = x by A1, TARSKI:def 1;

          then x in d by A8, XBOOLE_0:def 4;

          then x in (d /\ c) by A4, XBOOLE_0:def 4;

          then d meets c;

          hence contradiction by A6, A5, A7, EQREL_1:def 4;

        end;

          suppose

           A9: not x in S;

          set c = the Element of P;

          take c;

          thus c in P;

          C misses S by A9, A1, ZFMISC_1: 50;

          then (S /\ C) = {} ;

          hence (S /\ C) c= c;

          let d be set such that

           A10: d in P and d <> c;

           not x in d by A9, A3, A10;

          then C misses d by A1, ZFMISC_1: 50;

          hence (C /\ d) = {} ;

        end;

      end;

    end

    theorem :: DILWORTH:52

    

     Th52: for R be with_finite_stability# non empty antisymmetric transitive RelStr holds ex S be non empty Subset of R st S is strong-chain & not ex D be Subset of R st D is strong-chain & S c< D

    proof

      let R be with_finite_stability# non empty antisymmetric transitive RelStr;

      set E = { C where C be Subset of R : C is strong-chain };

      set x = the Element of R;

      

       A1: {x} in E;

      now

        let Z be set such that

         A2: Z c= E and

         A3: Z is c=-linear;

        set Y = ( union Z);

        take Y;

        now

          let B be set;

          assume B in Z;

          then B in E by A2;

          then ex C be Subset of R st C = B & C is strong-chain;

          hence B c= the carrier of R;

        end;

        then

        reconsider Y9 = Y as Subset of R by ZFMISC_1: 76;

        Y9 is strong-chain

        proof

          let S be finite non empty Subset of R;

          set F = (S /\ Y);

          per cases ;

            suppose

             A4: F is empty;

            consider p be Clique-partition of ( subrelstr S) such that

             A5: ( card p) = ( stability# ( subrelstr S)) by Th51;

            take p;

            thus ( card p) <= ( stability# R) by Th44, A5;

            set c = the Element of p;

            take c;

            thus c in p;

            thus (S /\ Y9) c= c by A4;

            let d be set such that

             A6: d in p and d <> c;

            d c= the carrier of ( subrelstr S) by A6;

            then d c= S by YELLOW_0:def 15;

            hence (Y9 /\ d) = {} by A4, XBOOLE_1: 3, XBOOLE_1: 26;

          end;

            suppose

             A7: F is non empty;

            then

             A8: Z is non empty by ZFMISC_1: 2;

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

            

             A9: for x be object st x in F holds ex y be object st y in Z & P[x, y]

            proof

              let x be object;

              assume

               A10: x in F;

              then x in Y by XBOOLE_0:def 4;

              then

              consider y be set such that

               A11: x in y and

               A12: y in Z by TARSKI:def 4;

              take y;

              thus thesis by A12, A10, A11;

            end;

            consider f be Function of F, Z such that

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

            set rf = ( rng f);

            rf c= Z & Z is c=-linear implies rf is c=-linear;

            then

            consider m be set such that

             A14: m in rf and

             A15: for C be set st C in rf holds C c= m by A3, A7, A8, FINSET_1: 12, RELAT_1:def 19;

            rf c= Z by RELAT_1:def 19;

            then m in Z by A14;

            then m in E by A2;

            then

            consider C be Subset of R such that

             A16: m = C and

             A17: C is strong-chain;

            

             A18: F c= C

            proof

              let x be object;

              assume

               A19: x in F;

              then P[x, (f . x)] by A13;

              then

               A20: x in (f . x);

              (f . x) c= C by A16, A15, A19, A8, FUNCT_2: 4;

              hence x in C by A20;

            end;

            consider p be Clique-partition of ( subrelstr S) such that

             A21: ( card p) <= ( stability# R) and

             A22: ex c be set st c in p & (S /\ C) c= c & for d be set st d in p & d <> c holds (C /\ d) = {} by A17;

            take p;

            thus ( card p) <= ( stability# R) by A21;

            consider c be set such that

             A23: c in p and

             A24: (S /\ C) c= c and

             A25: for d be set st d in p & d <> c holds (C /\ d) = {} by A22;

            take c;

            thus c in p by A23;

            thus (S /\ Y9) c= c

            proof

              let x be object;

              assume x in (S /\ Y9);

              then x in S & x in C by A18, XBOOLE_0:def 4;

              then x in (S /\ C) by XBOOLE_0:def 4;

              hence x in c by A24;

            end;

            let d be set such that

             A26: d in p and

             A27: d <> c;

            assume (Y9 /\ d) <> {} ;

            then

            consider x be object such that

             A28: x in (Y9 /\ d) by XBOOLE_0:def 1;

            

             A29: x in Y9 by A28, XBOOLE_0:def 4;

            

             A30: x in d by A28, XBOOLE_0:def 4;

            d is Subset of S by A26, YELLOW_0:def 15;

            then x in F by A30, A29, XBOOLE_0:def 4;

            then x in (C /\ d) by A30, A18, XBOOLE_0:def 4;

            hence contradiction by A26, A27, A25;

          end;

        end;

        hence Y in E;

        let X1 be set such that

         A31: X1 in Z;

        thus X1 c= Y by A31, ZFMISC_1: 74;

      end;

      then

      consider Y be set such that

       A32: Y in E and

       A33: for Z be set st Z in E & Z <> Y holds not Y c= Z by A1, ORDERS_1: 65;

      consider C be Subset of R such that

       A34: Y = C and

       A35: C is strong-chain by A32;

      reconsider S = C as non empty Subset of R by A34, A1, A33, XBOOLE_1: 2;

      take S;

      thus S is strong-chain by A35;

      let D be Subset of R such that

       A36: D is strong-chain and

       A37: S c< D;

      

       A38: D in E by A36;

      D <> S & S c= D by A37;

      hence contradiction by A34, A38, A33;

    end;

    theorem :: DILWORTH:53

    for R be with_finite_stability# antisymmetric transitive RelStr holds ex C be Clique-partition of R st ( card C) = ( stability# R)

    proof

      let R be with_finite_stability# antisymmetric transitive RelStr;

      per cases ;

        suppose R is finite;

        hence thesis by Th51;

      end;

        suppose

         A1: R is infinite;

        defpred P[ Nat] means for P be with_finite_stability# non empty antisymmetric transitive RelStr st ( stability# P) = $1 holds ex C be Clique-partition of P st ( card C) = ( stability# P);

        

         A2: P[ 0 ];

        

         A3: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A4: P[k];

          let P be with_finite_stability# non empty antisymmetric transitive RelStr;

          assume

           A5: ( stability# P) = (k + 1);

          consider C be non empty Subset of P such that

           A6: C is strong-chain and

           A7: not ex D be Subset of P st D is strong-chain & C c< D by Th52;

          set cP = the carrier of P;

          per cases ;

            suppose

             A8: C = cP;

            for x be set st x in {C} holds x is Clique of P by A6, TARSKI:def 1;

            then

            reconsider Cp = {C} as Clique-partition of P by Def11, A8, EQREL_1: 39;

            take Cp;

            

             A9: cP = ( [#] P);

            

            thus ( card Cp) = 1 by CARD_1: 30

            .= ( stability# P) by A9, A6, A8, Th20;

          end;

            suppose C <> cP;

            then

             A10: C c< cP;

            set cP9 = (cP \ C);

            

             A11: (cP \ cP9) = (cP /\ C) by XBOOLE_1: 48

            .= C by XBOOLE_1: 28;

            reconsider cP9 as Subset of P;

            cP9 <> {} by A10, XBOOLE_1: 105;

            then

            reconsider P9 = ( subrelstr cP9) as with_finite_stability# non empty antisymmetric transitive RelStr;

            

             A12: cP9 = the carrier of P9 by YELLOW_0:def 15;

            

             A13: ( stability# P9) <= (k + 1) by A5, Th44;

            

             A14: ( stability# P9) <> (k + 1)

            proof

              assume

               A15: ( stability# P9) = (k + 1);

              consider A be finite StableSet of P9 such that

               A16: ( card A) = ( stability# P9) by Def6;

              reconsider A9 = A as finite non empty StableSet of P by A16, Th30;

              defpred R[ set, set, set] means for c be set st c in $2 holds not ($1 /\ $3) c= c or ex d be set st d in $2 & d <> c & ($3 /\ d) <> {} ;

              defpred Q[ finite Subset of P, set] means for p be Clique-partition of ( subrelstr $1) st ( card p) <= ( stability# P) holds R[$1, p, $2];

              defpred P[ object, object] means ex S be finite non empty Subset of P st $2 = S & $1 in S & Q[S, (C \/ {$1})];

              

               A17: for x be object st x in A holds ex y be object st P[x, y]

              proof

                let a be object;

                assume

                 A18: a in A;

                A c= cP by A12, XBOOLE_1: 1;

                then {a} c= cP by A18, ZFMISC_1: 31;

                then

                reconsider Ca = (C \/ {a}) as Subset of P by XBOOLE_1: 8;

                now

                  assume

                   A19: Ca is strong-chain;

                  a in {a} by TARSKI:def 1;

                  then

                   A20: a in Ca by XBOOLE_0:def 3;

                  

                   A21: not a in C by A12, A18, XBOOLE_0:def 5;

                  C c= Ca by XBOOLE_1: 7;

                  then C c< Ca by A20, A21;

                  hence contradiction by A19, A7;

                end;

                then

                consider S be finite non empty Subset of P such that

                 A22: Q[S, Ca];

                take S;

                take S;

                thus S = S;

                now

                  assume

                   A23: not a in S;

                  

                   A24: (S /\ C) c= (S /\ Ca)

                  proof

                    let x be object;

                    assume x in (S /\ C);

                    then x in S & x in C by XBOOLE_0:def 4;

                    then x in S & x in Ca by XBOOLE_0:def 3;

                    hence x in (S /\ Ca) by XBOOLE_0:def 4;

                  end;

                  (S /\ Ca) c= (S /\ C)

                  proof

                    let x be object;

                    assume

                     A25: x in (S /\ Ca);

                    then

                     A26: x in S by XBOOLE_0:def 4;

                    x in Ca by A25, XBOOLE_0:def 4;

                    then x in C or x in {a} by XBOOLE_0:def 3;

                    hence x in (S /\ C) by A26, A23, TARSKI:def 1, XBOOLE_0:def 4;

                  end;

                  then

                   A27: (S /\ C) = (S /\ Ca) by A24;

                  consider p be Clique-partition of ( subrelstr S) such that

                   A28: ( card p) <= ( stability# P) and

                   A29: not R[S, p, C] by A6;

                  consider c be set such that

                   A30: c in p and

                   A31: (S /\ C) c= c and

                   A32: for d be set st d in p & d <> c holds (C /\ d) = {} by A29;

                  for d be set st d in p & d <> c holds (Ca /\ d) = {}

                  proof

                    let d be set such that

                     A33: d in p and

                     A34: d <> c;

                    now

                      assume (Ca /\ d) <> {} ;

                      then

                      consider x be object such that

                       A35: x in (Ca /\ d) by XBOOLE_0:def 1;

                      

                       A36: x in Ca by A35, XBOOLE_0:def 4;

                      

                       A37: x in d by A35, XBOOLE_0:def 4;

                      per cases by A36, XBOOLE_0:def 3;

                        suppose x in C;

                        then x in (C /\ d) by A37, XBOOLE_0:def 4;

                        hence contradiction by A33, A34, A32;

                      end;

                        suppose x in {a};

                        then x = a by TARSKI:def 1;

                        then a in the carrier of ( subrelstr S) by A37, A33;

                        hence contradiction by A23, YELLOW_0:def 15;

                      end;

                    end;

                    hence (Ca /\ d) = {} ;

                  end;

                  hence contradiction by A30, A31, A28, A27, A22;

                end;

                hence a in S;

                thus thesis by A22;

              end;

              consider f be Function such that

               A38: ( dom f) = A and

               A39: for x be object st x in A holds P[x, (f . x)] from CLASSES1:sch 1( A17);

              

               A40: ( rng f) is finite by A38, FINSET_1: 8;

              set SS = ( union ( rng f));

              

               A41: for x be set st x in ( rng f) holds x is finite

              proof

                let x be set;

                assume x in ( rng f);

                then

                consider a be object such that

                 A42: a in ( dom f) and

                 A43: x = (f . a) by FUNCT_1:def 3;

                 P[a, (f . a)] by A38, A42, A39;

                then

                consider S be finite non empty Subset of P such that

                 A44: (f . a) = S and a in (f . a) & Q[S, (C \/ {a})];

                thus x is finite by A44, A43;

              end;

              

               A45: SS c= cP

              proof

                let x be object;

                assume x in SS;

                then

                consider y be set such that

                 A46: x in y and

                 A47: y in ( rng f) by TARSKI:def 4;

                consider a be object such that

                 A48: a in ( dom f) and

                 A49: y = (f . a) by A47, FUNCT_1:def 3;

                 P[a, (f . a)] by A38, A48, A39;

                then

                consider S be finite non empty Subset of P such that

                 A50: (f . a) = S and a in (f . a) & Q[S, (C \/ {a})];

                thus x in cP by A46, A49, A50;

              end;

              

               A51: A9 c= SS

              proof

                let x be object;

                assume

                 A52: x in A9;

                then P[x, (f . x)] by A39;

                then

                consider S be finite non empty Subset of P such that (f . x) = S and

                 A53: x in (f . x) and Q[S, (C \/ {x})];

                (f . x) in ( rng f) by A52, A38, FUNCT_1: 3;

                hence x in SS by A53, TARSKI:def 4;

              end;

              then

              reconsider SS as finite non empty Subset of P by A41, A40, A45, FINSET_1: 7;

              set SSp = ( subrelstr SS);

              

               A54: SS = the carrier of SSp by YELLOW_0:def 15;

              consider p be Clique-partition of SSp such that

               A55: ( card p) <= ( stability# P) and

               A56: not R[SS, p, C] by A6;

              consider c be set such that

               A57: c in p and

               A58: (SS /\ C) c= c and

               A59: for d be set st d in p & d <> c holds (C /\ d) = {} by A56;

              reconsider c as Element of p by A57;

              A9 = (A9 /\ SS) by A51, XBOOLE_1: 28;

              then

              reconsider A = A9 as finite non empty StableSet of SSp by Th31;

              

               A60: ( stability# SSp) >= ( card A) by Def6;

              ( card p) >= ( stability# SSp) by Th46;

              then ( card p) >= ( card A) by A60, XXREAL_0: 2;

              then

              consider a be Element of A such that

               A61: (c /\ A) = {a} by Th48, A55, A16, A15, A5, XXREAL_0: 1;

              a in (c /\ A) by A61, TARSKI:def 1;

              then

               A62: a in c by XBOOLE_0:def 4;

               P[a, (f . a)] by A39;

              then

              consider S be finite non empty Subset of P such that

               A63: (f . a) = S and

               A64: a in (f . a) and

               A65: Q[S, (C \/ {a})];

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

              defpred P[ set] means $1 meets S;

              set Sp = { F(e) where e be Element of p : P[e] };

              

               A66: S c= SS

              proof

                let x be object;

                assume

                 A67: x in S;

                S in ( rng f) by A63, A38, FUNCT_1: 3;

                hence x in SS by A67, TARSKI:def 4;

              end;

              then

              reconsider Sp as a_partition of S by A54, PUA2MSS1: 11;

              for x be set st x in Sp holds x is Clique of ( subrelstr S)

              proof

                let x be set;

                assume x in Sp;

                then

                consider e be Element of p such that

                 A68: x = (e /\ S) and e meets S;

                e is Clique of SSp by Def11;

                then e is Clique of P by Th28;

                hence x is Clique of ( subrelstr S) by A68, Th29;

              end;

              then

              reconsider Sp as Clique-partition of ( subrelstr S) by Def11, YELLOW_0:def 15;

              

               A69: Sp = { F(e) where e be Element of p : P[e] };

              

               A70: ( card Sp) <= ( card p) from FraenkelFinCard1( A69);

              set cc = (c /\ S);

              c meets S by A62, A63, A64, XBOOLE_0: 3;

              then

               A71: cc in Sp;

              (S /\ (C \/ {a})) c= cc

              proof

                let x be object;

                assume

                 A72: x in (S /\ (C \/ {a}));

                then

                 A73: x in S by XBOOLE_0:def 4;

                

                 A74: x in (C \/ {a}) by A72, XBOOLE_0:def 4;

                per cases by A74, XBOOLE_0:def 3;

                  suppose x in C;

                  then x in (SS /\ C) by A73, A66, XBOOLE_0:def 4;

                  hence x in cc by A73, A58, XBOOLE_0:def 4;

                end;

                  suppose x in {a};

                  then x = a by TARSKI:def 1;

                  hence x in cc by A62, A63, A64, XBOOLE_0:def 4;

                end;

              end;

              then

              consider d be set such that

               A75: d in Sp and

               A76: d <> cc and

               A77: ((C \/ {a}) /\ d) <> {} by A71, A70, A55, A65, XXREAL_0: 2;

              consider dd be Element of p such that

               A78: d = (dd /\ S) and dd meets S by A75;

              (C /\ dd) = {} by A78, A76, A59;

              

              then

               A79: (C /\ d) = ( {} /\ S) by A78, XBOOLE_1: 16

              .= {} ;

              ((C /\ d) \/ ( {a} /\ d)) <> {} by A77, XBOOLE_1: 23;

              then

              consider x be object such that

               A80: x in ( {a} /\ d) by A79, XBOOLE_0:def 1;

              x in {a} & x in d by A80, XBOOLE_0:def 4;

              then a in d by TARSKI:def 1;

              then a in dd by A78, XBOOLE_0:def 4;

              then c meets dd by A62, XBOOLE_0: 3;

              hence contradiction by A78, A76, EQREL_1:def 4;

            end;

            then ( stability# P9) < (k + 1) by A13, XXREAL_0: 1;

            then

             A81: ( stability# P9) <= k by NAT_1: 13;

            consider A be finite StableSet of P such that

             A82: ( card A) = ( stability# P) by Def6;

            

             A83: ( stability# P9) = k

            proof

              per cases ;

                suppose

                 A84: (A /\ C) = {} ;

                A c= cP9

                proof

                  let x be object;

                  assume

                   A85: x in A;

                  then not x in C by A84, XBOOLE_0:def 4;

                  hence x in cP9 by A85, XBOOLE_0:def 5;

                end;

                hence thesis by A5, A14, A82, Th45;

              end;

                suppose (A /\ C) <> {} ;

                then

                consider x be object such that

                 A86: x in (A /\ C) by XBOOLE_0:def 1;

                

                 A87: x in A by A86, XBOOLE_0:def 4;

                

                 A88: x in C by A86, XBOOLE_0:def 4;

                set A9 = (A \ {x});

                 {x} c= A by A87, ZFMISC_1: 31;

                then

                 A89: A = (A9 \/ {x}) by XBOOLE_1: 45;

                x in {x} by TARSKI:def 1;

                then not x in A9 by XBOOLE_0:def 5;

                then

                 A90: ( card A) = (( card A9) + 1) by A89, CARD_2: 41;

                

                 A91: A9 c= A by XBOOLE_1: 36;

                A9 c= cP9

                proof

                  let xx be object;

                  assume

                   A92: xx in A9;

                  then

                   A93: xx in A by XBOOLE_0:def 5;

                   not xx in {x} by A92, XBOOLE_0:def 5;

                  then xx <> x by TARSKI:def 1;

                  then not xx in C by A87, A88, A93, A6, Th15;

                  hence xx in cP9 by A92, XBOOLE_0:def 5;

                end;

                then

                 A94: A9 c= (A /\ cP9) by A91, XBOOLE_1: 19;

                (A /\ cP9) c= A9

                proof

                  let xx be object;

                  assume

                   A95: xx in (A /\ cP9);

                  then

                   A96: xx in A by XBOOLE_0:def 4;

                  xx in cP9 by A95, XBOOLE_0:def 4;

                  then x <> xx by A88, XBOOLE_0:def 5;

                  then not xx in {x} by TARSKI:def 1;

                  hence xx in A9 by A96, XBOOLE_0:def 5;

                end;

                then A9 = (A /\ cP9) by A94;

                then

                reconsider A9 as StableSet of P9 by Th31;

                ( stability# P9) >= ( card A9) by Def6;

                hence thesis by A90, A82, A5, A81, XXREAL_0: 1;

              end;

            end;

            then

            consider Cp9 be Clique-partition of P9 such that

             A97: ( card Cp9) = ( stability# P9) by A4;

            set Cp = (Cp9 \/ {(cP \ cP9)});

            

             A98: Cp9 is finite by A97;

            cP9 <> cP by A11, XBOOLE_1: 37;

            then

             A99: cP9 c< cP;

            then

            reconsider Cp as a_partition of cP by A12, Th4;

            now

              let x be set;

              assume

               A100: x in Cp;

              per cases by A100, XBOOLE_0:def 3;

                suppose x in Cp9;

                then x is Clique of P9 by Def11;

                hence x is Clique of P by Th28;

              end;

                suppose x in {(cP \ cP9)};

                hence x is Clique of P by A6, A11, TARSKI:def 1;

              end;

            end;

            then

            reconsider Cp as Clique-partition of P by Def11;

            take Cp;

             not (cP \ cP9) in Cp9

            proof

              assume not thesis;

              then cP c= (cP9 \/ cP9) by A12, XBOOLE_1: 44;

              hence contradiction by A99, XBOOLE_1: 60;

            end;

            hence ( card Cp) = ( stability# P) by A5, A83, A97, A98, CARD_2: 41;

          end;

        end;

        for k be Nat holds P[k] from NAT_1:sch 2( A2, A3);

        hence thesis by A1;

      end;

    end;

    theorem :: DILWORTH:54

    for R be with_finite_clique# antisymmetric transitive RelStr holds ex A be Coloring of R st ( card A) = ( clique# R)

    proof

      let R be with_finite_clique# antisymmetric transitive RelStr;

      defpred P[ Nat] means for P be with_finite_clique# antisymmetric transitive RelStr st ( clique# P) = $1 holds ex A be Coloring of P st ( card A) = ( clique# P);

      

       A1: P[ 0 ]

      proof

        let P be with_finite_clique# antisymmetric transitive RelStr;

        assume

         A2: ( clique# P) = 0 ;

        then P is empty;

        then

        reconsider C = {} as Coloring of P by EQREL_1: 45;

        take C;

        thus ( card C) = ( clique# P) by A2;

      end;

      

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

      proof

        let n be Nat;

        assume

         A4: P[n];

        let P be with_finite_clique# antisymmetric transitive RelStr;

        assume

         A5: ( clique# P) = (n + 1);

        then

         A6: P is non empty;

        reconsider PP = P as with_finite_clique# non empty antisymmetric transitive RelStr by A5;

        set M = ( maximals PP);

        set cP = the carrier of P;

        set cPM = (cP \ M);

        reconsider cPM as Subset of P;

        set PM = ( subrelstr cPM);

        

         A7: cPM = the carrier of PM by YELLOW_0:def 15;

        reconsider PM as with_finite_clique# antisymmetric transitive RelStr;

        consider Ca be finite Clique of PM such that

         A8: ( card Ca) = ( clique# PM) by Def4;

        

         A9: Ca is Clique of P by Th28;

        consider C be finite Clique of P such that

         A10: ( card C) = (n + 1) by A5, Def4;

        

         A11: C <> {} by A10;

        set cC = (C /\ cPM);

        reconsider cC as finite Clique of PM by Th29;

        consider m be Element of P such that

         A12: m in C and

         A13: m is_maximal_wrt (C,the InternalRel of P) by A6, A11, BAGORDER: 6;

        

         A14: m is_maximal_in C by A13, WAYBEL_4:def 24;

        

         A15: (C /\ M) = {m}

        proof

          thus (C /\ M) c= {m}

          proof

            let a be object;

            assume

             A16: a in (C /\ M);

            then

             A17: a in C by XBOOLE_0:def 4;

            

             A18: a in M by A16, XBOOLE_0:def 4;

            reconsider a9 = a as Element of P by A16;

            

             A19: a9 is_maximal_in ( [#] P) by A18, Def10;

            now

              assume

               A20: a <> m;

               not m < a9 by A17, A14, WAYBEL_4: 55;

              then not m <= a9 by A20;

              then a9 <= m by A12, A17, A20, Th6;

              then a9 < m by A20;

              hence contradiction by A19, A12, WAYBEL_4: 55;

            end;

            hence a in {m} by TARSKI:def 1;

          end;

          thus {m} c= (C /\ M)

          proof

            let a be object;

            assume a in {m};

            then

             A21: a = m by TARSKI:def 1;

            now

              assume

               A22: not a in M;

              consider y be Element of P such that

               A23: y is_maximal_in ( [#] P) and

               A24: m = y or m < y by A6, Th38;

              set Cm = (C \/ {y});

              now

                per cases ;

                  suppose m = y;

                  hence Cm is finite Clique of P by A12, ZFMISC_1: 40;

                end;

                  suppose m <> y;

                  then m <= y by A24;

                  hence Cm is finite Clique of P by A14, Th11;

                end;

              end;

              then

              reconsider Cm as finite Clique of P;

               not y in C by A21, A22, A23, Def10, A24, A14, WAYBEL_4: 55;

              then ( card Cm) = (( card C) + 1) by CARD_2: 41;

              then ((n + 1) + 1) <= ((n + 1) + 0 ) by A10, A5, Def4;

              hence contradiction by XREAL_1: 6;

            end;

            hence a in (C /\ M) by A21, A12, XBOOLE_0:def 4;

          end;

        end;

        

         A25: cC = ((C /\ cP) \ (C /\ M)) by XBOOLE_1: 50;

        (C /\ cP) = C by XBOOLE_1: 28;

        

        then

         A26: ( card cC) = (( card C) - ( card {m})) by A12, A15, A25, EULER_1: 4

        .= ((n + 1) - 1) by A10, CARD_1: 30

        .= n;

        

         A27: ( clique# PM) >= ( card cC) by Def4;

        

         A28: ( clique# PM) <= ( clique# P) by Th42;

        now

          assume

           A29: ( clique# PM) = (n + 1);

          then

           A30: Ca <> {} by A8;

          

           A31: PM is non empty by A29;

          then

          consider x be Element of PM such that

           A32: x in Ca and

           A33: x is_maximal_wrt (Ca,the InternalRel of PM) by A30, BAGORDER: 6;

          

           A34: x is_maximal_in Ca by A33, WAYBEL_4:def 24;

          reconsider x9 = x as Element of P by A31, YELLOW_0: 58;

          consider y be Element of P such that

           A35: y is_maximal_in ( [#] P) and

           A36: x9 = y or x9 < y by Th38;

          set Cb = (Ca \/ {y});

          now

            per cases ;

              suppose x9 = y;

              hence Cb is finite Clique of P by A32, A9, ZFMISC_1: 40;

            end;

              suppose x9 <> y;

              then x9 <= y by A36;

              hence Cb is finite Clique of P by A34, Th32, A9, Th11;

            end;

          end;

          then

          reconsider Cb as finite Clique of P;

          y in M by A35, Def10;

          then not y in Ca by A7, XBOOLE_0:def 5;

          then

           A37: ( card Cb) = ((n + 1) + 1) by A8, A29, CARD_2: 41;

          ( card Cb) <= (n + 1) by A5, Def4;

          then (n + 1) <= (n + 0 ) by A37, XREAL_1: 6;

          hence contradiction by XREAL_1: 6;

        end;

        then ( clique# PM) < (n + 1) by A5, A28, XXREAL_0: 1;

        then ( clique# PM) <= n by NAT_1: 13;

        then ( clique# PM) = n by A26, A27, XXREAL_0: 1;

        then

        consider Aa be Coloring of PM such that

         A38: ( card Aa) = n by A4;

        reconsider Ab = Aa as finite set by A38;

        set A = (Aa \/ {M});

        

         A39: cP = (cPM \/ M) by XBOOLE_1: 45;

         {M} is a_partition of M by EQREL_1: 39;

        then

         A40: A is a_partition of cP by A39, A7, Th3, XBOOLE_1: 79;

        now

          let x be set;

          assume

           A41: x in A;

          per cases by A41, XBOOLE_0:def 3;

            suppose x in Aa;

            then x is StableSet of PM by Def12;

            hence x is StableSet of P by Th30;

          end;

            suppose x in {M};

            hence x is StableSet of P by TARSKI:def 1;

          end;

        end;

        then

        reconsider A as Coloring of P by A40, Def12;

        take A;

         not M in Ab by A7, XBOOLE_1: 38;

        hence ( card A) = ( clique# P) by A5, A38, CARD_2: 41;

      end;

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

      hence ex A be Coloring of R st ( card A) = ( clique# R);

    end;

    begin

    ::$Notion-Name

    theorem :: DILWORTH:55

    

     Th55: for R be finite antisymmetric transitive RelStr, r,s be Nat st ( card R) = ((r * s) + 1) holds (ex C be Clique of R st ( card C) >= (r + 1)) or (ex A be StableSet of R st ( card A) >= (s + 1))

    proof

      let R be finite antisymmetric transitive RelStr, r,s be Nat such that

       A1: ( card R) = ((r * s) + 1) and

       A2: for C be Clique of R holds ( card C) < (r + 1) and

       A3: for A be StableSet of R holds ( card A) < (s + 1);

      consider p be Clique-partition of R such that

       A4: ( card p) = ( stability# R) by Th51;

      consider A be finite StableSet of R such that

       A5: ( card A) = ( stability# R) by Def6;

      ( stability# R) < (s + 1) by A3, A5;

      then

       A6: ( stability# R) <= s by NAT_1: 13;

      set wR = ( stability# R);

      set cR = the carrier of R;

      set f = ( canFS p);

      

       A7: ( len f) = ( card p) by FINSEQ_1: 93;

      

       A8: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

      set f = ( canFS p);

      

       A9: ( rng f) = p by FUNCT_2:def 3;

      then

      reconsider f as FinSequence of ( bool cR) by FINSEQ_1:def 4;

      now

        let d,e be Nat such that

         A10: d in ( dom f) and

         A11: e in ( dom f) and

         A12: d <> e;

        

         A13: (f . d) in ( rng f) by A10, FUNCT_1: 3;

        

         A14: (f . e) in ( rng f) by A11, FUNCT_1: 3;

        then

        reconsider fd = (f . d), fe = (f . e) as Subset of cR by A13, A9;

        fd <> fe by A12, A10, A11, FUNCT_1:def 4;

        hence (f . d) misses (f . e) by A13, A14, A9, EQREL_1:def 4;

      end;

      then

       A15: ( card ( union ( rng f))) = ( Sum ( Card f)) by INT_5: 48;

      reconsider n9 = r as Element of NAT by ORDINAL1:def 12;

      reconsider h = (wR |-> n9) as Element of (wR -tuples_on NAT );

      

       A16: ( Sum h) = (wR * r) by RVSUM_1: 80;

      ( dom f) = ( dom ( Card f)) by CARD_3:def 2;

      then ( len ( Card f)) = wR by A7, A4, FINSEQ_3: 29;

      then

      reconsider Cf = ( Card f) as Element of (wR -tuples_on NAT ) by FINSEQ_2: 92;

      now

        let j be Nat such that

         A19: j in ( Seg wR);

        

         A20: (h . j) = r by A19, FINSEQ_2: 57;

        

         A21: (Cf . j) = ( card (f . j)) by A19, A7, A8, A4, CARD_3:def 2;

        (f . j) in p by A9, A19, A4, A7, A8, FUNCT_1: 3;

        then

        reconsider fj = (f . j) as Clique of R by Def11;

        ( card fj) < (r + 1) by A2;

        hence (Cf . j) <= (h . j) by A20, A21, NAT_1: 13;

      end;

      then

       A22: ( Sum Cf) <= ( Sum h) by RVSUM_1: 82;

      (wR * r) <= (s * r) by A6, XREAL_1: 64;

      then ( Sum Cf) <= (s * r) by A16, A22, XXREAL_0: 2;

      then ((r * s) + 1) <= ((r * s) + 0 ) by A15, A9, A1, EQREL_1:def 4;

      hence contradiction by XREAL_1: 6;

    end;

    theorem :: DILWORTH:56

    for f be real-valued FinSequence, n be Nat st ( card f) = ((n ^2 ) + 1) & f is one-to-one holds ex g be real-valued FinSubsequence st g c= f & ( card g) >= (n + 1) & (g is increasing or g is decreasing)

    proof

      let f be real-valued FinSequence, n be Nat such that

       A1: ( card f) = ((n ^2 ) + 1) and

       A2: f is one-to-one;

      set cP = f;

      defpred P[ object, object] means ex i,j be Nat, r,s be Real st $1 = [i, r] & $2 = [j, s] & i < j & r < s;

      consider iP be Relation of f, f such that

       A3: for x,y be object holds [x, y] in iP iff x in f & y in f & P[x, y] from RELSET_1:sch 1;

      set P = RelStr (# cP, iP #);

      

       A4: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

      

       A5: P is antisymmetric

      proof

        let x,y be object such that x in the carrier of P and y in the carrier of P and

         A6: [x, y] in the InternalRel of P and

         A7: [y, x] in the InternalRel of P;

        consider i,j be Nat, r,s be Real such that

         A8: x = [i, r] and

         A9: y = [j, s] and

         A10: i < j & r < s by A6, A3;

        consider j1,i1 be Nat, s1,r1 be Real such that

         A11: y = [j1, s1] and

         A12: x = [i1, r1] and

         A13: j1 < i1 & s1 < r1 by A7, A3;

        i = i1 & j = j1 by A8, A9, A11, A12, XTUPLE_0: 1;

        hence x = y by A10, A13;

      end;

      P is transitive

      proof

        let x,y,z be object such that

         A14: x in the carrier of P and y in the carrier of P and

         A15: z in the carrier of P and

         A16: [x, y] in the InternalRel of P and

         A17: [y, z] in the InternalRel of P;

        consider ix,jy be Nat, rx,sy be Real such that

         A18: x = [ix, rx] and

         A19: y = [jy, sy] and

         A20: ix < jy & rx < sy by A16, A3;

        consider iy,jz be Nat, ry,sz be Real such that

         A21: y = [iy, ry] and

         A22: z = [jz, sz] and

         A23: iy < jz & ry < sz by A17, A3;

        jy = iy & sy = ry by A19, A21, XTUPLE_0: 1;

        then ix < jz & rx < sz by A20, A23, XXREAL_0: 2;

        hence [x, z] in the InternalRel of P by A18, A22, A14, A15, A3;

      end;

      then

      reconsider P as finite antisymmetric transitive RelStr by A5;

      

       A24: ( card P) = ( card f);

      per cases by A24, A1, Th55;

        suppose ex C be Clique of P st ( card C) >= (n + 1);

        then

        consider C be Clique of P such that

         A25: ( card C) >= (n + 1);

        set g = C;

        reconsider g as Subset of f;

        reconsider g as Function;

        ( dom g) c= ( Seg ( len f))

        proof

          let x be object;

          assume x in ( dom g);

          then

          consider y be object such that

           A26: [x, y] in g by XTUPLE_0:def 12;

          x in ( dom f) by A26, XTUPLE_0:def 12;

          hence thesis by FINSEQ_1:def 3;

        end;

        then

        reconsider g as FinSubsequence by FINSEQ_1:def 12;

        reconsider g as real-valued FinSubsequence;

        take g;

        thus g c= f;

        thus ( card g) >= (n + 1) by A25;

        g is increasing

        proof

          let e1,e2 be ExtReal such that

           A27: e1 in ( dom g) and

           A28: e2 in ( dom g) and

           A29: e1 < e2;

          

           A30: [e1, (g . e1)] in g by A27, FUNCT_1: 1;

          

           A31: [e2, (g . e2)] in g by A28, FUNCT_1: 1;

          then

          reconsider p1 = [e1, (g . e1)], p2 = [e2, (g . e2)] as Element of P by A30;

          

           A32: p1 <> p2 by A29, XTUPLE_0: 1;

          per cases by A30, A31, A32, Th6;

            suppose p1 <= p2;

            then [p1, p2] in iP;

            then

            consider i,j be Nat, r,s be Real such that

             A33: p1 = [i, r] and

             A34: p2 = [j, s] and

             A35: i < j & r < s by A3;

            j = e2 & s = (g . e2) by A34, XTUPLE_0: 1;

            hence (g . e1) < (g . e2) by A35, A33, XTUPLE_0: 1;

          end;

            suppose p2 <= p1;

            then [p2, p1] in iP;

            then

            consider i,j be Nat, r,s be Real such that

             A36: p2 = [i, r] and

             A37: p1 = [j, s] and

             A38: i < j & r < s by A3;

            i = e2 & j = e1 by A36, A37, XTUPLE_0: 1;

            hence (g . e1) < (g . e2) by A29, A38;

          end;

        end;

        hence thesis;

      end;

        suppose ex A be StableSet of P st ( card A) >= (n + 1);

        then

        consider A be StableSet of P such that

         A39: ( card A) >= (n + 1);

        set g = A;

        reconsider g as Subset of f;

        reconsider g as Function;

        

         A40: ( dom g) c= ( Seg ( len f))

        proof

          let x be object;

          assume x in ( dom g);

          then

          consider y be object such that

           A41: [x, y] in g by XTUPLE_0:def 12;

          x in ( dom f) by A41, XTUPLE_0:def 12;

          hence thesis by FINSEQ_1:def 3;

        end;

        then

        reconsider g as FinSubsequence by FINSEQ_1:def 12;

        reconsider g as real-valued FinSubsequence;

        take g;

        thus g c= f;

        thus ( card g) >= (n + 1) by A39;

        g is decreasing

        proof

          let e1,e2 be ExtReal such that

           A42: e1 in ( dom g) and

           A43: e2 in ( dom g) and

           A44: e1 < e2;

          

           A45: [e1, (g . e1)] in g by A42, FUNCT_1: 1;

          

           A46: [e2, (g . e2)] in g by A43, FUNCT_1: 1;

          then

          reconsider p1 = [e1, (g . e1)], p2 = [e2, (g . e2)] as Element of P by A45;

          

           A47: p1 <> p2 by A44, XTUPLE_0: 1;

          (g . e1) = (f . e1) & (g . e2) = (f . e2) by A42, A43, GRFUNC_1: 2;

          then

           A48: (g . e1) <> (g . e2) by A4, A40, A42, A43, A44, A2;

          reconsider i = e1, j = e2 as Nat by A42, A43;

          reconsider r = (g . e1), s = (g . e2) as Real;

          

           A49: p1 = [i, r] & p2 = [j, s];

          per cases by A48, XXREAL_0: 1;

            suppose (g . e1) < (g . e2);

            then [p1, p2] in iP by A45, A3, A44, A49;

            then p1 <= p2;

            hence (g . e1) > (g . e2) by A45, A46, A47, Def2;

          end;

            suppose (g . e1) > (g . e2);

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end;