dickson.miz



    begin

    theorem :: DICKSON:1

    

     Th1: for g be Function, x be set st ( dom g) = {x} holds g = (x .--> (g . x))

    proof

      let g be Function, x be set such that

       A1: ( dom g) = {x};

      now

        let a,b be object;

        

         A2: ( dom (x .--> (g . x))) = {x};

        hereby

          assume

           A3: [a, b] in g;

          then

           A4: a in {x} by A1, FUNCT_1: 1;

          then

           A5: a = x by TARSKI:def 1;

          then b = (g . x) by A3, FUNCT_1: 1;

          then ((x .--> (g . x)) . a) = b by A5, FUNCOP_1: 72;

          hence [a, b] in (x .--> (g . x)) by A2, A4, FUNCT_1: 1;

        end;

        assume

         A6: [a, b] in (x .--> (g . x));

        then

         A7: a in {x} by A2, FUNCT_1: 1;

        then

         A8: a = x by TARSKI:def 1;

        b = ((x .--> (g . x)) . a) by A6, FUNCT_1: 1

        .= (g . a) by A8, FUNCOP_1: 72;

        hence [a, b] in g by A1, A7, FUNCT_1: 1;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    ::$Canceled

    theorem :: DICKSON:3

    

     Th2: for X be infinite set holds ex f be sequence of X st f is one-to-one

    proof

      let X be infinite set;

      ( card NAT ) c= ( card X) by CARD_3: 85;

      then

      consider f be Function such that

       A1: f is one-to-one and

       A2: ( dom f) = NAT and

       A3: ( rng f) c= X by CARD_1: 10;

      for x be object st x in NAT holds (f . x) in X by A3, A2, FUNCT_1: 3;

      then

      reconsider f as sequence of X by A2, FUNCT_2: 3;

      take f;

      thus thesis by A1;

    end;

    definition

      let R be RelStr, f be sequence of R;

      :: DICKSON:def1

      attr f is ascending means for n be Element of NAT holds (f . (n + 1)) <> (f . n) & [(f . n), (f . (n + 1))] in the InternalRel of R;

    end

    definition

      let R be RelStr, f be sequence of R;

      :: DICKSON:def2

      attr f is weakly-ascending means for n be Nat holds [(f . n), (f . (n + 1))] in the InternalRel of R;

    end

    theorem :: DICKSON:4

    

     Th3: for R be non empty transitive RelStr, f be sequence of R st f is weakly-ascending holds for i,j be Nat st i < j holds (f . i) <= (f . j)

    proof

      let R be non empty transitive RelStr, f be sequence of R such that

       A1: f is weakly-ascending;

      let i be Nat;

      defpred P[ Nat] means i < $1 implies (f . i) <= (f . $1);

      

       A2: P[ 0 ] by NAT_1: 2;

      

       A3: for j be Nat st P[j] holds P[(j + 1)]

      proof

        let j be Nat such that

         A4: P[j] and

         A5: i < (j + 1);

        reconsider fj1 = (f . (j + 1)) as Element of R;

        

         A6: [(f . j), (f . (j + 1))] in the InternalRel of R by A1;

        then

         A7: (f . j) <= fj1;

        

         A8: i <= j by A5, NAT_1: 13;

        per cases by A8, XXREAL_0: 1;

          suppose i < j;

          hence thesis by A4, A7, ORDERS_2: 3;

        end;

          suppose i = j;

          hence thesis by A6;

        end;

      end;

      thus for j be Nat holds P[j] from NAT_1:sch 2( A2, A3);

    end;

    theorem :: DICKSON:5

    

     Th4: for R be non empty RelStr holds R is connected iff the InternalRel of R is_strongly_connected_in the carrier of R

    proof

      let R be non empty RelStr;

      set IR = the InternalRel of R, CR = the carrier of R;

      hereby

        assume

         A1: R is connected;

        now

          let x,y be object such that

           A2: x in CR and

           A3: y in CR;

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

          x9 <= y9 or y9 <= x9 by A1, WAYBEL_0:def 29;

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

        end;

        hence IR is_strongly_connected_in CR;

      end;

      assume IR is_strongly_connected_in CR;

      then for x,y be Element of R holds x <= y or y <= x;

      hence thesis by WAYBEL_0:def 29;

    end;

    theorem :: DICKSON:6

    

     Th5: for L be RelStr, Y be set, a be set holds (the InternalRel of L -Seg a) misses Y & a in Y iff a is_minimal_wrt (Y,the InternalRel of L)

    proof

      let L be RelStr, Y be set, a be set;

      set IR = the InternalRel of L;

      hereby

        assume that

         A1: (IR -Seg a) misses Y and

         A2: a in Y;

        

         A3: ((IR -Seg a) /\ Y) = {} by A1, XBOOLE_0:def 7;

        now

          assume ex y be set st y in Y & y <> a & [y, a] in IR;

          then

          consider y be set such that

           A4: y in Y and

           A5: y <> a and

           A6: [y, a] in IR;

          y in (IR -Seg a) by A5, A6, WELLORD1: 1;

          hence contradiction by A3, A4, XBOOLE_0:def 4;

        end;

        hence a is_minimal_wrt (Y,IR) by A2, WAYBEL_4:def 25;

      end;

      assume

       A7: a is_minimal_wrt (Y,IR);

      now

        assume not (IR -Seg a) misses Y;

        then ((IR -Seg a) /\ Y) <> {} by XBOOLE_0:def 7;

        then

        consider y be object such that

         A8: y in ((IR -Seg a) /\ Y) by XBOOLE_0:def 1;

        

         A9: y in (IR -Seg a) by A8, XBOOLE_0:def 4;

        

         A10: y in Y by A8, XBOOLE_0:def 4;

        

         A11: y <> a by A9, WELLORD1: 1;

         [y, a] in IR by A9, WELLORD1: 1;

        hence contradiction by A7, A10, A11, WAYBEL_4:def 25;

      end;

      hence (IR -Seg a) misses Y;

      thus thesis by A7, WAYBEL_4:def 25;

    end;

    theorem :: DICKSON:7

    

     Th6: for L be non empty transitive antisymmetric RelStr, x be Element of L, a,N be set st a is_minimal_wrt (((the InternalRel of L -Seg x) /\ N),the InternalRel of L) holds a is_minimal_wrt (N,the InternalRel of L)

    proof

      let L be non empty transitive antisymmetric RelStr, x be Element of L, a,N be set such that

       A1: a is_minimal_wrt (((the InternalRel of L -Seg x) /\ N),the InternalRel of L);

      set IR = the InternalRel of L, CR = the carrier of L;

      

       A2: IR is_transitive_in CR by ORDERS_2:def 3;

      now

        

         A3: a in ((IR -Seg x) /\ N) by A1, WAYBEL_4:def 25;

        then

         A4: a in (IR -Seg x) by XBOOLE_0:def 4;

        then

         A5: a <> x by WELLORD1: 1;

        

         A6: [a, x] in IR by A4, WELLORD1: 1;

        then

        reconsider a9 = a as Element of L by ZFMISC_1: 87;

        thus a in N by A3, XBOOLE_0:def 4;

        now

          assume ex y be set st y in N & y <> a & [y, a] in IR;

          then

          consider y be set such that

           A7: y in N and

           A8: y <> a and

           A9: [y, a] in IR;

          

           A10: a in CR by A9, ZFMISC_1: 87;

          y in CR by A9, ZFMISC_1: 87;

          then

           A11: [y, x] in IR by A2, A6, A9, A10;

          per cases ;

            suppose x = y;

            then

             A12: x <= a9 by A9;

            a9 <= x by A6;

            hence contradiction by A5, A12, ORDERS_2: 2;

          end;

            suppose x <> y;

            then y in (IR -Seg x) by A11, WELLORD1: 1;

            then y in ((IR -Seg x) /\ N) by A7, XBOOLE_0:def 4;

            hence contradiction by A1, A8, A9, WAYBEL_4:def 25;

          end;

        end;

        hence not ex y be set st y in N & y <> a & [y, a] in IR;

      end;

      hence thesis by WAYBEL_4:def 25;

    end;

    begin

    definition

      let R be RelStr;

      :: DICKSON:def3

      attr R is quasi_ordered means R is reflexive transitive;

    end

    definition

      let R be RelStr;

      :: DICKSON:def4

      func EqRel R -> Equivalence_Relation of the carrier of R equals

      : Def4: (the InternalRel of R /\ (the InternalRel of R ~ ));

      coherence

      proof

        set IR = the InternalRel of R, CR = the carrier of R;

        R is reflexive by A1;

        then

         A2: IR is_reflexive_in CR;

        R is transitive by A1;

        then

         A3: IR is_transitive_in CR;

        then

         A4: IR quasi_orders CR by A2;

        

         A5: (IR /\ (IR ~ )) is_reflexive_in CR

        proof

          let x be object;

          assume x in CR;

          then

           A6: [x, x] in IR by A2;

          then [x, x] in (IR ~ ) by RELAT_1:def 7;

          hence thesis by A6, XBOOLE_0:def 4;

        end;

        then

         A7: ( dom (IR /\ (IR ~ ))) = CR by ORDERS_1: 13;

        

         A8: ( field (IR /\ (IR ~ ))) = CR by A5, ORDERS_1: 13;

        

         A9: (IR /\ (IR ~ )) is_symmetric_in CR

        proof

          let x,y be object such that x in CR and y in CR and

           A10: [x, y] in (IR /\ (IR ~ ));

          

           A11: [x, y] in IR by A10, XBOOLE_0:def 4;

          

           A12: [x, y] in (IR ~ ) by A10, XBOOLE_0:def 4;

          

           A13: [y, x] in (IR ~ ) by A11, RELAT_1:def 7;

           [y, x] in IR by A12, RELAT_1:def 7;

          hence thesis by A13, XBOOLE_0:def 4;

        end;

        (IR /\ (IR ~ )) is_transitive_in CR

        proof

          let x,y,z be object such that

           A14: x in CR and

           A15: y in CR and

           A16: z in CR and

           A17: [x, y] in (IR /\ (IR ~ )) and

           A18: [y, z] in (IR /\ (IR ~ ));

          

           A19: [x, y] in IR by A17, XBOOLE_0:def 4;

          

           A20: [x, y] in (IR ~ ) by A17, XBOOLE_0:def 4;

          

           A21: [y, z] in IR by A18, XBOOLE_0:def 4;

          

           A22: [y, z] in (IR ~ ) by A18, XBOOLE_0:def 4;

          

           A23: [x, z] in IR by A3, A14, A15, A16, A19, A21;

          (IR ~ ) quasi_orders CR by A4, ORDERS_1: 40;

          then (IR ~ ) is_transitive_in CR;

          then [x, z] in (IR ~ ) by A14, A15, A16, A20, A22;

          hence thesis by A23, XBOOLE_0:def 4;

        end;

        hence thesis by A7, A8, A9, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

      end;

    end

    theorem :: DICKSON:8

    

     Th7: for R be RelStr, x,y be Element of R st R is quasi_ordered holds x in ( Class (( EqRel R),y)) iff x <= y & y <= x

    proof

      let R be RelStr, x,y be Element of R such that

       A1: R is quasi_ordered;

      set IR = the InternalRel of R;

      hereby

        assume x in ( Class (( EqRel R),y));

        then [x, y] in ( EqRel R) by EQREL_1: 19;

        then

         A2: [x, y] in (IR /\ (IR ~ )) by A1, Def4;

        then

         A3: [x, y] in IR by XBOOLE_0:def 4;

        

         A4: [x, y] in (IR ~ ) by A2, XBOOLE_0:def 4;

        thus x <= y by A3;

         [y, x] in IR by A4, RELAT_1:def 7;

        hence y <= x;

      end;

      assume that

       A5: x <= y and

       A6: y <= x;

      

       A7: [y, x] in IR by A6;

      

       A8: [x, y] in IR by A5;

       [x, y] in (IR ~ ) by A7, RELAT_1:def 7;

      then [x, y] in (IR /\ (IR ~ )) by A8, XBOOLE_0:def 4;

      then [x, y] in ( EqRel R) by A1, Def4;

      hence thesis by EQREL_1: 19;

    end;

    definition

      let R be RelStr;

      :: DICKSON:def5

      func <=E R -> Relation of ( Class ( EqRel R)) means

      : Def5: for A,B be object holds [A, B] in it iff ex a,b be Element of R st A = ( Class (( EqRel R),a)) & B = ( Class (( EqRel R),b)) & a <= b;

      existence

      proof

        set IR = the InternalRel of R, CR = the carrier of R;

        per cases ;

          suppose

           A1: CR = {} ;

          reconsider IT = {} as Relation of ( Class ( EqRel R)) by RELSET_1: 12;

          take IT;

          let A,B be object;

          thus [A, B] in IT implies ex a,b be Element of R st A = ( Class (( EqRel R),a)) & B = ( Class (( EqRel R),b)) & a <= b;

          given a,b be Element of R such that A = ( Class (( EqRel R),a)) and B = ( Class (( EqRel R),b)) and

           A2: a <= b;

          IR = {} by A1;

          hence thesis by A2;

        end;

          suppose CR is non empty;

          then

          reconsider R9 = R as non empty RelStr;

          set IT = { [( Class (( EqRel R),a)), ( Class (( EqRel R),b))] where a,b be Element of R9 : a <= b };

          set Y = ( Class ( EqRel R));

          IT c= [:Y, Y:]

          proof

            let x be object;

            assume x in IT;

            then

            consider a,b be Element of R9 such that

             A3: x = [( Class (( EqRel R),a)), ( Class (( EqRel R),b))] and a <= b;

            

             A4: ( Class (( EqRel R),a)) in Y by EQREL_1:def 3;

            ( Class (( EqRel R),b)) in Y by EQREL_1:def 3;

            hence thesis by A3, A4, ZFMISC_1:def 2;

          end;

          then

          reconsider IT as Relation of ( Class ( EqRel R));

          take IT;

          let A,B be object;

          hereby

            assume [A, B] in IT;

            then

            consider a,b be Element of R such that

             A5: [A, B] = [( Class (( EqRel R),a)), ( Class (( EqRel R),b))] and

             A6: a <= b;

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

            take a9, b9;

            thus A = ( Class (( EqRel R),a9)) & B = ( Class (( EqRel R),b9)) & a9 <= b9 by A5, A6, XTUPLE_0: 1;

          end;

          given a,b be Element of R such that

           A7: A = ( Class (( EqRel R),a)) and

           A8: B = ( Class (( EqRel R),b)) and

           A9: a <= b;

          thus thesis by A7, A8, A9;

        end;

      end;

      uniqueness

      proof

        let IT1,IT2 be Relation of ( Class ( EqRel R)) such that

         A10: for A,B be object holds [A, B] in IT1 iff ex a,b be Element of R st A = ( Class (( EqRel R),a)) & B = ( Class (( EqRel R),b)) & a <= b and

         A11: for A,B be object holds [A, B] in IT2 iff ex a,b be Element of R st A = ( Class (( EqRel R),a)) & B = ( Class (( EqRel R),b)) & a <= b;

        now

          let x be object;

          hereby

            assume

             A12: x in IT1;

            set Y = ( Class ( EqRel R));

            consider A,B be object such that A in Y and B in Y and

             A13: x = [A, B] by A12, ZFMISC_1:def 2;

            ex a,b be Element of R st (A = ( Class (( EqRel R),a))) & (B = ( Class (( EqRel R),b))) & (a <= b) by A10, A12, A13;

            hence x in IT2 by A11, A13;

          end;

          assume

           A14: x in IT2;

          set Y = ( Class ( EqRel R));

          consider A,B be object such that A in Y and B in Y and

           A15: x = [A, B] by A14, ZFMISC_1:def 2;

          ex a,b be Element of R st (A = ( Class (( EqRel R),a))) & (B = ( Class (( EqRel R),b))) & (a <= b) by A11, A14, A15;

          hence x in IT1 by A10, A15;

        end;

        hence IT1 = IT2 by TARSKI: 2;

      end;

    end

    theorem :: DICKSON:9

    

     Th8: for R be RelStr st R is quasi_ordered holds ( <=E R) partially_orders ( Class ( EqRel R))

    proof

      let R be RelStr;

      set CR = the carrier of R;

      set IR = the InternalRel of R;

      assume

       A1: R is quasi_ordered;

      then R is transitive;

      then

       A2: IR is_transitive_in CR;

      thus ( <=E R) is_reflexive_in ( Class ( EqRel R))

      proof

        let x be object;

        assume x in ( Class ( EqRel R));

        then

        consider a be object such that

         A3: a in CR and

         A4: x = ( Class (( EqRel R),a)) by EQREL_1:def 3;

        R is reflexive by A1;

        then IR is_reflexive_in CR;

        then

         A5: [a, a] in IR by A3;

        reconsider a9 = a as Element of R by A3;

        a9 <= a9 by A5;

        hence thesis by A4, Def5;

      end;

      thus ( <=E R) is_transitive_in ( Class ( EqRel R))

      proof

        let x,y,z be object such that

         A6: x in ( Class ( EqRel R)) and y in ( Class ( EqRel R)) and z in ( Class ( EqRel R)) and

         A7: [x, y] in ( <=E R) and

         A8: [y, z] in ( <=E R);

        consider a,b be Element of R such that

         A9: x = ( Class (( EqRel R),a)) and

         A10: y = ( Class (( EqRel R),b)) and

         A11: a <= b by A7, Def5;

        consider c,d be Element of R such that

         A12: y = ( Class (( EqRel R),c)) and

         A13: z = ( Class (( EqRel R),d)) and

         A14: c <= d by A8, Def5;

        

         A15: [a, b] in IR by A11;

        

         A16: [c, d] in IR by A14;

        

         A17: ex x1 be object st (x1 in CR) & (x = ( Class (( EqRel R),x1))) by A6, EQREL_1:def 3;

        then b in ( Class (( EqRel R),c)) by A10, A12, EQREL_1: 23;

        then [b, c] in ( EqRel R) by EQREL_1: 19;

        then [b, c] in (IR /\ (IR ~ )) by A1, Def4;

        then [b, c] in IR by XBOOLE_0:def 4;

        then [a, c] in IR by A2, A15, A17;

        then [a, d] in IR by A2, A16, A17;

        then a <= d;

        hence thesis by A9, A13, Def5;

      end;

      thus ( <=E R) is_antisymmetric_in ( Class ( EqRel R))

      proof

        let x,y be object such that

         A18: x in ( Class ( EqRel R)) and y in ( Class ( EqRel R)) and

         A19: [x, y] in ( <=E R) and

         A20: [y, x] in ( <=E R);

        consider a,b be Element of R such that

         A21: x = ( Class (( EqRel R),a)) and

         A22: y = ( Class (( EqRel R),b)) and

         A23: a <= b by A19, Def5;

        consider c,d be Element of R such that

         A24: y = ( Class (( EqRel R),c)) and

         A25: x = ( Class (( EqRel R),d)) and

         A26: c <= d by A20, Def5;

        

         A27: [a, b] in IR by A23;

        

         A28: [c, d] in IR by A26;

        

         A29: ex x1 be object st (x1 in CR) & (x = ( Class (( EqRel R),x1))) by A18, EQREL_1:def 3;

        then

         A30: d in ( Class (( EqRel R),a)) by A21, A25, EQREL_1: 23;

        a in ( Class (( EqRel R),a)) by A29, EQREL_1: 20;

        then

         A31: [a, d] in ( EqRel R) by A30, EQREL_1: 22;

        

         A32: c in ( Class (( EqRel R),b)) by A22, A24, A29, EQREL_1: 23;

        b in ( Class (( EqRel R),b)) by A29, EQREL_1: 20;

        then

         A33: [b, c] in ( EqRel R) by A32, EQREL_1: 22;

         [a, d] in (IR /\ (IR ~ )) by A1, A31, Def4;

        then [a, d] in (IR ~ ) by XBOOLE_0:def 4;

        then

         A34: [d, a] in IR by RELAT_1:def 7;

         [b, c] in (IR /\ (IR ~ )) by A1, A33, Def4;

        then [b, c] in IR by XBOOLE_0:def 4;

        then [b, d] in IR by A2, A28, A29;

        then

         A35: [b, a] in IR by A2, A29, A34;

         [b, a] in (IR ~ ) by A27, RELAT_1:def 7;

        then [b, a] in (IR /\ (IR ~ )) by A35, XBOOLE_0:def 4;

        then [b, a] in ( EqRel R) by A1, Def4;

        then b in ( Class (( EqRel R),a)) by EQREL_1: 19;

        hence thesis by A21, A22, EQREL_1: 23;

      end;

    end;

    theorem :: DICKSON:10

    for R be non empty RelStr st R is quasi_ordered & R is connected holds ( <=E R) linearly_orders ( Class ( EqRel R))

    proof

      let R be non empty RelStr such that

       A1: R is quasi_ordered and

       A2: R is connected;

      

       A3: ( <=E R) partially_orders ( Class ( EqRel R)) by A1, Th8;

      hence ( <=E R) is_reflexive_in ( Class ( EqRel R));

      thus ( <=E R) is_transitive_in ( Class ( EqRel R)) by A3;

      thus ( <=E R) is_antisymmetric_in ( Class ( EqRel R)) by A3;

      thus ( <=E R) is_connected_in ( Class ( EqRel R))

      proof

        set CR = the carrier of R;

        let x,y be object such that

         A4: x in ( Class ( EqRel R)) and

         A5: y in ( Class ( EqRel R)) and x <> y and

         A6: not [x, y] in ( <=E R);

        consider a be object such that

         A7: a in CR and

         A8: x = ( Class (( EqRel R),a)) by A4, EQREL_1:def 3;

        consider b be object such that

         A9: b in CR and

         A10: y = ( Class (( EqRel R),b)) by A5, EQREL_1:def 3;

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

         not a9 <= b9 by A6, A8, A10, Def5;

        then b9 <= a9 by A2, WAYBEL_0:def 29;

        hence thesis by A8, A10, Def5;

      end;

    end;

    definition

      let R be Relation;

      :: DICKSON:def6

      func R \~ -> Relation equals (R \ (R ~ ));

      correctness ;

    end

    registration

      let R be Relation;

      cluster (R \~ ) -> asymmetric;

      coherence

      proof

        now

          let x,y be object such that x in ( field (R \~ )) and y in ( field (R \~ )) and

           A1: [x, y] in (R \~ );

           not [x, y] in (R ~ ) by A1, XBOOLE_0:def 5;

          hence not [y, x] in (R \~ ) by RELAT_1:def 7;

        end;

        then (R \~ ) is_asymmetric_in ( field (R \~ ));

        hence thesis;

      end;

    end

    definition

      let X be set, R be Relation of X;

      :: original: \~

      redefine

      func R \~ -> Relation of X ;

      coherence

      proof

        (R \~ ) = (R \ (R ~ ));

        hence thesis;

      end;

    end

    definition

      let R be RelStr;

      :: DICKSON:def7

      func R \~ -> strict RelStr equals RelStr (# the carrier of R, (the InternalRel of R \~ ) #);

      correctness ;

    end

    registration

      let R be non empty RelStr;

      cluster (R \~ ) -> non empty;

      coherence ;

    end

    registration

      let R be transitive RelStr;

      cluster (R \~ ) -> transitive;

      coherence

      proof

        set IR = the InternalRel of R, CR = the carrier of R;

        set IR9 = the InternalRel of (R \~ ), CR9 = the carrier of (R \~ );

        

         A1: IR is_transitive_in CR by ORDERS_2:def 3;

        now

          let x,y,z be object such that

           A2: x in CR9 and

           A3: y in CR9 and

           A4: z in CR9 and

           A5: [x, y] in IR9 and

           A6: [y, z] in IR9;

          

           A7: not [x, y] in (IR ~ ) by A5, XBOOLE_0:def 5;

          

           A8: [x, z] in IR by A1, A2, A3, A4, A5, A6;

          now

            assume [x, z] in (IR ~ );

            then [z, x] in IR by RELAT_1:def 7;

            then [y, x] in IR by A1, A2, A3, A4, A6;

            hence contradiction by A7, RELAT_1:def 7;

          end;

          hence [x, z] in IR9 by A8, XBOOLE_0:def 5;

        end;

        then IR9 is_transitive_in CR9;

        hence thesis;

      end;

    end

    registration

      let R be RelStr;

      cluster (R \~ ) -> antisymmetric;

      coherence

      proof

        set IR = the InternalRel of R;

        set IR9 = the InternalRel of (R \~ ), CR9 = the carrier of (R \~ );

        now

          let x,y be object such that x in CR9 and y in CR9 and

           A1: [x, y] in IR9 and

           A2: [y, x] in IR9;

           not [x, y] in (IR ~ ) by A1, XBOOLE_0:def 5;

          hence x = y by A2, RELAT_1:def 7;

        end;

        then IR9 is_antisymmetric_in CR9;

        hence thesis;

      end;

    end

    theorem :: DICKSON:11

    for R be non empty Poset, x be Element of R holds ( Class (( EqRel R),x)) = {x}

    proof

      let R be non empty Poset;

      set IR = the InternalRel of R, CR = the carrier of R;

      let x be Element of CR;

      

       A1: R is quasi_ordered;

      

       A2: IR is_antisymmetric_in CR by ORDERS_2:def 4;

      now

        let z be object;

        hereby

          assume z in ( Class (( EqRel R),x));

          then [z, x] in ( EqRel R) by EQREL_1: 19;

          then

           A3: [z, x] in (IR /\ (IR ~ )) by A1, Def4;

          then

           A4: [z, x] in IR by XBOOLE_0:def 4;

           [z, x] in (IR ~ ) by A3, XBOOLE_0:def 4;

          then

           A5: [x, z] in IR by RELAT_1:def 7;

          z in ( dom IR) by A4, XTUPLE_0:def 12;

          then z = x by A2, A4, A5;

          hence z in {x} by TARSKI:def 1;

        end;

        assume z in {x};

        then z = x by TARSKI:def 1;

        hence z in ( Class (( EqRel R),x)) by EQREL_1: 20;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: DICKSON:12

    for R be Relation holds R = (R \~ ) iff R is asymmetric

    proof

      let R be Relation;

      thus R = (R \~ ) implies R is asymmetric;

      assume R is asymmetric;

      then

       A1: R is_asymmetric_in ( field R);

      now

        let a,b be object;

        hereby

          assume

           A2: [a, b] in R;

          then

           A3: a in ( field R) by RELAT_1: 15;

          b in ( field R) by A2, RELAT_1: 15;

          then not [b, a] in R by A1, A2, A3;

          then not [a, b] in (R ~ ) by RELAT_1:def 7;

          hence [a, b] in (R \~ ) by A2, XBOOLE_0:def 5;

        end;

        assume [a, b] in (R \~ );

        hence [a, b] in R;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    theorem :: DICKSON:13

    for R be Relation st R is transitive holds (R \~ ) is transitive

    proof

      let R be Relation;

      assume R is transitive;

      then

       A1: R is_transitive_in ( field R);

      now

        let x,y,z be object such that x in ( field (R \~ )) and y in ( field (R \~ )) and z in ( field (R \~ )) and

         A2: [x, y] in (R \~ ) and

         A3: [y, z] in (R \~ );

        

         A4: x in ( field R) by A2, RELAT_1: 15;

        

         A5: y in ( field R) by A2, RELAT_1: 15;

        

         A6: z in ( field R) by A3, RELAT_1: 15;

        then

         A7: [x, z] in R by A1, A2, A3, A4, A5;

         not [x, y] in (R ~ ) by A2, XBOOLE_0:def 5;

        then not [y, x] in R by RELAT_1:def 7;

        then not [z, x] in R by A1, A3, A4, A5, A6;

        then not [x, z] in (R ~ ) by RELAT_1:def 7;

        hence [x, z] in (R \~ ) by A7, XBOOLE_0:def 5;

      end;

      then (R \~ ) is_transitive_in ( field (R \~ ));

      hence thesis;

    end;

    theorem :: DICKSON:14

    for R be Relation, a,b be set st R is antisymmetric holds [a, b] in (R \~ ) iff [a, b] in R & a <> b

    proof

      let R be Relation, a,b be set;

      assume R is antisymmetric;

      then

       A1: R is_antisymmetric_in ( field R);

      

       A2: (R \~ ) is_asymmetric_in ( field (R \~ )) by RELAT_2:def 13;

      hereby

        assume

         A3: [a, b] in (R \~ );

        hence [a, b] in R;

        now

          assume

           A4: a = b;

          a in ( field (R \~ )) by A3, RELAT_1: 15;

          hence contradiction by A2, A3, A4;

        end;

        hence a <> b;

      end;

      assume that

       A5: [a, b] in R and

       A6: a <> b;

      

       A7: a in ( field R) by A5, RELAT_1: 15;

      b in ( field R) by A5, RELAT_1: 15;

      then not [b, a] in R by A1, A5, A6, A7;

      then not [a, b] in (R ~ ) by RELAT_1:def 7;

      hence thesis by A5, XBOOLE_0:def 5;

    end;

    theorem :: DICKSON:15

    

     Th14: for R be RelStr st R is well_founded holds (R \~ ) is well_founded

    proof

      let R be RelStr such that

       A1: R is well_founded;

      set IR = the InternalRel of R, CR = the carrier of R;

      set IR9 = the InternalRel of (R \~ ), CR9 = the carrier of (R \~ );

      

       A2: IR is_well_founded_in CR by A1, WELLFND1:def 2;

      now

        let Y be set such that

         A3: Y c= CR9 and

         A4: Y <> {} ;

        consider a be object such that

         A5: a in Y and

         A6: (IR -Seg a) misses Y by A2, A3, A4, WELLORD1:def 3;

        

         A7: ((IR -Seg a) /\ Y) = {} by A6, XBOOLE_0:def 7;

        take a;

        thus a in Y by A5;

        now

          given z be object such that

           A8: z in ((IR9 -Seg a) /\ Y);

          

           A9: z in (IR9 -Seg a) by A8, XBOOLE_0:def 4;

          

           A10: z in Y by A8, XBOOLE_0:def 4;

          

           A11: z <> a by A9, WELLORD1: 1;

           [z, a] in IR9 by A9, WELLORD1: 1;

          then z in (IR -Seg a) by A11, WELLORD1: 1;

          hence contradiction by A7, A10, XBOOLE_0:def 4;

        end;

        then ((IR9 -Seg a) /\ Y) = {} by XBOOLE_0:def 1;

        hence (IR9 -Seg a) misses Y by XBOOLE_0:def 7;

      end;

      then IR9 is_well_founded_in CR9 by WELLORD1:def 3;

      hence thesis by WELLFND1:def 2;

    end;

    theorem :: DICKSON:16

    

     Th15: for R be RelStr st (R \~ ) is well_founded & R is antisymmetric holds R is well_founded

    proof

      let R be RelStr such that

       A1: (R \~ ) is well_founded and

       A2: R is antisymmetric;

      set IR = the InternalRel of R, CR = the carrier of R;

      set IR9 = the InternalRel of (R \~ );

      

       A3: IR is_antisymmetric_in CR by A2;

      

       A4: IR9 is_well_founded_in CR by A1, WELLFND1:def 2;

      now

        let Y be set such that

         A5: Y c= CR and

         A6: Y <> {} ;

        consider a be object such that

         A7: a in Y and

         A8: (IR9 -Seg a) misses Y by A4, A5, A6, WELLORD1:def 3;

        

         A9: ((IR9 -Seg a) /\ Y) = {} by A8, XBOOLE_0:def 7;

        take a;

        thus a in Y by A7;

        now

          assume ((IR -Seg a) /\ Y) <> {} ;

          then

          consider z be object such that

           A10: z in ((IR -Seg a) /\ Y) by XBOOLE_0:def 1;

          

           A11: z in (IR -Seg a) by A10, XBOOLE_0:def 4;

          

           A12: z in Y by A10, XBOOLE_0:def 4;

          

           A13: z <> a by A11, WELLORD1: 1;

          

           A14: [z, a] in IR by A11, WELLORD1: 1;

          then not [a, z] in IR by A3, A5, A7, A12, A13;

          then not [z, a] in (IR ~ ) by RELAT_1:def 7;

          then [z, a] in (IR \ (IR ~ )) by A14, XBOOLE_0:def 5;

          then z in (IR9 -Seg a) by A13, WELLORD1: 1;

          hence contradiction by A9, A12, XBOOLE_0:def 4;

        end;

        hence (IR -Seg a) misses Y by XBOOLE_0:def 7;

      end;

      then IR is_well_founded_in CR by WELLORD1:def 3;

      hence thesis by WELLFND1:def 2;

    end;

    begin

    theorem :: DICKSON:17

    

     Th16: for L be RelStr, N be set, x be Element of (L \~ ) holds x is_minimal_wrt (N,the InternalRel of (L \~ )) iff (x in N & for y be Element of L st y in N & [y, x] in the InternalRel of L holds [x, y] in the InternalRel of L)

    proof

      let L be RelStr, N be set, x be Element of (L \~ );

      set IR = the InternalRel of L;

      set IR9 = the InternalRel of (L \~ );

      hereby

        assume

         A1: x is_minimal_wrt (N,the InternalRel of (L \~ ));

        hence x in N by WAYBEL_4:def 25;

        let y be Element of L such that

         A2: y in N;

        assume

         A3: [y, x] in IR;

        now

          per cases ;

            suppose x = y;

            hence [x, y] in IR by A3;

          end;

            suppose x <> y;

            then not [y, x] in IR9 by A1, A2, WAYBEL_4:def 25;

            then [y, x] in (IR ~ ) by A3, XBOOLE_0:def 5;

            hence [x, y] in IR by RELAT_1:def 7;

          end;

        end;

        hence [x, y] in the InternalRel of L;

      end;

      assume that

       A4: x in N and

       A5: for y be Element of L st y in N holds [y, x] in the InternalRel of L implies [x, y] in the InternalRel of L;

      now

        assume ex y be set st y in N & y <> x & [y, x] in IR9;

        then

        consider y be set such that

         A6: y in N and y <> x and

         A7: [y, x] in IR9;

        reconsider y9 = y as Element of L by A7, ZFMISC_1: 87;

        

         A8: not [y, x] in (IR ~ ) by A7, XBOOLE_0:def 5;

         [y9, x] in IR implies [x, y9] in IR by A5, A6;

        hence contradiction by A7, A8, RELAT_1:def 7;

      end;

      hence thesis by A4, WAYBEL_4:def 25;

    end;

    theorem :: DICKSON:18

    for R,S be non empty RelStr, m be Function of R, S st R is quasi_ordered & S is antisymmetric & (S \~ ) is well_founded & for a,b be Element of R holds (a <= b implies (m . a) <= (m . b)) & ((m . a) = (m . b) implies [a, b] in ( EqRel R)) holds (R \~ ) is well_founded

    proof

      let R,S be non empty RelStr, m be Function of R, S such that

       A1: R is quasi_ordered and

       A2: S is antisymmetric and

       A3: (S \~ ) is well_founded and

       A4: for a,b be Element of R holds (a <= b implies (m . a) <= (m . b)) & ((m . a) = (m . b) implies [a, b] in ( EqRel R));

      set IR = the InternalRel of R, IS = the InternalRel of S;

      

       A5: IS is_antisymmetric_in the carrier of S by A2;

      now

        assume ex f be sequence of (R \~ ) st f is descending;

        then

        consider f be sequence of (R \~ ) such that

         A6: f is descending;

        reconsider f9 = f as sequence of R;

        deffunc F( Element of NAT ) = (m . (f9 . $1));

        consider g9 be sequence of the carrier of S such that

         A7: for k be Element of NAT holds (g9 . k) = F(k) from FUNCT_2:sch 4;

        reconsider g = g9 as sequence of (S \~ );

        now

          let n be Nat;

          reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

          

           A8: [(f . (n + 1)), (f . n)] in the InternalRel of (R \~ ) by A6, WELLFND1:def 6;

          

           A9: [(f . (n + 1)), (f . n)] in (IR \ (IR ~ )) by A6, WELLFND1:def 6;

          

           A10: not [(f . (n + 1)), (f . n)] in (IR ~ ) by A8, XBOOLE_0:def 5;

          

           A11: (g . n1) = (m . (f . n1)) by A7;

           A12:

          now

            assume (g . (n + 1)) = (g . n);

            then (m . (f . (n + 1))) = (m . (f . n)) by A7, A11;

            then [(f9 . (n + 1)), (f9 . n)] in ( EqRel R) by A4;

            then [(f . (n + 1)), (f . n)] in (IR /\ (IR ~ )) by A1, Def4;

            hence contradiction by A10, XBOOLE_0:def 4;

          end;

          hence (g . (n + 1)) <> (g . n);

          reconsider fn1 = (f . (n + 1)) as Element of R;

          reconsider fn = (f . n) as Element of R;

          

           A13: fn1 <= fn by A9;

          

           A14: (g9 . (n + 1)) = (m . fn1) by A7;

          (g9 . n1) = (m . fn) by A7;

          then (g9 . (n + 1)) <= (g9 . n) by A4, A13, A14;

          then

           A15: [(g . (n + 1)), (g . n)] in IS;

          then not [(g . n), (g . (n + 1))] in IS by A5, A12;

          then not [(g . (n + 1)), (g . n)] in (IS ~ ) by RELAT_1:def 7;

          hence [(g . (n + 1)), (g . n)] in the InternalRel of (S \~ ) by A15, XBOOLE_0:def 5;

        end;

        then g is descending by WELLFND1:def 6;

        hence contradiction by A3, WELLFND1: 14;

      end;

      hence thesis by WELLFND1: 14;

    end;

    definition

      let R be non empty RelStr, N be Subset of R;

      :: DICKSON:def8

      func min-classes N -> Subset-Family of R means

      : Def8: for x be set holds x in it iff ex y be Element of (R \~ ) st y is_minimal_wrt (N,the InternalRel of (R \~ )) & x = (( Class (( EqRel R),y)) /\ N);

      existence

      proof

        set IR9 = the InternalRel of (R \~ );

        set C = { (x /\ N) where x be Element of ( Class ( EqRel R)) : ex y be Element of (R \~ ) st x = ( Class (( EqRel R),y)) & y is_minimal_wrt (N,IR9) };

        now

          let x be object;

          assume x in C;

          then ex xx be Element of ( Class ( EqRel R)) st (x = (xx /\ N)) & (ex y be Element of (R \~ ) st xx = ( Class (( EqRel R),y)) & y is_minimal_wrt (N,IR9));

          hence x in ( bool the carrier of R);

        end;

        then

        reconsider C as Subset-Family of R by TARSKI:def 3;

        take C;

        let x be set;

        hereby

          assume x in C;

          then ex xx be Element of ( Class ( EqRel R)) st (x = (xx /\ N)) & (ex y be Element of (R \~ ) st xx = ( Class (( EqRel R),y)) & y is_minimal_wrt (N,IR9));

          hence ex y be Element of (R \~ ) st y is_minimal_wrt (N,IR9) & x = (( Class (( EqRel R),y)) /\ N);

        end;

        given y be Element of (R \~ ) such that

         A1: y is_minimal_wrt (N,IR9) and

         A2: x = (( Class (( EqRel R),y)) /\ N);

        reconsider y9 = y as Element of R;

        ( EqClass (( EqRel R),y9)) in ( Class ( EqRel R));

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        set IR = the InternalRel of (R \~ );

        let IT1,IT2 be Subset-Family of R such that

         A3: for x be set holds x in IT1 iff ex y be Element of (R \~ ) st y is_minimal_wrt (N,IR) & x = (( Class (( EqRel R),y)) /\ N) and

         A4: for x be set holds x in IT2 iff ex y be Element of (R \~ ) st y is_minimal_wrt (N,IR) & x = (( Class (( EqRel R),y)) /\ N);

        now

          let x be object;

          hereby

            assume x in IT1;

            then ex y be Element of (R \~ ) st y is_minimal_wrt (N,IR) & x = (( Class (( EqRel R),y)) /\ N) by A3;

            hence x in IT2 by A4;

          end;

          assume x in IT2;

          then ex y be Element of (R \~ ) st y is_minimal_wrt (N,IR) & x = (( Class (( EqRel R),y)) /\ N) by A4;

          hence x in IT1 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: DICKSON:19

    

     Th18: for R be non empty RelStr, N be Subset of R, x be set st R is quasi_ordered & x in ( min-classes N) holds for y be Element of (R \~ ) st y in x holds y is_minimal_wrt (N,the InternalRel of (R \~ ))

    proof

      let R be non empty RelStr, N be Subset of R, x be set such that

       A1: R is quasi_ordered and

       A2: x in ( min-classes N);

      set IR = the InternalRel of R, CR = the carrier of R;

      set IR9 = the InternalRel of (R \~ );

      let c be Element of (R \~ ) such that

       A3: c in x;

      consider b be Element of (R \~ ) such that

       A4: b is_minimal_wrt (N,IR9) and

       A5: x = (( Class (( EqRel R),b)) /\ N) by A2, Def8;

      c in ( Class (( EqRel R),b)) by A3, A5, XBOOLE_0:def 4;

      then [c, b] in ( EqRel R) by EQREL_1: 19;

      then [c, b] in (IR /\ (IR ~ )) by A1, Def4;

      then

       A6: [c, b] in IR by XBOOLE_0:def 4;

       A7:

      now

        assume ex d be set st d in N & d <> c & [d, c] in IR9;

        then

        consider d be set such that

         A8: d in N and d <> c and

         A9: [d, c] in IR9;

        

         A10: not [d, c] in (IR ~ ) by A9, XBOOLE_0:def 5;

        R is transitive by A1;

        then

         A11: IR is_transitive_in CR;

        then

         A12: [d, b] in IR by A6, A8, A9;

        now

          assume [d, b] in (IR ~ );

          then [b, d] in IR by RELAT_1:def 7;

          then [c, d] in IR by A6, A8, A11;

          hence contradiction by A10, RELAT_1:def 7;

        end;

        then

         A13: [d, b] in IR9 by A12, XBOOLE_0:def 5;

        b <> d by A6, A10, RELAT_1:def 7;

        hence contradiction by A4, A8, A13, WAYBEL_4:def 25;

      end;

      c in N by A3, A5, XBOOLE_0:def 4;

      hence thesis by A7, WAYBEL_4:def 25;

    end;

    theorem :: DICKSON:20

    

     Th19: for R be non empty RelStr holds (R \~ ) is well_founded iff for N be Subset of R st N <> {} holds ex x be object st x in ( min-classes N)

    proof

      let R be non empty RelStr;

      set CR = the carrier of R;

      set IR9 = the InternalRel of (R \~ ), CR9 = the carrier of (R \~ );

      hereby

        assume (R \~ ) is well_founded;

        then

         A1: IR9 is_well_founded_in CR9 by WELLFND1:def 2;

        let N be Subset of CR such that

         A2: N <> {} ;

        reconsider N9 = N as Subset of CR9;

        consider y be object such that

         A3: y in N9 and

         A4: (IR9 -Seg y) misses N9 by A1, A2, WELLORD1:def 3;

        

         A5: ((IR9 -Seg y) /\ N9) = {} by A4, XBOOLE_0:def 7;

        reconsider y as Element of (R \~ ) by A3;

        set x = (( Class (( EqRel R),y)) /\ N);

        now

          assume ex z be set st z in N & z <> y & [z, y] in IR9;

          then

          consider z be set such that

           A6: z in N and

           A7: z <> y and

           A8: [z, y] in IR9;

          z in (IR9 -Seg y) by A7, A8, WELLORD1: 1;

          hence contradiction by A5, A6, XBOOLE_0:def 4;

        end;

        then y is_minimal_wrt (N,IR9) by A3, WAYBEL_4:def 25;

        then x in ( min-classes N) by Def8;

        hence ex x be object st x in ( min-classes N);

      end;

      assume

       A9: for N be Subset of R st N <> {} holds ex x be object st x in ( min-classes N);

      now

        let N be set such that

         A10: N c= CR9 and

         A11: N <> {} ;

        reconsider N9 = N as Subset of R by A10;

        consider x be object such that

         A12: x in ( min-classes N9) by A9, A11;

        consider a be Element of (R \~ ) such that

         A13: a is_minimal_wrt (N9,IR9) and x = (( Class (( EqRel R),a)) /\ N9) by A12, Def8;

        reconsider a9 = a as object;

        take a9;

        thus a9 in N by A13, WAYBEL_4:def 25;

        now

          assume ((IR9 -Seg a9) /\ N) <> {} ;

          then

          consider z be object such that

           A14: z in ((IR9 -Seg a9) /\ N) by XBOOLE_0:def 1;

          

           A15: z in (IR9 -Seg a9) by A14, XBOOLE_0:def 4;

          

           A16: z in N by A14, XBOOLE_0:def 4;

          then

          reconsider z as Element of (R \~ ) by A10;

          

           A17: z <> a9 by A15, WELLORD1: 1;

           [z, a] in IR9 by A15, WELLORD1: 1;

          hence contradiction by A13, A16, A17, WAYBEL_4:def 25;

        end;

        hence (IR9 -Seg a9) misses N by XBOOLE_0:def 7;

      end;

      then IR9 is_well_founded_in CR9 by WELLORD1:def 3;

      hence thesis by WELLFND1:def 2;

    end;

    theorem :: DICKSON:21

    

     Th20: for R be non empty RelStr, N be Subset of R, y be Element of (R \~ ) st y is_minimal_wrt (N,the InternalRel of (R \~ )) holds ( min-classes N) is non empty

    proof

      let R be non empty RelStr, N be Subset of R, y be Element of (R \~ ) such that

       A1: y is_minimal_wrt (N,the InternalRel of (R \~ ));

      ex x be set st (x = (( Class (( EqRel R),y)) /\ N));

      hence thesis by A1, Def8;

    end;

    theorem :: DICKSON:22

    

     Th21: for R be non empty RelStr, N be Subset of R, x be set st x in ( min-classes N) holds x is non empty

    proof

      let R be non empty RelStr, N be Subset of R, x be set;

      assume x in ( min-classes N);

      then

      consider y be Element of (R \~ ) such that

       A1: y is_minimal_wrt (N,the InternalRel of (R \~ )) and

       A2: x = (( Class (( EqRel R),y)) /\ N) by Def8;

      

       A3: y in N by A1, WAYBEL_4:def 25;

      y in ( Class (( EqRel R),y)) by EQREL_1: 20;

      hence thesis by A2, A3, XBOOLE_0:def 4;

    end;

    theorem :: DICKSON:23

    

     Th22: for R be non empty RelStr st R is quasi_ordered holds R is connected & (R \~ ) is well_founded iff for N be non empty Subset of R holds ( card ( min-classes N)) = 1

    proof

      let R be non empty RelStr such that

       A1: R is quasi_ordered;

      set IR = the InternalRel of R, CR = the carrier of R;

      set IR9 = the InternalRel of (R \~ );

      hereby

        assume that

         A2: R is connected and

         A3: (R \~ ) is well_founded;

        let N be non empty Subset of CR;

        consider x be object such that

         A4: x in ( min-classes N) by A3, Th19;

        consider a be Element of (R \~ ) such that

         A5: a is_minimal_wrt (N,the InternalRel of (R \~ )) and

         A6: x = (( Class (( EqRel R),a)) /\ N) by A4, Def8;

        

         A7: a in N by A5, WAYBEL_4:def 25;

        now

          let y be object;

          hereby

            assume y in ( min-classes N);

            then

            consider b be Element of (R \~ ) such that

             A8: b is_minimal_wrt (N,IR9) and

             A9: y = (( Class (( EqRel R),b)) /\ N) by Def8;

            

             A10: b in N by A8, WAYBEL_4:def 25;

            reconsider a9 = a as Element of R;

            reconsider b9 = b as Element of R;

             A11:

            now

              per cases by A2, WAYBEL_0:def 29;

                suppose

                 A12: a9 <= b9;

                then

                 A13: [a, b] in IR;

                now

                  per cases ;

                    suppose a = b;

                    hence [b, a] in IR by A12;

                  end;

                    suppose

                     A14: a <> b;

                    now

                      assume not [b, a] in IR;

                      then not [a, b] in (IR ~ ) by RELAT_1:def 7;

                      then [a, b] in (IR \ (IR ~ )) by A13, XBOOLE_0:def 5;

                      hence contradiction by A7, A8, A14, WAYBEL_4:def 25;

                    end;

                    hence [b, a] in IR;

                  end;

                end;

                hence [a, b] in IR & [b, a] in IR by A12;

              end;

                suppose

                 A15: b9 <= a9;

                then

                 A16: [b, a] in IR;

                now

                  per cases ;

                    suppose a = b;

                    hence [a, b] in IR by A15;

                  end;

                    suppose

                     A17: a <> b;

                    now

                      assume not [a, b] in IR;

                      then not [b, a] in (IR ~ ) by RELAT_1:def 7;

                      then [b, a] in (IR \ (IR ~ )) by A16, XBOOLE_0:def 5;

                      hence contradiction by A5, A10, A17, WAYBEL_4:def 25;

                    end;

                    hence [a, b] in IR;

                  end;

                end;

                hence [a, b] in IR & [b, a] in IR by A15;

              end;

            end;

            then [b, a] in (IR ~ ) by RELAT_1:def 7;

            then [b, a] in (IR /\ (IR ~ )) by A11, XBOOLE_0:def 4;

            then [b, a] in ( EqRel R) by A1, Def4;

            then b in ( Class (( EqRel R),a)) by EQREL_1: 19;

            then ( Class (( EqRel R),b)) = ( Class (( EqRel R),a)) by EQREL_1: 23;

            hence y in {x} by A6, A9, TARSKI:def 1;

          end;

          assume y in {x};

          then y = (( Class (( EqRel R),a)) /\ N) by A6, TARSKI:def 1;

          hence y in ( min-classes N) by A5, Def8;

        end;

        then ( min-classes N) = {x} by TARSKI: 2;

        hence ( card ( min-classes N)) = 1 by CARD_1: 30;

      end;

      assume

       A18: for N be non empty Subset of R holds ( card ( min-classes N)) = 1;

      now

        let a,b be Element of R;

        assume that

         A19: not a <= b and

         A20: not a >= b;

        

         A21: not [a, b] in IR by A19;

        then

         A22: not [b, a] in (IR ~ ) by RELAT_1:def 7;

         not [b, a] in IR by A20;

        then

         A23: not [a, b] in (IR ~ ) by RELAT_1:def 7;

        set N9 = {a, b};

        set MCN = { {a}, {b}};

        now

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          hereby

            assume x in ( min-classes N9);

            then

            consider y be Element of (R \~ ) such that

             A24: y is_minimal_wrt (N9,IR9) and

             A25: x = (( Class (( EqRel R),y)) /\ N9) by Def8;

            

             A26: y in N9 by A24, WAYBEL_4:def 25;

            per cases by A26, TARSKI:def 2;

              suppose

               A27: y = a;

              now

                let z be object;

                hereby

                  assume

                   A28: z in xx;

                  then

                   A29: z in ( Class (( EqRel R),a)) by A25, A27, XBOOLE_0:def 4;

                  

                   A30: z in N9 by A25, A28, XBOOLE_0:def 4;

                  now

                    per cases by A30, TARSKI:def 2;

                      suppose z = a;

                      hence z in {a} by TARSKI:def 1;

                    end;

                      suppose z = b;

                      then [b, a] in ( EqRel R) by A29, EQREL_1: 19;

                      then [b, a] in (IR /\ (IR ~ )) by A1, Def4;

                      hence z in {a} by A22, XBOOLE_0:def 4;

                    end;

                  end;

                  hence z in {a};

                end;

                assume z in {a};

                then

                 A31: z = a by TARSKI:def 1;

                then

                 A32: z in N9 by TARSKI:def 2;

                z in ( Class (( EqRel R),a)) by A31, EQREL_1: 20;

                hence z in xx by A25, A27, A32, XBOOLE_0:def 4;

              end;

              then x = {a} by TARSKI: 2;

              hence x in MCN by TARSKI:def 2;

            end;

              suppose

               A33: y = b;

              now

                let z be object;

                hereby

                  assume

                   A34: z in xx;

                  then

                   A35: z in ( Class (( EqRel R),b)) by A25, A33, XBOOLE_0:def 4;

                  

                   A36: z in N9 by A25, A34, XBOOLE_0:def 4;

                  now

                    per cases by A36, TARSKI:def 2;

                      suppose z = b;

                      hence z in {b} by TARSKI:def 1;

                    end;

                      suppose z = a;

                      then [a, b] in ( EqRel R) by A35, EQREL_1: 19;

                      then [a, b] in (IR /\ (IR ~ )) by A1, Def4;

                      hence z in {b} by A21, XBOOLE_0:def 4;

                    end;

                  end;

                  hence z in {b};

                end;

                assume z in {b};

                then

                 A37: z = b by TARSKI:def 1;

                then

                 A38: z in N9 by TARSKI:def 2;

                z in ( Class (( EqRel R),b)) by A37, EQREL_1: 20;

                hence z in xx by A25, A33, A38, XBOOLE_0:def 4;

              end;

              then x = {b} by TARSKI: 2;

              hence x in MCN by TARSKI:def 2;

            end;

          end;

          assume

           A39: x in MCN;

          per cases by A39, TARSKI:def 2;

            suppose

             A40: x = {a};

            now

              reconsider a9 = a as Element of (R \~ );

              take a9;

              

               A41: a9 in N9 by TARSKI:def 2;

              now

                assume ex y be set st y in N9 & y <> a9 & [y, a9] in IR9;

                then

                consider y be set such that

                 A42: y in N9 and

                 A43: y <> a9 and

                 A44: [y, a9] in IR9;

                y = b by A42, A43, TARSKI:def 2;

                hence contradiction by A20, A44;

              end;

              hence a9 is_minimal_wrt (N9,the InternalRel of (R \~ )) by A41, WAYBEL_4:def 25;

              now

                let z be object;

                hereby

                  assume z in xx;

                  then

                   A45: z = a by A40, TARSKI:def 1;

                  then z in ( Class (( EqRel R),a)) by EQREL_1: 20;

                  hence z in (( Class (( EqRel R),a)) /\ N9) by A41, A45, XBOOLE_0:def 4;

                end;

                assume

                 A46: z in (( Class (( EqRel R),a)) /\ N9);

                then

                 A47: z in ( Class (( EqRel R),a)) by XBOOLE_0:def 4;

                

                 A48: z in N9 by A46, XBOOLE_0:def 4;

                per cases by A48, TARSKI:def 2;

                  suppose z = a;

                  hence z in xx by A40, TARSKI:def 1;

                end;

                  suppose z = b;

                  then [b, a] in ( EqRel R) by A47, EQREL_1: 19;

                  then [b, a] in (IR /\ (IR ~ )) by A1, Def4;

                  hence z in xx by A22, XBOOLE_0:def 4;

                end;

              end;

              hence x = (( Class (( EqRel R),a9)) /\ N9) by TARSKI: 2;

            end;

            hence x in ( min-classes N9) by Def8;

          end;

            suppose

             A49: x = {b};

            now

              reconsider b9 = b as Element of (R \~ );

              take b9;

              

               A50: b9 in N9 by TARSKI:def 2;

              now

                assume ex y be set st y in N9 & y <> b9 & [y, b9] in IR9;

                then

                consider y be set such that

                 A51: y in N9 and

                 A52: y <> b9 and

                 A53: [y, b9] in IR9;

                y = a by A51, A52, TARSKI:def 2;

                hence contradiction by A19, A53;

              end;

              hence b9 is_minimal_wrt (N9,the InternalRel of (R \~ )) by A50, WAYBEL_4:def 25;

              now

                let z be object;

                hereby

                  assume z in xx;

                  then

                   A54: z = b by A49, TARSKI:def 1;

                  then z in ( Class (( EqRel R),b)) by EQREL_1: 20;

                  hence z in (( Class (( EqRel R),b)) /\ N9) by A50, A54, XBOOLE_0:def 4;

                end;

                assume

                 A55: z in (( Class (( EqRel R),b)) /\ N9);

                then

                 A56: z in ( Class (( EqRel R),b)) by XBOOLE_0:def 4;

                

                 A57: z in N9 by A55, XBOOLE_0:def 4;

                per cases by A57, TARSKI:def 2;

                  suppose z = b;

                  hence z in xx by A49, TARSKI:def 1;

                end;

                  suppose z = a;

                  then [a, b] in ( EqRel R) by A56, EQREL_1: 19;

                  then [a, b] in (IR /\ (IR ~ )) by A1, Def4;

                  hence z in xx by A23, XBOOLE_0:def 4;

                end;

              end;

              hence x = (( Class (( EqRel R),b9)) /\ N9) by TARSKI: 2;

            end;

            hence x in ( min-classes N9) by Def8;

          end;

        end;

        then ( min-classes N9) = MCN by TARSKI: 2;

        then

         A58: ( card MCN) = 1 by A18;

        now

          assume {a} = {b};

          then

           A59: a = b by ZFMISC_1: 3;

          R is reflexive by A1;

          then IR is_reflexive_in CR;

          hence contradiction by A21, A59;

        end;

        hence contradiction by A58, CARD_2: 57;

      end;

      hence R is connected by WAYBEL_0:def 29;

      now

        let N be Subset of R;

        assume N <> {} ;

        then ( card ( min-classes N)) = 1 by A18;

        then ( min-classes N) <> {} ;

        hence ex x be object st x in ( min-classes N) by XBOOLE_0:def 1;

      end;

      hence thesis by Th19;

    end;

    theorem :: DICKSON:24

    for R be non empty Poset holds the InternalRel of R well_orders the carrier of R iff for N be non empty Subset of R holds ( card ( min-classes N)) = 1

    proof

      let R be non empty Poset;

      set IR = the InternalRel of R, CR = the carrier of R;

      

       A1: R is quasi_ordered;

      hereby

        assume

         A2: IR well_orders CR;

        then

         A3: IR is_reflexive_in CR by WELLORD1:def 5;

        

         A4: IR is_connected_in CR by A2, WELLORD1:def 5;

        

         A5: IR is_well_founded_in CR by A2, WELLORD1:def 5;

        IR is_strongly_connected_in CR by A3, A4, ORDERS_1: 7;

        then

         A6: R is connected by Th4;

        R is well_founded by A5, WELLFND1:def 2;

        then (R \~ ) is well_founded by Th14;

        hence for N be non empty Subset of R holds ( card ( min-classes N)) = 1 by A1, A6, Th22;

      end;

      assume

       A7: for N be non empty Subset of R holds ( card ( min-classes N)) = 1;

      then

       A8: R is connected by A1, Th22;

      

       A9: (R \~ ) is well_founded by A1, A7, Th22;

      

       A10: IR is_strongly_connected_in CR by A8, Th4;

      

       A11: R is well_founded by A9, Th15;

      

       A12: IR is_reflexive_in CR by ORDERS_2:def 2;

      

       A13: IR is_transitive_in CR by ORDERS_2:def 3;

      

       A14: IR is_antisymmetric_in CR by ORDERS_2:def 4;

      

       A15: IR is_connected_in CR by A10;

      IR is_well_founded_in CR by A11, WELLFND1:def 2;

      hence thesis by A12, A13, A14, A15, WELLORD1:def 5;

    end;

    definition

      let R be RelStr, N be Subset of R, B be set;

      :: DICKSON:def9

      pred B is_Dickson-basis_of N,R means B c= N & for a be Element of R st a in N holds ex b be Element of R st b in B & b <= a;

    end

    theorem :: DICKSON:25

    for R be RelStr holds {} is_Dickson-basis_of (( {} the carrier of R),R);

    theorem :: DICKSON:26

    

     Th25: for R be non empty RelStr, N be non empty Subset of R, B be set st B is_Dickson-basis_of (N,R) holds B is non empty

    proof

      let R be non empty RelStr, N be non empty Subset of R, B be set;

      assume

       A1: B is_Dickson-basis_of (N,R);

      set a = the Element of N;

      ex b be Element of R st (b in B) & (b <= a) by A1;

      hence thesis;

    end;

    definition

      let R be RelStr;

      :: DICKSON:def10

      attr R is Dickson means for N be Subset of R holds ex B be set st B is_Dickson-basis_of (N,R) & B is finite;

    end

    theorem :: DICKSON:27

    

     Th26: for R be non empty RelStr st (R \~ ) is well_founded & R is connected holds R is Dickson

    proof

      let R be non empty RelStr such that

       A1: (R \~ ) is well_founded and

       A2: R is connected;

      set IR9 = the InternalRel of (R \~ ), CR9 = the carrier of (R \~ );

      set IR = the InternalRel of R, CR = the carrier of R;

      let N be Subset of CR;

      per cases ;

        suppose

         A3: N = ( {} CR);

        take B = {} ;

        thus B is_Dickson-basis_of (N,R) by A3;

        thus thesis;

      end;

        suppose

         A4: N <> ( {} CR);

        IR9 is_well_founded_in CR9 by A1, WELLFND1:def 2;

        then

        consider b be object such that

         A5: b in N and

         A6: (IR9 -Seg b) misses N by A4, WELLORD1:def 3;

        

         A7: ((IR9 -Seg b) /\ N) = {} by A6, XBOOLE_0:def 7;

        take B = {b};

        reconsider b as Element of N by A5;

        thus B is_Dickson-basis_of (N,R)

        proof

           {b} is Subset of N by A4, SUBSET_1: 33;

          hence B c= N;

          let a be Element of R such that

           A8: a in N;

          reconsider b as Element of R by A5;

          take b;

          thus b in B by TARSKI:def 1;

          per cases by A2, WAYBEL_0:def 29;

            suppose b <= a;

            hence thesis;

          end;

            suppose

             A9: a <= b;

            then

             A10: [a, b] in IR;

            now

              per cases ;

                suppose a = b;

                hence thesis by A9;

              end;

                suppose

                 A11: not a = b;

                now

                  per cases ;

                    suppose [a, b] in IR9;

                    then a in (IR9 -Seg b) by A11, WELLORD1: 1;

                    hence thesis by A7, A8, XBOOLE_0:def 4;

                  end;

                    suppose not [a, b] in IR9;

                    then [a, b] in (IR ~ ) by A10, XBOOLE_0:def 5;

                    then [b, a] in IR by RELAT_1:def 7;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        thus thesis;

      end;

    end;

    theorem :: DICKSON:28

    

     Th27: for R,S be RelStr st the InternalRel of R c= the InternalRel of S & R is Dickson & the carrier of R = the carrier of S holds S is Dickson

    proof

      let r,s be RelStr such that

       A1: the InternalRel of r c= the InternalRel of s and

       A2: r is Dickson and

       A3: the carrier of r = the carrier of s;

      let N be Subset of s;

      reconsider N9 = N as Subset of r by A3;

      consider B be set such that

       A4: B is_Dickson-basis_of (N9,r) and

       A5: B is finite by A2;

      take B;

      thus B c= N by A4;

      hereby

        let a be Element of s such that

         A6: a in N;

        reconsider a9 = a as Element of r by A3;

        consider b be Element of r such that

         A7: b in B and

         A8: b <= a9 by A4, A6;

        reconsider b9 = b as Element of s by A3;

        take b9;

         [b, a9] in the InternalRel of r by A8;

        hence b9 in B & b9 <= a by A1, A7;

      end;

      thus thesis by A5;

    end;

    definition

      let f be Function, b be set;

      :: DICKSON:def11

      func f mindex b -> Element of NAT means

      : Def11: (f . it ) = b & for i be Element of NAT st (f . i) = b holds it <= i;

      existence

      proof

        set N = { i where i be Element of NAT : (f . i) = b };

        consider x be object such that

         A3: x in NAT and

         A4: (f . x) = b by A1, A2, FUNCT_1:def 3;

        reconsider x as Element of NAT by A3;

        

         A5: x in N by A4;

        now

          let x be object;

          assume x in N;

          then ex i be Element of NAT st (x = i) & ((f . i) = b);

          hence x in NAT ;

        end;

        then

        reconsider N as non empty Subset of NAT by A5, TARSKI:def 3;

        take I = ( min N);

        I in N by XXREAL_2:def 7;

        then ex II be Element of NAT st (II = I) & ((f . II) = b);

        hence (f . I) = b;

        let i be Element of NAT ;

        assume (f . i) = b;

        then i in N;

        hence thesis by XXREAL_2:def 7;

      end;

      uniqueness

      proof

        let IT1,IT2 be Element of NAT such that

         A6: (f . IT1) = b and

         A7: for i be Element of NAT st (f . i) = b holds IT1 <= i and

         A8: (f . IT2) = b and

         A9: for i be Element of NAT st (f . i) = b holds IT2 <= i;

        assume

         A10: IT1 <> IT2;

        per cases by A10, XXREAL_0: 1;

          suppose IT1 < IT2;

          hence contradiction by A6, A9;

        end;

          suppose IT1 > IT2;

          hence contradiction by A7, A8;

        end;

      end;

    end

    definition

      let R be non empty 1-sorted, f be sequence of R, b be set, m be Element of NAT ;

      assume

       A1: ex j be Element of NAT st m < j & (f . j) = b;

      :: DICKSON:def12

      func f mindex (b,m) -> Element of NAT means

      : Def12: (f . it ) = b & m < it & for i be Element of NAT st m < i & (f . i) = b holds it <= i;

      existence

      proof

        set N = { i where i be Element of NAT : m < i & (f . i) = b };

        consider j be Element of NAT such that

         A2: m < j and

         A3: (f . j) = b by A1;

        

         A4: j in N by A2, A3;

        now

          let x be object;

          assume x in N;

          then ex i be Element of NAT st (x = i) & (m < i) & ((f . i) = b);

          hence x in NAT ;

        end;

        then

        reconsider N as non empty Subset of NAT by A4, TARSKI:def 3;

        take I = ( min N);

        I in N by XXREAL_2:def 7;

        then ex II be Element of NAT st (II = I) & (m < II) & ((f . II) = b);

        hence (f . I) = b & m < I;

        let i be Element of NAT such that

         A5: m < i and

         A6: (f . i) = b;

        i in N by A5, A6;

        hence thesis by XXREAL_2:def 7;

      end;

      uniqueness

      proof

        let IT1,IT2 be Element of NAT such that

         A7: (f . IT1) = b and

         A8: m < IT1 and

         A9: for i be Element of NAT st m < i & (f . i) = b holds IT1 <= i and

         A10: (f . IT2) = b and

         A11: m < IT2 and

         A12: for i be Element of NAT st m < i & (f . i) = b holds IT2 <= i;

        assume

         A13: IT1 <> IT2;

        per cases by A13, XXREAL_0: 1;

          suppose IT1 < IT2;

          hence contradiction by A7, A8, A12;

        end;

          suppose IT1 > IT2;

          hence contradiction by A9, A10, A11;

        end;

      end;

    end

    theorem :: DICKSON:29

    

     Th28: for R be non empty RelStr st R is Dickson holds for f be sequence of R holds ex i,j be Nat st i < j & (f . i) <= (f . j)

    proof

      let R be non empty RelStr such that

       A1: R is Dickson;

      let f be sequence of R;

      set N = ( rng f);

      

       A2: ( dom f) = NAT by FUNCT_2:def 1;

      consider B be set such that

       A3: B is_Dickson-basis_of (N,R) and

       A4: B is finite by A1;

      reconsider B as finite non empty set by A3, A4, Th25;

      defpred P[ set] means not contradiction;

      deffunc F( set) = (f mindex $1);

      set BI = { F(b) where b be Element of B : P[b] };

      

       A5: BI is finite from PRE_CIRC:sch 1;

      set b = the Element of B;

      

       A6: (f mindex b) in BI;

      now

        let x be object;

        assume x in BI;

        then ex b be Element of B st (x = (f mindex b));

        hence x in NAT ;

      end;

      then

      reconsider BI as finite non empty Subset of NAT by A5, A6, TARSKI:def 3;

      reconsider mB = ( max BI) as Element of NAT by ORDINAL1:def 12;

      set j = (mB + 1);

      reconsider fj = (f . j) as Element of R;

      fj in N by A2, FUNCT_1: 3;

      then

      consider b be Element of R such that

       A7: b in B and

       A8: b <= fj by A3;

      

       A9: B c= N by A3;

      take i = (f mindex b);

      take j;

      i in BI by A7;

      then i <= ( max BI) by XXREAL_2:def 8;

      hence i < j by NAT_1: 13;

      ( dom f) = NAT by NORMSP_1: 12;

      hence thesis by A7, A8, A9, Def11;

    end;

    theorem :: DICKSON:30

    

     Th29: for R be RelStr, N be Subset of R, x be Element of (R \~ ) st R is quasi_ordered & x in N & ((the InternalRel of R -Seg x) /\ N) c= ( Class (( EqRel R),x)) holds x is_minimal_wrt (N,the InternalRel of (R \~ ))

    proof

      let R be RelStr, N be Subset of R, x be Element of (R \~ ) such that

       A1: R is quasi_ordered and

       A2: x in N and

       A3: ((the InternalRel of R -Seg x) /\ N) c= ( Class (( EqRel R),x));

      set IR = the InternalRel of R;

      set IR9 = the InternalRel of (R \~ );

      now

        assume ex y be set st y in N & y <> x & [y, x] in IR9;

        then

        consider y be set such that

         A4: y in N and

         A5: y <> x and

         A6: [y, x] in IR9;

        

         A7: not [y, x] in (IR ~ ) by A6, XBOOLE_0:def 5;

        y in (IR -Seg x) by A5, A6, WELLORD1: 1;

        then y in ((IR -Seg x) /\ N) by A4, XBOOLE_0:def 4;

        then [y, x] in ( EqRel R) by A3, EQREL_1: 19;

        then [y, x] in (IR /\ (IR ~ )) by A1, Def4;

        hence contradiction by A7, XBOOLE_0:def 4;

      end;

      hence thesis by A2, WAYBEL_4:def 25;

    end;

    theorem :: DICKSON:31

    

     Th30: for R be non empty RelStr st R is quasi_ordered & (for f be sequence of R holds ex i,j be Nat st i < j & (f . i) <= (f . j)) holds for N be non empty Subset of R holds ( min-classes N) is finite & ( min-classes N) is non empty

    proof

      let R be non empty RelStr such that

       A1: R is quasi_ordered and

       A2: for f be sequence of R holds ex i,j be Nat st i < j & (f . i) <= (f . j);

      set IR = the InternalRel of R;

      set IR9 = the InternalRel of (R \~ );

      

       A3: R is transitive by A1;

      let N be non empty Subset of R such that

       A4: not (( min-classes N) is finite & ( min-classes N) is non empty);

      per cases by A4;

        suppose

         A5: ( min-classes N) is infinite;

        then

        reconsider MCN = ( min-classes N) as infinite set;

        consider f be sequence of ( min-classes N) such that

         A6: f is one-to-one by A5, Th2;

        deffunc F( object) = the Element of (f . $1);

         A7:

        now

          let x be object;

          assume x in NAT ;

          then

          reconsider x9 = x as Element of NAT ;

          (f . x9) is Element of ( min-classes N);

          then

           A8: (f . x) in MCN;

          then (f . x) is non empty by Th21;

          then the Element of (f . x9) in (f . x);

          hence F(x) in the carrier of R by A8;

        end;

        consider g be sequence of the carrier of R such that

         A9: for x be object st x in NAT holds (g . x) = F(x) from FUNCT_2:sch 2( A7);

        reconsider g as sequence of R;

        consider i,j be Nat such that

         A10: i < j and

         A11: (g . i) <= (g . j) by A2;

        reconsider gi = (g . i), gj = (g . j) as Element of (R \~ );

        

         A12: [gi, gj] in IR by A11;

        

         A13: (f . i) in MCN;

        then

         A14: (f . i) is non empty by Th21;

        

         A15: (f . j) in MCN;

        then

         A16: (f . j) is non empty by Th21;

        j in NAT by ORDINAL1:def 12;

        then

         A17: (g . j) = the Element of (f . j) by A9;

        i in NAT by ORDINAL1:def 12;

        then

         A18: (g . i) = the Element of (f . i) by A9;

        

         A19: gj is_minimal_wrt (N,the InternalRel of (R \~ )) by A1, A15, A16, A17, Th18;

        gi is_minimal_wrt (N,the InternalRel of (R \~ )) by A1, A13, A14, A18, Th18;

        then

         A20: gi in N by WAYBEL_4:def 25;

         A21:

        now

          per cases ;

            suppose gi = gj;

            hence [gi, gj] in (IR ~ ) by A12, RELAT_1:def 7;

          end;

            suppose

             A22: gi <> gj;

            now

              assume not [gi, gj] in (IR ~ );

              then [gi, gj] in (IR \ (IR ~ )) by A12, XBOOLE_0:def 5;

              hence contradiction by A19, A20, A22, WAYBEL_4:def 25;

            end;

            hence [gi, gj] in (IR ~ );

          end;

        end;

         [gi, gj] in IR by A11;

        then [gi, gj] in (IR /\ (IR ~ )) by A21, XBOOLE_0:def 4;

        then [gi, gj] in ( EqRel R) by A1, Def4;

        then gi in ( Class (( EqRel R),gj)) by EQREL_1: 19;

        then

         A23: ( Class (( EqRel R),gj)) = ( Class (( EqRel R),gi)) by EQREL_1: 23;

        consider mj be Element of (R \~ ) such that mj is_minimal_wrt (N,IR9) and

         A24: (f . j) = (( Class (( EqRel R),mj)) /\ N) by A15, Def8;

        consider mi be Element of (R \~ ) such that mi is_minimal_wrt (N,IR9) and

         A25: (f . i) = (( Class (( EqRel R),mi)) /\ N) by A13, Def8;

        gj in ( Class (( EqRel R),mj)) by A16, A17, A24, XBOOLE_0:def 4;

        then

         A26: ( Class (( EqRel R),gj)) = ( Class (( EqRel R),mj)) by EQREL_1: 23;

        

         A27: i in NAT by ORDINAL1:def 12;

        

         A28: j in NAT by ORDINAL1:def 12;

        gi in ( Class (( EqRel R),mi)) by A14, A18, A25, XBOOLE_0:def 4;

        then (f . i) = (f . j) by A23, A24, A25, A26, EQREL_1: 23;

        hence contradiction by A5, A6, A10, FUNCT_2: 19, A27, A28;

      end;

        suppose

         A29: ( min-classes N) is empty;

        deffunc F( set, set) = the Element of (((IR -Seg $2) /\ N) \ ( Class (( EqRel R),$2)));

        consider f be Function such that

         A30: ( dom f) = NAT and

         A31: (f . 0 ) = the Element of N and

         A32: for n be Nat holds (f . (n + 1)) = F(n,.) from NAT_1:sch 11;

        defpred P[ Nat] means (f . $1) in N;

        

         A33: P[ 0 ] by A31;

         A34:

        now

          let i be Nat such that

           A35: P[i];

          reconsider fi = (f . i) as Element of (R \~ ) by A35;

          set IC = (((IR -Seg fi) /\ N) \ ( Class (( EqRel R),fi)));

          

           A36: (f . (i + 1)) = the Element of (((IR -Seg (f . i)) /\ N) \ ( Class (( EqRel R),(f . i)))) by A32;

          now

            assume IC is empty;

            then ((IR -Seg fi) /\ N) c= ( Class (( EqRel R),fi)) by XBOOLE_1: 37;

            hence contradiction by A1, A29, A35, Th20, Th29;

          end;

          then (f . (i + 1)) in ((IR -Seg (f . i)) /\ N) by A36, XBOOLE_0:def 5;

          hence P[(i + 1)] by XBOOLE_0:def 4;

        end;

        

         A37: for i be Nat holds P[i] from NAT_1:sch 2( A33, A34);

        now

          let x be object;

          assume x in NAT ;

          then (f . x) in N by A37;

          hence (f . x) in the carrier of R;

        end;

        then

        reconsider f as sequence of R by A30, FUNCT_2: 3;

         A38:

        now

          let i be Nat;

          defpred P[ Nat] means i < $1 implies (f . i) >= (f . $1);

          

           A39: P[ 0 ] by NAT_1: 2;

          

           A40: for j be Nat st P[j] holds P[(j + 1)]

          proof

            let j be Nat such that

             A41: i < j implies (f . i) >= (f . j) and

             A42: i < (j + 1);

            

             A43: i <= j by A42, NAT_1: 13;

            reconsider fj = (f . j), fj1 = (f . (j + 1)) as Element of (R \~ );

            set IC = (((IR -Seg fj) /\ N) \ ( Class (( EqRel R),fj)));

            

             A44: fj in N by A37;

            

             A45: fj1 = the Element of IC by A32;

            now

              assume IC is empty;

              then ((IR -Seg fj) /\ N) c= ( Class (( EqRel R),fj)) by XBOOLE_1: 37;

              hence contradiction by A1, A29, A44, Th20, Th29;

            end;

            then fj1 in ((IR -Seg fj) /\ N) by A45, XBOOLE_0:def 5;

            then fj1 in (IR -Seg fj) by XBOOLE_0:def 4;

            then

             A46: [fj1, fj] in IR by WELLORD1: 1;

            then

             A47: (f . j) >= (f . (j + 1));

            per cases by A43, XXREAL_0: 1;

              suppose i < j;

              hence thesis by A3, A41, A47, ORDERS_2: 3;

            end;

              suppose i = j;

              hence thesis by A46;

            end;

          end;

          thus for j be Nat holds P[j] from NAT_1:sch 2( A39, A40);

        end;

        now

          let i be Nat;

          defpred P[ Nat] means i < $1 implies not (f . i) <= (f . $1);

          

           A48: P[ 0 ] by NAT_1: 2;

          

           A49: for j be Nat st P[j] holds P[(j + 1)]

          proof

            let j be Nat such that i < j implies not (f . i) <= (f . j) and

             A50: i < (j + 1);

            

             A51: i <= j by A50, NAT_1: 13;

            reconsider fj = (f . j), fj1 = (f . (j + 1)) as Element of (R \~ );

            

             A52: fj in N by A37;

            per cases by A51, XXREAL_0: 1;

              suppose

               A53: i < j;

              assume

               A54: (f . i) <= (f . (j + 1));

              j < (j + 1) by NAT_1: 13;

              then

               A55: (f . j) >= (f . (j + 1)) by A38;

              (f . i) >= (f . j) by A38, A53;

              then (f . j) <= (f . (j + 1)) by A3, A54, ORDERS_2: 3;

              then

               A56: fj1 in ( Class (( EqRel R),fj)) by A1, A55, Th7;

              set IC = (((IR -Seg fj) /\ N) \ ( Class (( EqRel R),fj)));

              

               A57: fj1 = the Element of IC by A32;

              now

                assume IC is empty;

                then ((IR -Seg fj) /\ N) c= ( Class (( EqRel R),fj)) by XBOOLE_1: 37;

                hence contradiction by A1, A29, A52, Th20, Th29;

              end;

              hence contradiction by A56, A57, XBOOLE_0:def 5;

            end;

              suppose

               A58: i = j;

              assume

               A59: (f . i) <= (f . (j + 1));

              j < (j + 1) by NAT_1: 13;

              then (f . (j + 1)) <= (f . j) by A38;

              then

               A60: fj1 in ( Class (( EqRel R),fj)) by A1, A58, A59, Th7;

              set IC = (((IR -Seg fj) /\ N) \ ( Class (( EqRel R),fj)));

              

               A61: fj1 = the Element of IC by A32;

              now

                assume IC is empty;

                then ((IR -Seg fj) /\ N) c= ( Class (( EqRel R),fj)) by XBOOLE_1: 37;

                hence contradiction by A1, A29, A52, Th20, Th29;

              end;

              hence contradiction by A60, A61, XBOOLE_0:def 5;

            end;

          end;

          thus for j be Nat holds P[j] from NAT_1:sch 2( A48, A49);

        end;

        hence contradiction by A2;

      end;

    end;

    theorem :: DICKSON:32

    

     Th31: for R be non empty RelStr st R is quasi_ordered & (for N be non empty Subset of R holds ( min-classes N) is finite & ( min-classes N) is non empty) holds R is Dickson

    proof

      let R be non empty RelStr such that

       A1: R is quasi_ordered and

       A2: for N be non empty Subset of R holds ( min-classes N) is finite & ( min-classes N) is non empty;

      

       A3: R is transitive by A1;

      

       A4: R is reflexive by A1;

      set IR = the InternalRel of R, CR = the carrier of R;

      set IR9 = the InternalRel of (R \~ );

      let N be Subset of CR;

      per cases ;

        suppose

         A5: N = ( {} CR);

        take B = {} ;

        thus B is_Dickson-basis_of (N,R) by A5;

        thus thesis;

      end;

        suppose not N is empty;

        then

        reconsider N9 = N as non empty Subset of CR;

        reconsider MCN9 = ( min-classes N9) as finite non empty Subset-Family of CR by A2;

        take B = the set of all the Element of x where x be Element of MCN9;

        thus B is_Dickson-basis_of (N,R)

        proof

          now

            let x be object;

            assume x in B;

            then

            consider y be Element of MCN9 such that

             A6: x = the Element of y;

            

             A7: ex z be Element of (R \~ ) st (z is_minimal_wrt (N,IR9)) & (y = (( Class (( EqRel R),z)) /\ N)) by Def8;

            y is non empty by Th21;

            hence x in N by A6, A7, XBOOLE_0:def 4;

          end;

          hence B c= N;

          let a be Element of R such that

           A8: a in N;

          defpred P[ Element of R] means $1 <= a;

          set NN9 = { d where d be Element of N9 : P[d] };

          

           A9: NN9 is Subset of N9 from DOMAIN_1:sch 7;

          a <= a by A4, ORDERS_2: 1;

          then a in NN9 by A8;

          then

          reconsider NN9 as non empty Subset of CR by A9, XBOOLE_1: 1;

          set m = the Element of ( min-classes NN9);

          

           A10: ( min-classes NN9) is non empty by A2;

          then

          reconsider m9 = m as non empty set by Th21;

          set c = the Element of m9;

          consider y be Element of (R \~ ) such that y is_minimal_wrt (NN9,IR9) and

           A11: m9 = (( Class (( EqRel R),y)) /\ NN9) by A10, Def8;

          

           A12: c in ( Class (( EqRel R),y)) by A11, XBOOLE_0:def 4;

          

           A13: c in NN9 by A11, XBOOLE_0:def 4;

          reconsider c as Element of (R \~ ) by A12;

          reconsider c9 = c as Element of R;

          

           A14: ex d be Element of N9 st (c = d) & (d <= a) by A13;

          

           A15: c is_minimal_wrt (NN9,IR9) by A1, A10, Th18;

          now

            assume not c is_minimal_wrt (N,IR9);

            then

            consider w be set such that

             A16: w in N and

             A17: w <> c and

             A18: [w, c] in IR9 by A14, WAYBEL_4:def 25;

            reconsider w9 = w as Element of R by A18, ZFMISC_1: 87;

            w9 <= c9 by A18;

            then w9 <= a by A3, A14, ORDERS_2: 3;

            then w9 in NN9 by A16;

            hence contradiction by A15, A17, A18, WAYBEL_4:def 25;

          end;

          then

           A19: (( Class (( EqRel R),c)) /\ N) in ( min-classes N) by Def8;

          then

           A20: (( Class (( EqRel R),c)) /\ N) is non empty by Th21;

          set t = the Element of (( Class (( EqRel R),c)) /\ N);

          t in N by A20, XBOOLE_0:def 4;

          then

          reconsider t as Element of R;

          take t;

          thus t in B by A19;

          t in ( Class (( EqRel R),c)) by A20, XBOOLE_0:def 4;

          then [t, c] in ( EqRel R) by EQREL_1: 19;

          then [t, c] in (IR /\ (IR ~ )) by A1, Def4;

          then [t, c] in IR by XBOOLE_0:def 4;

          then t <= c9;

          hence thesis by A3, A14, ORDERS_2: 3;

        end;

        deffunc F( set) = the Element of $1;

        defpred P[ set] means not contradiction;

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

        hence thesis;

      end;

    end;

    theorem :: DICKSON:33

    

     Th32: for R be non empty RelStr st R is quasi_ordered & R is Dickson holds (R \~ ) is well_founded

    proof

      let R be non empty RelStr such that

       A1: R is quasi_ordered and

       A2: R is Dickson;

      

       A3: for f be sequence of R holds ex i,j be Nat st i < j & (f . i) <= (f . j) by A2, Th28;

      now

        let N be Subset of R;

        assume N <> {} ;

        then ( min-classes N) is non empty by A1, A3, Th30;

        hence ex x be object st x in ( min-classes N) by XBOOLE_0:def 1;

      end;

      hence thesis by Th19;

    end;

    theorem :: DICKSON:34

    for R be non empty Poset, N be non empty Subset of R st R is Dickson holds ex B be set st B is_Dickson-basis_of (N,R) & for C be set st C is_Dickson-basis_of (N,R) holds B c= C

    proof

      let R be non empty Poset, N be non empty Subset of R such that

       A1: R is Dickson;

      set IR = the InternalRel of R, CR = the carrier of R;

      set IR9 = the InternalRel of (R \~ );

      set B = { b where b be Element of (R \~ ) : b is_minimal_wrt (N,IR9) };

      

       A2: R is quasi_ordered;

      for f be sequence of R holds ex i,j be Nat st i < j & (f . i) <= (f . j) by A1, Th28;

      then ( min-classes N) is non empty by A2, Th30;

      then

      consider x be object such that

       A3: x in ( min-classes N) by XBOOLE_0:def 1;

      consider y be Element of (R \~ ) such that

       A4: y is_minimal_wrt (N,IR9) and x = (( Class (( EqRel R),y)) /\ N) by A3, Def8;

      y in B by A4;

      then

      reconsider B as non empty set;

      take B;

       A5:

      now

        let x be object;

        assume x in B;

        then ex b be Element of (R \~ ) st (x = b) & (b is_minimal_wrt (N,IR9));

        hence x in N by WAYBEL_4:def 25;

      end;

      then

       A6: B c= N;

      thus B is_Dickson-basis_of (N,R)

      proof

        thus B c= N by A5;

        let a be Element of R such that

         A7: a in N;

        reconsider a9 = a as Element of (R \~ );

        now

          assume

           A8: not ex b be Element of R st b in B & b <= a;

          per cases ;

            suppose ((IR9 -Seg a) /\ N) = {} ;

            then (IR9 -Seg a) misses N by XBOOLE_0:def 7;

            then a9 is_minimal_wrt (N,IR9) by A7, Th5;

            then a in B;

            hence contradiction by A8;

          end;

            suppose

             A9: ((IR9 -Seg a) /\ N) <> {} ;

            (R \~ ) is well_founded by A1, A2, Th32;

            then IR9 is_well_founded_in CR by WELLFND1:def 2;

            then

            consider z be object such that

             A10: z in ((IR9 -Seg a) /\ N) and

             A11: (IR9 -Seg z) misses ((IR9 -Seg a) /\ N) by A9, WELLORD1:def 3;

            

             A12: z in (IR9 -Seg a) by A10, XBOOLE_0:def 4;

            then [z, a] in IR9 by WELLORD1: 1;

            then z in ( dom IR9) by XTUPLE_0:def 12;

            then

            reconsider z as Element of (R \~ );

            reconsider z9 = z as Element of R;

            z is_minimal_wrt (((IR9 -Seg a9) /\ N),IR9) by A10, A11, Th5;

            then z is_minimal_wrt (N,IR9) by Th6;

            then

             A13: z in B;

             [z, a] in (IR \ (IR ~ )) by A12, WELLORD1: 1;

            then z9 <= a;

            hence contradiction by A8, A13;

          end;

        end;

        hence ex b be Element of R st b in B & b <= a;

      end;

      let C be set such that

       A14: C is_Dickson-basis_of (N,R);

      

       A15: C c= N by A14;

      now

        let b be object such that

         A16: b in B;

        b in N by A5, A16;

        then

        reconsider b9 = b as Element of R;

        consider c be Element of R such that

         A17: c in C and

         A18: c <= b9 by A6, A14, A16;

        

         A19: ex b99 be Element of (R \~ ) st (b99 = b) & (b99 is_minimal_wrt (N,IR9)) by A16;

        

         A20: [c, b] in IR by A18;

        

         A21: IR is_antisymmetric_in CR by ORDERS_2:def 4;

         [b, c] in IR by A15, A17, A19, A20, Th16;

        hence b in C by A17, A18, A21;

      end;

      hence thesis;

    end;

    definition

      let R be non empty RelStr, N be Subset of R;

      :: DICKSON:def13

      func Dickson-bases (N,R) -> non empty Subset-Family of R means

      : Def13: for B be set holds B in it iff B is_Dickson-basis_of (N,R);

      existence

      proof

        set BB = { b where b be Subset of N : b is_Dickson-basis_of (N,R) };

        set CR = the carrier of R;

        consider bp be set such that

         A2: bp is_Dickson-basis_of (N,R) and bp is finite by A1;

        

         A3: bp in BB by A2;

        now

          let x be object;

          assume x in BB;

          then

          consider b be Subset of N such that

           A4: x = b and b is_Dickson-basis_of (N,R);

          b c= CR by XBOOLE_1: 1;

          hence x in ( bool CR) by A4;

        end;

        then

        reconsider BB as non empty Subset-Family of CR by A3, TARSKI:def 3;

        take BB;

        let B be set;

        hereby

          assume B in BB;

          then ex b be Subset of N st (b = B) & (b is_Dickson-basis_of (N,R));

          hence B is_Dickson-basis_of (N,R);

        end;

        assume

         A5: B is_Dickson-basis_of (N,R);

        thus thesis by A5;

      end;

      uniqueness

      proof

        let IT1,IT2 be non empty Subset-Family of R such that

         A6: for B be set holds B in IT1 iff B is_Dickson-basis_of (N,R) and

         A7: for B be set holds B in IT2 iff B is_Dickson-basis_of (N,R);

        for x be object holds x in IT1 iff x in IT2 by A6, A7;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: DICKSON:35

    

     Th34: for R be non empty RelStr, s be sequence of R st R is Dickson holds ex t be sequence of R st t is subsequence of s & t is weakly-ascending

    proof

      let R be non empty RelStr, s be sequence of R such that

       A1: R is Dickson;

      set CR = the carrier of R;

      deffunc Bi( Element of ( rng s), Element of NAT ) = { n where n be Element of NAT : $1 <= (s . n) & $2 < n };

      deffunc Bi2( Element of ( rng s)) = { n where n be Element of NAT : $1 <= (s . n) };

      defpred P[ set, Element of NAT , set] means ex N be Subset of CR, B be non empty Subset of CR st N = { (s . w) where w be Element of NAT : (s . $2) <= (s . w) & $2 < w } & { w where w be Element of NAT : (s . $2) <= (s . w) & $2 < w } is infinite & B = the Element of { BB where BB be Element of ( Dickson-bases (N,R)) : BB is finite } & $3 = (s mindex ( the Element of { b where b be Element of B : ex b9 be Element of ( rng s) st b9 = b & Bi(b9,$2) is infinite },$2));

      defpred Q[ set, Element of NAT , set] means { w where w be Element of NAT : (s . $2) <= (s . w) & $2 < w } is infinite implies P[$1, $2, $3];

      

       A2: for n be Nat holds for x be Element of NAT holds ex y be Element of NAT st Q[n, x, y]

      proof

        let n be Nat, x be Element of NAT ;

        set N = { (s . w) where w be Element of NAT : (s . x) <= (s . w) & x < w };

        now

          let y be object;

          assume y in N;

          then ex w be Element of NAT st (y = (s . w)) & ((s . x) <= (s . w)) & (x < w);

          hence y in CR;

        end;

        then

        reconsider N as Subset of CR by TARSKI:def 3;

        set W = { w where w be Element of NAT : (s . x) <= (s . w) & x < w };

        per cases ;

          suppose

           A3: N is empty;

          take 1;

          assume W is infinite;

          then

          consider ww be object such that

           A4: ww in W by XBOOLE_0:def 1;

          consider www be Element of NAT such that www = ww and

           A5: (s . x) <= (s . www) and

           A6: x < www by A4;

          (s . www) in N by A5, A6;

          hence thesis by A3;

        end;

          suppose

           A7: N is non empty;

          set BBX = { BB where BB be Element of ( Dickson-bases (N,R)) : BB is finite };

          set B = the Element of BBX;

          consider BD1 be set such that

           A8: BD1 is_Dickson-basis_of (N,R) and

           A9: BD1 is finite by A1;

          BD1 in ( Dickson-bases (N,R)) by A1, A8, Def13;

          then BD1 in BBX by A9;

          then B in BBX;

          then ex BBB be Element of ( Dickson-bases (N,R)) st (B = BBB) & (BBB is finite);

          then

           A10: B is_Dickson-basis_of (N,R) by A1, Def13;

          reconsider B as non empty Subset of CR by A7, A10, Th25, XBOOLE_1: 1;

          set y = (s mindex ( the Element of { b where b be Element of B : ex b9 be Element of ( rng s) st b9 = b & Bi(b9,x) is infinite },x));

          take y;

          set W = { w where w be Element of NAT : (s . x) <= (s . w) & x < w };

          assume

           A11: W is infinite;

          take N;

          reconsider B as non empty Subset of CR;

          take B;

          thus N = { (s . w) where w be Element of NAT : (s . x) <= (s . w) & x < w };

          thus { w where w be Element of NAT : (s . x) <= (s . w) & x < w } is infinite by A11;

          thus B = the Element of { BB where BB be Element of ( Dickson-bases (N,R)) : BB is finite };

          thus thesis;

        end;

      end;

      consider B be set such that

       A12: B is_Dickson-basis_of (( rng s),R) and

       A13: B is finite by A1;

      reconsider B as non empty set by A12, Th25;

      set BALL = { b where b be Element of B : ex b9 be Element of ( rng s) st b9 = b & Bi2(b9) is infinite };

      set b1 = the Element of BALL;

      consider f be sequence of NAT such that

       A14: (f . 0 ) = (s mindex b1) and

       A15: for n be Nat holds Q[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A2);

      

       A16: ( dom f) = NAT by FUNCT_2:def 1;

      

       A17: ( rng f) c= NAT ;

      now

        

         A18: B is finite by A13;

        assume

         A19: for b be Element of ( rng s) st b in B holds Bi2(b) is finite;

        set Ball = { Bi2(b) where b be Element of ( rng s) : b in B };

        

         A20: Ball is finite from FRAENKEL:sch 21( A18);

        now

          let X be set;

          assume X in Ball;

          then ex b be Element of ( rng s) st (X = Bi2(b)) & (b in B);

          hence X is finite by A19;

        end;

        then

         A21: ( union Ball) is finite by A20, FINSET_1: 7;

        now

          let x be object;

          assume x in NAT ;

          then

          reconsider x9 = x as Element of NAT ;

          ( dom s) = NAT by FUNCT_2:def 1;

          then x9 in ( dom s);

          then

           A22: (s . x) in ( rng s) by FUNCT_1: 3;

          then

          reconsider sx = (s . x) as Element of R;

          consider b be Element of R such that

           A23: b in B and

           A24: b <= sx by A12, A22;

          B c= ( rng s) by A12;

          then

          reconsider b as Element of ( rng s) by A23;

          

           A25: x9 in Bi2(b) by A24;

           Bi2(b) in Ball by A23;

          hence x in ( union Ball) by A25, TARSKI:def 4;

        end;

        then NAT c= ( union Ball);

        hence contradiction by A21;

      end;

      then

      consider tb be Element of ( rng s) such that

       A26: tb in B and

       A27: Bi2(tb) is infinite;

      

       A28: tb in BALL by A26, A27;

      then b1 in BALL;

      then

       A29: ex bt be Element of B st (b1 = bt) & (ex b9 be Element of ( rng s) st b9 = bt & Bi2(b9) is infinite);

      ( dom s) = NAT by NORMSP_1: 12;

      then

       A30: (s . (f . 0 )) = b1 by A14, A29, Def11;

      b1 in BALL by A28;

      then

       A31: ex eb be Element of B st (b1 = eb) & (ex eb9 be Element of ( rng s) st eb9 = eb & Bi2(eb9) is infinite);

      deffunc F( set) = $1;

      defpred P[ Nat] means 0 <= $1 & (s . (f . 0 )) <= (s . $1);

      set W1 = { w where w be Element of NAT : (s . (f . 0 )) <= (s . w) };

      set W2 = { w where w be Element of NAT : (s . (f . 0 )) <= (s . w) & (f . 0 ) < w };

      set W3 = { F(w) where w be Nat : w <= (f . 0 ) & P[w] };

      

       A32: W3 is finite from FINSEQ_1:sch 6;

      now

        let x be object;

        hereby

          assume x in W1;

          then

          consider w be Element of NAT such that

           A33: x = w and

           A34: (s . (f . 0 )) <= (s . w);

          

           A35: 0 <= w by NAT_1: 2;

          w <= (f . 0 ) or w > (f . 0 );

          then x in W2 or x in W3 by A33, A34, A35;

          hence x in (W2 \/ W3) by XBOOLE_0:def 3;

        end;

        assume

         A36: x in (W2 \/ W3);

        per cases by A36, XBOOLE_0:def 3;

          suppose x in W2;

          then ex w be Element of NAT st (x = w) & ((s . (f . 0 )) <= (s . w)) & ((f . 0 ) < w);

          hence x in W1;

        end;

          suppose x in W3;

          then

           A37: ex w be Nat st x = w & w <= (f . 0 ) & 0 <= w & (s . (f . 0 )) <= (s . w);

          then

          reconsider w = x as Element of NAT by ORDINAL1:def 12;

           0 <= w & w <= (f . 0 ) & (s . (f . 0 )) <= (s . w) by A37;

          hence x in W1;

        end;

      end;

      then

       A38: W2 is infinite by A30, A31, A32, TARSKI: 2;

      defpred R[ Nat] means P[$1, (f . $1), (f . ($1 + 1))];

      

       A39: R[ 0 ] by A15, A38;

       A40:

      now

        let k be Nat;

        assume R[k];

        then

        consider N be Subset of CR, B be non empty Subset of CR such that

         A41: N = { (s . w) where w be Element of NAT : (s . (f . k)) <= (s . w) & (f . k) < w } and

         A42: { w where w be Element of NAT : (s . (f . k)) <= (s . w) & (f . k) < w } is infinite and

         A43: B = the Element of { BB where BB be Element of ( Dickson-bases (N,R)) : BB is finite } and

         A44: (f . (k + 1)) = (s mindex ( the Element of { b where b be Element of B : ex b9 be Element of ( rng s) st b9 = b & Bi(b9,.) is infinite },(f . k)));

        set BALL = { b where b be Element of B : ex b9 be Element of ( rng s) st b9 = b & Bi(b9,.) is infinite };

        set BBX = { BB where BB be Element of ( Dickson-bases (N,R)) : BB is finite };

        set iN = { w where w be Element of NAT : (s . (f . k)) <= (s . w) & (f . k) < w };

        consider BD be set such that

         A45: BD is_Dickson-basis_of (N,R) and

         A46: BD is finite by A1;

        BD in ( Dickson-bases (N,R)) by A1, A45, Def13;

        then BD in BBX by A46;

        then B in BBX by A43;

        then

         A47: ex BB be Element of ( Dickson-bases (N,R)) st (B = BB) & (BB is finite);

        then

         A48: B is_Dickson-basis_of (N,R) by A1, Def13;

        now

          deffunc F( Element of ( rng s)) = Bi($1,.);

          

           A49: B is finite by A47;

          assume

           A50: for b be Element of ( rng s) st b in B holds Bi(b,.) is finite;

          set Ball = { F(b) where b be Element of ( rng s) : b in B };

          

           A51: Ball is finite from FRAENKEL:sch 21( A49);

          now

            let X be set;

            assume X in Ball;

            then ex b be Element of ( rng s) st (X = Bi(b,.)) & (b in B);

            hence X is finite by A50;

          end;

          then

           A52: ( union Ball) is finite by A51, FINSET_1: 7;

          iN c= ( union Ball)

          proof

            let x be object;

            assume x in iN;

            then

            consider w be Element of NAT such that

             A53: x = w and

             A54: (s . (f . k)) <= (s . w) and

             A55: (f . k) < w;

            

             A56: (s . w) in N by A41, A54, A55;

            reconsider sw = (s . w) as Element of R;

            consider b be Element of R such that

             A57: b in B and

             A58: b <= sw by A48, A56;

            

             A59: B c= N by A48;

            N c= ( rng s)

            proof

              let x be object;

              assume x in N;

              then

               A60: ex u be Element of NAT st (x = (s . u)) & ((s . (f . k)) <= (s . u)) & ((f . k) < u) by A41;

              ( dom s) = NAT by FUNCT_2:def 1;

              hence thesis by A60, FUNCT_1: 3;

            end;

            then B c= ( rng s) by A59;

            then

            reconsider b as Element of ( rng s) by A57;

            

             A61: w in Bi(b,.) by A55, A58;

             Bi(b,.) in Ball by A57;

            hence thesis by A53, A61, TARSKI:def 4;

          end;

          hence contradiction by A42, A52;

        end;

        then

        consider b be Element of ( rng s) such that

         A62: b in B and

         A63: Bi(b,.) is infinite;

        b in BALL by A62, A63;

        then the Element of BALL in BALL;

        then

        consider b be Element of B such that

         A64: b = the Element of BALL and

         A65: ex b9 be Element of ( rng s) st b9 = b & Bi(b9,.) is infinite;

        B c= N by A48;

        then b in N;

        then

         A66: ex w be Element of NAT st (b = (s . w)) & ((s . (f . k)) <= (s . w)) & ((f . k) < w) by A41;

        then

         A67: (s . (f . (k + 1))) = the Element of BALL by A44, A64, Def12;

        

         A68: (f . k) < (f . (k + 1)) by A44, A64, A66, Def12;

        deffunc F( set) = $1;

        defpred P[ Nat] means (f . k) < $1 & (s . (f . (k + 1))) <= (s . $1);

        set W1 = { w1 where w1 be Element of NAT : (s . (f . (k + 1))) <= (s . w1) & (f . k) < w1 };

        set W2 = { w1 where w1 be Element of NAT : (s . (f . (k + 1))) <= (s . w1) & (f . (k + 1)) < w1 };

        set W3 = { F(w1) where w1 be Nat : w1 <= (f . (k + 1)) & P[w1] };

        

         A69: W3 is finite from FINSEQ_1:sch 6;

        now

          let x be object;

          hereby

            assume x in W1;

            then

            consider w be Element of NAT such that

             A70: x = w and

             A71: (s . (f . (k + 1))) <= (s . w) and

             A72: (f . k) < w;

            w <= (f . (k + 1)) or w > (f . (k + 1));

            then x in W2 or x in W3 by A70, A71, A72;

            hence x in (W2 \/ W3) by XBOOLE_0:def 3;

          end;

          assume

           A73: x in (W2 \/ W3);

          per cases by A73, XBOOLE_0:def 3;

            suppose x in W2;

            then

            consider w be Element of NAT such that

             A74: x = w and

             A75: (s . (f . (k + 1))) <= (s . w) and

             A76: (f . (k + 1)) < w;

            (f . k) < w by A68, A76, XXREAL_0: 2;

            hence x in W1 by A74, A75;

          end;

            suppose x in W3;

            then

            consider w be Nat such that

             A77: x = w & w <= (f . (k + 1)) & (f . k) < w & (s . (f . (k + 1))) <= (s . w);

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

            x = w & (f . k) < w & w <= (f . (k + 1)) & (s . (f . (k + 1))) <= (s . w) by A77;

            hence x in W1;

          end;

        end;

        then W2 is infinite by A64, A65, A67, A69, TARSKI: 2;

        hence R[(k + 1)] by A15;

      end;

      

       A78: for n be Nat holds R[n] from NAT_1:sch 2( A39, A40);

      set t = (s * f);

      take t;

      reconsider f as sequence of REAL by FUNCT_2: 7, NUMBERS: 19;

      now

        now

          let n be Nat;

          

           A79: n in NAT by ORDINAL1:def 12;

          (f . n) in ( rng f) by A16, A79, FUNCT_1:def 3;

          then

          reconsider fn = (f . n) as Element of NAT by A17;

          consider N be Subset of CR, B be non empty Subset of CR such that

           A80: N = { (s . w) where w be Element of NAT : (s . fn) <= (s . w) & fn < w } and

           A81: { w where w be Element of NAT : (s . fn) <= (s . w) & fn < w } is infinite and

           A82: B = the Element of { BB where BB be Element of ( Dickson-bases (N,R)) : BB is finite } and

           A83: (f . (n + 1)) = (s mindex ( the Element of { b where b be Element of B : ex b9 be Element of ( rng s) st b9 = b & Bi(b9,fn) is infinite },fn)) by A78;

          set BBX = { BB where BB be Element of ( Dickson-bases (N,R)) : BB is finite };

          set BJ = { b where b be Element of B : ex b9 be Element of ( rng s) st b9 = b & Bi(b9,fn) is infinite };

          set BC = the Element of BJ;

          consider BD be set such that

           A84: BD is_Dickson-basis_of (N,R) and

           A85: BD is finite by A1;

          BD in ( Dickson-bases (N,R)) by A1, A84, Def13;

          then BD in BBX by A85;

          then B in BBX by A82;

          then

           A86: ex BB be Element of ( Dickson-bases (N,R)) st (B = BB) & (BB is finite);

          then

           A87: B is_Dickson-basis_of (N,R) by A1, Def13;

          then

           A88: B c= N;

          now

            

             A89: B is finite by A86;

            assume

             A90: for b be Element of ( rng s) st b in B holds Bi(b,fn) is finite;

            deffunc F( Element of ( rng s)) = Bi($1,fn);

            set Ball = { F(b) where b be Element of ( rng s) : b in B };

            set iN = { w where w be Element of NAT : (s . fn) <= (s . w) & fn < w };

            

             A91: Ball is finite from FRAENKEL:sch 21( A89);

            now

              let X be set;

              assume X in Ball;

              then ex b be Element of ( rng s) st (X = Bi(b,fn)) & (b in B);

              hence X is finite by A90;

            end;

            then

             A92: ( union Ball) is finite by A91, FINSET_1: 7;

            iN c= ( union Ball)

            proof

              let x be object;

              assume x in iN;

              then

              consider w be Element of NAT such that

               A93: x = w and

               A94: (s . fn) <= (s . w) and

               A95: (f . n) < w;

              

               A96: (s . w) in N by A80, A94, A95;

              reconsider sw = (s . w) as Element of R;

              consider b be Element of R such that

               A97: b in B and

               A98: b <= sw by A87, A96;

              

               A99: B c= N by A87;

              N c= ( rng s)

              proof

                let x be object;

                assume x in N;

                then

                 A100: ex u be Element of NAT st (x = (s . u)) & ((s . fn) <= (s . u)) & (fn < u) by A80;

                ( dom s) = NAT by FUNCT_2:def 1;

                hence thesis by A100, FUNCT_1: 3;

              end;

              then B c= ( rng s) by A99;

              then

              reconsider b as Element of ( rng s) by A97;

              

               A101: w in Bi(b,fn) by A95, A98;

               Bi(b,fn) in Ball by A97;

              hence thesis by A93, A101, TARSKI:def 4;

            end;

            hence contradiction by A81, A92;

          end;

          then

          consider b be Element of ( rng s) such that

           A102: b in B and

           A103: Bi(b,fn) is infinite;

          b in BJ by A102, A103;

          then BC in BJ;

          then ex b be Element of B st (BC = b) & (ex b9 be Element of ( rng s) st b9 = b & Bi(b9,fn) is infinite);

          then BC in N by A88;

          then ex j be Element of NAT st (BC = (s . j)) & ((s . fn) <= (s . j)) & (fn < j) by A80;

          hence (f . n) < (f . (n + 1)) by A83, Def12;

        end;

        hence f is increasing by SEQM_3:def 6;

        let n be Element of NAT ;

        (f . n) in ( rng f) by A16, FUNCT_1:def 3;

        hence (f . n) is Element of NAT by A17;

      end;

      then

      reconsider f as increasing sequence of NAT ;

      t = (s * f);

      hence t is subsequence of s;

      let n be Nat;

      n in NAT by ORDINAL1:def 12;

      then

       A104: (t . n) = (s . (f . n)) by A16, FUNCT_1: 13;

      

       A105: (t . (n + 1)) = (s . (f . (n + 1))) by A16, FUNCT_1: 13;

      consider N be Subset of CR, B be non empty Subset of CR such that

       A106: N = { (s . w) where w be Element of NAT : (s . (f . n)) <= (s . w) & (f . n) < w } and

       A107: { w where w be Element of NAT : (s . (f . n)) <= (s . w) & (f . n) < w } is infinite and

       A108: B = the Element of { BB where BB be Element of ( Dickson-bases (N,R)) : BB is finite } and

       A109: (f . (n + 1)) = (s mindex ( the Element of { b where b be Element of B : ex b9 be Element of ( rng s) st b9 = b & Bi(b9,.) is infinite },(f . n))) by A78;

      set BX = { b where b be Element of B : ex b9 be Element of ( rng s) st b9 = b & Bi(b9,.) is infinite };

      set sfn1 = the Element of BX;

      set BBX = { BB where BB be Element of ( Dickson-bases (N,R)) : BB is finite };

      consider BD be set such that

       A110: BD is_Dickson-basis_of (N,R) and

       A111: BD is finite by A1;

      BD in ( Dickson-bases (N,R)) by A1, A110, Def13;

      then BD in BBX by A111;

      then B in BBX by A108;

      then

       A112: ex BB be Element of ( Dickson-bases (N,R)) st (BB = B) & (BB is finite);

      then

       A113: B is_Dickson-basis_of (N,R) by A1, Def13;

      now

        

         A114: B is finite by A112;

        assume

         A115: for b be Element of ( rng s) st b in B holds Bi(b,.) is finite;

        deffunc F( Element of ( rng s)) = Bi($1,.);

        set Ball = { F(b) where b be Element of ( rng s) : b in B };

        set iN = { w where w be Element of NAT : (s . (f . n)) <= (s . w) & (f . n) < w };

        

         A116: Ball is finite from FRAENKEL:sch 21( A114);

        now

          let X be set;

          assume X in Ball;

          then ex b be Element of ( rng s) st (X = Bi(b,.)) & (b in B);

          hence X is finite by A115;

        end;

        then

         A117: ( union Ball) is finite by A116, FINSET_1: 7;

        iN c= ( union Ball)

        proof

          let x be object;

          assume x in iN;

          then

          consider w be Element of NAT such that

           A118: x = w and

           A119: (s . (f . n)) <= (s . w) and

           A120: (f . n) < w;

          

           A121: (s . w) in N by A106, A119, A120;

          reconsider sw = (s . w) as Element of R;

          consider b be Element of R such that

           A122: b in B and

           A123: b <= sw by A113, A121;

          

           A124: B c= N by A113;

          N c= ( rng s)

          proof

            let x be object;

            assume x in N;

            then

             A125: ex u be Element of NAT st (x = (s . u)) & ((s . (f . n)) <= (s . u)) & ((f . n) < u) by A106;

            ( dom s) = NAT by FUNCT_2:def 1;

            hence thesis by A125, FUNCT_1: 3;

          end;

          then B c= ( rng s) by A124;

          then

          reconsider b as Element of ( rng s) by A122;

          

           A126: w in Bi(b,.) by A120, A123;

           Bi(b,.) in Ball by A122;

          hence thesis by A118, A126, TARSKI:def 4;

        end;

        hence contradiction by A107, A117;

      end;

      then

      consider b be Element of ( rng s) such that

       A127: b in B and

       A128: Bi(b,.) is infinite;

      b in BX by A127, A128;

      then sfn1 in BX;

      then ex b be Element of B st (b = sfn1) & (ex b9 be Element of ( rng s) st b9 = b & Bi(b9,.) is infinite);

      then

       A129: sfn1 in B;

      B c= N by A113;

      then sfn1 in N by A129;

      then ex w be Element of NAT st (sfn1 = (s . w)) & ((s . (f . n)) <= (s . w)) & ((f . n) < w) by A106;

      then (t . n) <= (t . (n + 1)) by A104, A105, A109, Def12;

      hence [(t . n), (t . (n + 1))] in the InternalRel of R;

    end;

    theorem :: DICKSON:36

    

     Th35: for R be RelStr st R is empty holds R is Dickson

    proof

      let R be RelStr such that

       A1: R is empty;

      now

        let N be Subset of R;

        take B = {} ;

        N = ( {} the carrier of R) by A1;

        hence B is_Dickson-basis_of (N,R);

        thus B is finite;

      end;

      hence thesis;

    end;

    theorem :: DICKSON:37

    

     Th36: for M,N be RelStr st M is Dickson & N is Dickson & M is quasi_ordered & N is quasi_ordered holds [:M, N:] is quasi_ordered & [:M, N:] is Dickson

    proof

      let M,N be RelStr such that

       A1: M is Dickson and

       A2: N is Dickson and

       A3: M is quasi_ordered and

       A4: N is quasi_ordered;

      reconsider M9 = M as reflexive transitive RelStr by A3;

      reconsider N9 = N as reflexive transitive RelStr by A4;

       [:M9, N9:] is reflexive;

      hence

       A5: [:M, N:] is quasi_ordered;

      per cases ;

        suppose M is non empty & N is non empty;

        then

        reconsider Me = M, Ne = N as non empty RelStr;

        set CPMN = [:Me, Ne:];

        for f be sequence of [:Me, Ne:] holds ex i,j be Nat st i < j & (f . i) <= (f . j)

        proof

          let f be sequence of [:Me, Ne:];

          deffunc F( Element of NAT ) = ((f . $1) `1 );

          consider a be sequence of the carrier of Me such that

           A6: for x be Element of NAT holds (a . x) = F(x) from FUNCT_2:sch 4;

          reconsider a as sequence of Me;

          consider sa be sequence of Me such that

           A7: sa is subsequence of a and

           A8: sa is weakly-ascending by A1, Th34;

          consider NS be increasing sequence of NAT such that

           A9: sa = (a * NS) by A7, VALUED_0:def 17;

          deffunc G( Element of NAT ) = ((f . (NS . $1)) `2 );

          consider b be sequence of the carrier of Ne such that

           A10: for x be Element of NAT holds (b . x) = G(x) from FUNCT_2:sch 4;

          reconsider b as sequence of Ne;

          consider i,j be Nat such that

           A11: i < j and

           A12: (b . i) <= (b . j) by A2, Th28;

          

           A13: i in NAT by ORDINAL1:def 12;

          

           A14: j in NAT by ORDINAL1:def 12;

          take (NS . i), (NS . j);

          ( dom NS) = NAT by FUNCT_2:def 1;

          hence (NS . i) < (NS . j) by A11, VALUED_0:def 13, A13, A14;

          reconsider x = (f . (NS . i)), y = (f . (NS . j)) as Element of [:Me, Ne:];

          

           A15: ( dom sa) = NAT by FUNCT_2:def 1;

          

          then

           A16: (sa . i) = (a . (NS . i)) by A9, FUNCT_1: 12, A13

          .= ((f . (NS . i)) `1 ) by A6;

          

           A17: (sa . j) = (a . (NS . j)) by A9, A15, FUNCT_1: 12, A14

          .= ((f . (NS . j)) `1 ) by A6;

          M is transitive by A3;

          then

           A18: (x `1 ) <= (y `1 ) by A8, A11, A16, A17, Th3;

          

           A19: (b . i) = (x `2 ) by A10, A13;

          (b . j) = (y `2 ) by A10, A14;

          hence thesis by A12, A18, A19, YELLOW_3: 12;

        end;

        then for N be non empty Subset of CPMN holds ( min-classes N) is finite & ( min-classes N) is non empty by A5, Th30;

        hence thesis by A5, Th31;

      end;

        suppose

         A20: not (M is non empty & N is non empty);

        now

          per cases by A20;

            suppose M is empty;

            then

            reconsider M2 = the carrier of M as empty set;

             [:M2, the carrier of N:] is empty;

            hence [:the carrier of M, the carrier of N:] is empty;

          end;

            suppose N is empty;

            then

            reconsider N2 = the carrier of N as empty set;

             [:the carrier of M, N2:] is empty;

            hence [:the carrier of M, the carrier of N:] is empty;

          end;

        end;

        then [:M, N:] is empty by YELLOW_3:def 2;

        hence thesis by Th35;

      end;

    end;

    theorem :: DICKSON:38

    

     Th37: for R,S be RelStr st (R,S) are_isomorphic & R is Dickson & R is quasi_ordered holds S is quasi_ordered & S is Dickson

    proof

      let R,S be RelStr such that

       A1: (R,S) are_isomorphic and

       A2: R is Dickson and

       A3: R is quasi_ordered;

      set CRS = the carrier of S, IRS = the InternalRel of S;

      per cases ;

        suppose not R is empty & not S is empty;

        then

        reconsider Re = R, Se = S as non empty RelStr;

        consider f be Function of Re, Se such that

         A4: f is isomorphic by A1, WAYBEL_1:def 8;

        

         A5: f is one-to-one by A4, WAYBEL_0: 66;

        

         A6: ( rng f) = the carrier of Se by A4, WAYBEL_0: 66;

        

         A7: Re is reflexive by A3;

        

         A8: Re is transitive by A3;

        

         A9: Se is reflexive by A1, A7, WAYBEL20: 15;

        Se is transitive by A1, A8, WAYBEL20: 16;

        hence

         A10: S is quasi_ordered by A9;

        now

          let t be sequence of Se;

          reconsider fi = (f " ) as Function of the carrier of Se, the carrier of Re by A5, A6, FUNCT_2: 25;

          deffunc F( Element of NAT ) = (fi . (t . $1));

          consider sr be sequence of the carrier of Re such that

           A11: for x be Element of NAT holds (sr . x) = F(x) from FUNCT_2:sch 4;

          reconsider sr as sequence of Re;

          consider i,j be Nat such that

           A12: i < j and

           A13: (sr . i) <= (sr . j) by A2, Th28;

          take i, j;

          

           A14: i in NAT by ORDINAL1:def 12;

          

           A15: j in NAT by ORDINAL1:def 12;

          thus i < j by A12;

          

           A16: (f . (sr . i)) = (f . ((f " ) . (t . i))) by A11, A14

          .= (t . i) by A5, A6, FUNCT_1: 35;

          (f . (sr . j)) = (f . ((f " ) . (t . j))) by A11, A15

          .= (t . j) by A5, A6, FUNCT_1: 35;

          hence (t . i) <= (t . j) by A4, A13, A16, WAYBEL_0: 66;

        end;

        then for N be non empty Subset of Se holds ( min-classes N) is finite & ( min-classes N) is non empty by A10, Th30;

        hence thesis by A10, Th31;

      end;

        suppose

         A17: not ( not R is empty & not S is empty);

         A18:

        now

          per cases by A17;

            suppose

             A19: R is empty;

            ex f be Function of R, S st (f is isomorphic) by A1, WAYBEL_1:def 8;

            hence S is empty by A19, WAYBEL_0:def 38;

          end;

            suppose S is empty;

            hence S is empty;

          end;

        end;

        then for x be object st x in CRS holds [x, x] in IRS;

        then

         A20: IRS is_reflexive_in CRS;

        for x,y,z be object st x in CRS & y in CRS & z in CRS & [x, y] in IRS & [y, z] in IRS holds [x, z] in IRS by A18;

        then

         A21: IRS is_transitive_in CRS;

        

         A22: S is reflexive by A20;

        S is transitive by A21;

        hence S is quasi_ordered by A22;

        thus thesis by A18, Th35;

      end;

    end;

    theorem :: DICKSON:39

    

     Th38: for p be RelStr-yielding ManySortedSet of { 0 }, z be Element of { 0 } holds ((p . z),( product p)) are_isomorphic

    proof

      let p be RelStr-yielding ManySortedSet of { 0 }, z be Element of { 0 };

      deffunc F( object) = ( 0 .--> $1);

      consider f be Function such that

       A1: ( dom f) = the carrier of (p . z) and

       A2: for x be object st x in the carrier of (p . z) holds (f . x) = F(x) from FUNCT_1:sch 3;

      

       A3: z = 0 by TARSKI:def 1;

      

       A4: 0 in { 0 } by TARSKI:def 1;

      now

        let x be object;

        assume

         A5: x in the carrier of (p . z);

        then

         A6: (f . x) = ( 0 .--> x) by A2;

        set g = ( 0 .--> x);

        

         A7: ( dom g) = { 0 }

        .= ( dom ( Carrier p)) by PARTFUN1:def 2;

        now

          let y be object;

          assume y in ( dom ( Carrier p));

          then

           A8: y in { 0 };

          then

           A9: y = 0 by TARSKI:def 1;

          ex R be 1-sorted st (R = (p . y)) & ((( Carrier p) . y) = the carrier of R) by A8, PRALG_1:def 15;

          hence (g . y) in (( Carrier p) . y) by A3, A5, A9;

        end;

        then (f . x) in ( product ( Carrier p)) by A6, A7, CARD_3:def 5;

        hence (f . x) in the carrier of ( product p) by YELLOW_1:def 4;

      end;

      then

      reconsider f as Function of (p . z), ( product p) by A1, FUNCT_2: 3;

      now

        per cases ;

          suppose

           A10: (p . z) is empty;

          now

            assume not the carrier of ( product p) is empty;

            then

             A11: ( product ( Carrier p)) is non empty by YELLOW_1:def 4;

            set x = the Element of ( product ( Carrier p));

            

             A12: ex g be Function st (x = g) & (( dom g) = ( dom ( Carrier p))) & (for y be object st y in ( dom ( Carrier p)) holds (g . y) in (( Carrier p) . y)) by A11, CARD_3:def 5;

            

             A13: 0 in ( dom ( Carrier p)) by A4, PARTFUN1:def 2;

            consider R be 1-sorted such that

             A14: R = (p . 0 ) and

             A15: (( Carrier p) . 0 ) = the carrier of R by A4, PRALG_1:def 15;

            R is empty by A10, A14, TARSKI:def 1;

            hence contradiction by A12, A13, A15;

          end;

          then ( product p) is empty;

          hence f is isomorphic by A10, WAYBEL_0:def 38;

        end;

          suppose

           A16: (p . z) is non empty;

          then

          reconsider pz = (p . z) as non empty RelStr;

          now

            let i be set;

            assume i in ( rng p);

            then

            consider x be object such that

             A17: x in ( dom p) and

             A18: i = (p . x) by FUNCT_1:def 3;

            x in { 0 } by A17;

            then i = (p . 0 ) by A18, TARSKI:def 1;

            hence i is non empty 1-sorted by A16, TARSKI:def 1;

          end;

          then

          reconsider np = p as yielding_non-empty_carriers RelStr-yielding ManySortedSet of { 0 } by YELLOW_6:def 2;

          ( product np) is non empty;

          then

          reconsider pp = ( product p) as non empty RelStr;

          now

            let x1,x2 be object such that

             A19: x1 in ( dom f) and

             A20: x2 in ( dom f) and

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

            

             A22: (f . x1) = ( 0 .--> x1) by A2, A19

            .= [: { 0 }, {x1}:];

            

             A23: (f . x2) = ( 0 .--> x2) by A2, A20

            .= [: { 0 }, {x2}:];

            

             A24: 0 in { 0 } by TARSKI:def 1;

            x1 in {x1} by TARSKI:def 1;

            then [ 0 , x1] in (f . x2) by A21, A22, A24, ZFMISC_1:def 2;

            then ex xa,ya be object st (xa in { 0 }) & (ya in {x2}) & ( [ 0 , x1] = [xa, ya]) by A23, ZFMISC_1:def 2;

            then x1 in {x2} by XTUPLE_0: 1;

            hence x1 = x2 by TARSKI:def 1;

          end;

          then

           A25: f is one-to-one by FUNCT_1:def 4;

          now

            let y be object;

            thus y in ( rng f) implies y in the carrier of ( product p);

            assume y in the carrier of ( product p);

            then y in ( product ( Carrier p)) by YELLOW_1:def 4;

            then

            consider g be Function such that

             A26: y = g and

             A27: ( dom g) = ( dom ( Carrier p)) and

             A28: for x be object st x in ( dom ( Carrier p)) holds (g . x) in (( Carrier p) . x) by CARD_3:def 5;

            

             A29: ( dom g) = { 0 } by A27, PARTFUN1:def 2;

            

             A30: 0 in ( dom ( Carrier p)) by A4, PARTFUN1:def 2;

            

             A31: ex R be 1-sorted st (R = (p . 0 )) & ((( Carrier p) . 0 ) = the carrier of R) by A4, PRALG_1:def 15;

            

             A32: g = ( 0 .--> (g . 0 )) by A29, Th1;

            

             A33: (f . (g . 0 )) = ( 0 .--> (g . 0 )) by A2, A3, A28, A30, A31;

            (g . 0 ) in ( dom f) by A1, A3, A28, A30, A31;

            hence y in ( rng f) by A26, A32, A33, FUNCT_1:def 3;

          end;

          then

           A34: ( rng f) = the carrier of ( product p) by TARSKI: 2;

          reconsider f9 = f as Function of pz, pp;

          now

            let x,y be Element of pz;

            ( product np) is non empty;

            then

             A35: ( product ( Carrier p)) is non empty by YELLOW_1:def 4;

            

             A36: (f9 . x) is Element of ( product ( Carrier p)) by YELLOW_1:def 4;

            hereby

              assume

               A37: x <= y;

              ex f1,g1 be Function st f1 = (f9 . x) & g1 = (f9 . y) & for i be object st i in { 0 } holds ex R be RelStr, xi,yi be Element of R st R = (p . i) & xi = (f1 . i) & yi = (g1 . i) & xi <= yi

              proof

                set f1 = ( 0 .--> x);

                set g1 = ( 0 .--> y);

                reconsider f1 as Function;

                reconsider g1 as Function;

                take f1, g1;

                thus f1 = (f9 . x) by A2;

                thus g1 = (f9 . y) by A2;

                let i be object such that

                 A38: i in { 0 };

                

                 A39: i = 0 by A38, TARSKI:def 1;

                 0 in ( dom p) by A4, PARTFUN1:def 2;

                then (p . 0 ) in ( rng p) by FUNCT_1:def 3;

                then

                reconsider p0 = (p . 0 ) as RelStr by YELLOW_1:def 3;

                set R = p0;

                reconsider x9 = x as Element of R by TARSKI:def 1;

                reconsider y9 = y as Element of R by TARSKI:def 1;

                take R, x9, y9;

                thus R = (p . i) by A38, TARSKI:def 1;

                thus x9 = (f1 . i) by A39, FUNCOP_1: 72;

                thus y9 = (g1 . i) by A39, FUNCOP_1: 72;

                thus thesis by A37, TARSKI:def 1;

              end;

              hence (f9 . x) <= (f9 . y) by A35, A36, YELLOW_1:def 4;

            end;

            assume (f9 . x) <= (f9 . y);

            then

            consider f1,g1 be Function such that

             A40: f1 = (f9 . x) and

             A41: g1 = (f9 . y) and

             A42: for i be object st i in { 0 } holds ex R be RelStr, xi,yi be Element of R st R = (p . i) & xi = (f1 . i) & yi = (g1 . i) & xi <= yi by A35, A36, YELLOW_1:def 4;

            consider R be RelStr, xi,yi be Element of R such that

             A43: R = (p . 0 ) and

             A44: xi = (f1 . 0 ) and

             A45: yi = (g1 . 0 ) and

             A46: xi <= yi by A4, A42;

            f1 = ( 0 .--> x) by A2, A40;

            then

             A47: xi = x by A44, FUNCOP_1: 72;

            

             A48: g1 = ( 0 .--> y) by A2, A41;

            R = pz by A43, TARSKI:def 1;

            hence x <= y by A45, A46, A47, A48, FUNCOP_1: 72;

          end;

          hence f is isomorphic by A25, A34, WAYBEL_0: 66;

        end;

      end;

      hence thesis by WAYBEL_1:def 8;

    end;

    registration

      let X be set, p be RelStr-yielding ManySortedSet of X, Y be Subset of X;

      cluster (p | Y) -> RelStr-yielding;

      coherence

      proof

        now

          let v be set;

          assume v in ( rng (p | Y));

          then

          consider x be object such that

           A1: x in ( dom (p | Y)) and

           A2: v = ((p | Y) . x) by FUNCT_1:def 3;

          

           A3: x in Y by A1;

          then

           A4: ((p | Y) . x) = (p . x) by FUNCT_1: 49;

          x in X by A3;

          then x in ( dom p) by PARTFUN1:def 2;

          then (p . x) in ( rng p) by FUNCT_1: 3;

          hence v is RelStr by A2, A4, YELLOW_1:def 3;

        end;

        hence thesis by YELLOW_1:def 3;

      end;

    end

    theorem :: DICKSON:40

    

     Th39: for n be non zero Nat, p be RelStr-yielding ManySortedSet of n holds ( product p) is non empty iff p is non-Empty

    proof

      let n be non zero Nat, p be RelStr-yielding ManySortedSet of n;

      hereby

        assume ( product p) is non empty;

        then ( product ( Carrier p)) is non empty by YELLOW_1:def 4;

        then

        consider z be object such that

         A1: z in ( product ( Carrier p)) by XBOOLE_0:def 1;

        

         A2: ex g be Function st (z = g) & (( dom g) = ( dom ( Carrier p))) & (for i be object st i in ( dom ( Carrier p)) holds (g . i) in (( Carrier p) . i)) by A1, CARD_3:def 5;

        now

          let S be 1-sorted;

          assume S in ( rng p);

          then

          consider x be object such that

           A3: x in ( dom p) and

           A4: S = (p . x) by FUNCT_1:def 3;

          

           A5: x in n by A3;

          then

           A6: x in ( dom ( Carrier p)) by PARTFUN1:def 2;

          ex R be 1-sorted st (R = (p . x)) & ((( Carrier p) . x) = the carrier of R) by A5, PRALG_1:def 15;

          hence S is non empty by A2, A4, A6;

        end;

        hence p is non-Empty by WAYBEL_3:def 7;

      end;

      assume

       A7: p is non-Empty;

      

       A8: ( dom ( Carrier p)) = n by PARTFUN1:def 2;

      deffunc F( object) = the Element of (( Carrier p) . $1);

      consider g be Function such that

       A9: ( dom g) = ( dom ( Carrier p)) and

       A10: for i be object st i in ( dom ( Carrier p)) holds (g . i) = F(i) from FUNCT_1:sch 3;

      set x = g;

      now

        take g;

        thus x = g;

        thus ( dom g) = ( dom ( Carrier p)) by A9;

        thus for i be object st i in ( dom ( Carrier p)) holds (g . i) in (( Carrier p) . i)

        proof

          let i be object such that

           A11: i in ( dom ( Carrier p));

          i in ( dom p) by A8, A11, PARTFUN1:def 2;

          then

           A12: (p . i) in ( rng p) by FUNCT_1:def 3;

          then

          reconsider pi1 = (p . i) as RelStr by YELLOW_1:def 3;

          pi1 is non empty by A7, A12, WAYBEL_3:def 7;

          then

           A13: the carrier of pi1 is non empty;

          i in n by A11;

          then

           A14: ex R be 1-sorted st (R = (p . i)) & ((( Carrier p) . i) = the carrier of R) by PRALG_1:def 15;

          (g . i) = the Element of (( Carrier p) . i) by A10, A11;

          hence thesis by A13, A14;

        end;

      end;

      then ( product ( Carrier p)) is non empty by CARD_3:def 5;

      hence thesis by YELLOW_1:def 4;

    end;

    theorem :: DICKSON:41

    

     Th40: for n be non zero Nat, p be RelStr-yielding ManySortedSet of ( Segm (n + 1)), ns be Subset of ( Segm (n + 1)), ne be Element of ( Segm (n + 1)) st ns = n & ne = n holds ( [:( product (p | ns)), (p . ne):],( product p)) are_isomorphic

    proof

      let n be non zero Nat, p be RelStr-yielding ManySortedSet of ( Segm (n + 1)), ns be Subset of ( Segm (n + 1)), ne be Element of ( Segm (n + 1)) such that

       A1: ns = n and

       A2: ne = n;

      set S = [:( product (p | ns)), (p . ne):];

      set T = ( product p);

      set CP = [:the carrier of ( product (p | ns)), the carrier of (p . ne):];

      set CPP = the carrier of ( product p);

      

       A3: ( dom ( Carrier (p | ns))) = n by A1, PARTFUN1:def 2;

      per cases ;

        suppose

         A4: the carrier of ( product p) is empty;

        then

         A5: T is empty;

         not p is non-Empty by A4;

        then

        consider r1 be 1-sorted such that

         A6: r1 in ( rng p) and

         A7: r1 is empty by WAYBEL_3:def 7;

        consider x be object such that

         A8: x in ( dom p) and

         A9: r1 = (p . x) by A6, FUNCT_1:def 3;

        x in ( Segm (n + 1)) by A8;

        then

         A10: x in (( Segm n) \/ {n}) by AFINSQ_1: 2;

        

         A11: S is empty

        proof

          per cases by A10, XBOOLE_0:def 3;

            suppose

             A12: x in n;

            then

             A13: ((p | ns) . x) = (p . x) by A1, FUNCT_1: 49;

            x in ( dom (p | ns)) by A1, A12, PARTFUN1:def 2;

            then (p . x) in ( rng (p | ns)) by A13, FUNCT_1:def 3;

            then not (p | ns) is non-Empty by A7, A9, WAYBEL_3:def 7;

            then

            reconsider ptemp = the carrier of ( product (p | ns)) as empty set by A1, Th39;

             [:ptemp, the carrier of (p . ne):] is empty;

            hence thesis by YELLOW_3:def 2;

          end;

            suppose x in {n};

            then (p . ne) is empty by A2, A7, A9, TARSKI:def 1;

            then

            reconsider pne = the carrier of (p . ne) as empty set;

            reconsider ptemp = the carrier of ( product (p | ns)) as set;

             [:ptemp, pne:] is empty;

            hence thesis by YELLOW_3:def 2;

          end;

        end;

        then

         A14: ( dom {} ) = the carrier of S;

        for x be object st x in {} holds ( {} . x) in the carrier of T;

        then

        reconsider f = {} as Function of S, T by A14, FUNCT_2: 3;

        f is isomorphic by A5, A11, WAYBEL_0:def 38;

        hence thesis by WAYBEL_1:def 8;

      end;

        suppose

         A15: the carrier of ( product p) is non empty;

        then

        reconsider CPP as non empty set;

        reconsider T as non empty RelStr by A15;

        

         A16: p is non-Empty by A15, Th39;

        reconsider p9 = p as RelStr-yielding non-Empty ManySortedSet of ( Segm (n + 1)) by A15, Th39;

        (p9 . ne) is non empty;

        then

        reconsider pne2 = the carrier of (p . ne) as non empty set;

        now

          let S be 1-sorted;

          assume S in ( rng (p | ns));

          then

          consider x be object such that

           A17: x in ( dom (p | ns)) and

           A18: S = ((p | ns) . x) by FUNCT_1:def 3;

          x in ns by A17;

          then x in (n + 1);

          then

           A19: x in ( dom p) by PARTFUN1:def 2;

          S = (p . x) by A17, A18, FUNCT_1: 47;

          then S in ( rng p) by A19, FUNCT_1:def 3;

          hence S is non empty by A16, WAYBEL_3:def 7;

        end;

        then

         A20: (p | ns) is non-Empty by WAYBEL_3:def 7;

        then

         A21: ( product (p | ns)) is non empty;

        reconsider ppns2 = the carrier of ( product (p | ns)) as non empty set by A20;

        CP = [:ppns2, pne2:];

        then

        reconsider S as non empty RelStr by YELLOW_3:def 2;

        CP = the carrier of S by YELLOW_3:def 2;

        then

        reconsider CP9 = CP as non empty set;

        defpred P[ set, set] means ex a be Function, b be Element of pne2 st a in ppns2 & $1 = [a, b] & $2 = (a +* (n .--> b));

        

         A22: for x be Element of CP9 holds ex y be Element of CPP st P[x, y]

        proof

          let x be Element of CP9;

          reconsider xx = x as Element of [:ppns2, pne2:];

          set a = (xx `1 ), b = (xx `2 );

          reconsider a as Element of ppns2 by MCART_1: 10;

          reconsider b as Element of pne2 by MCART_1: 10;

          

           A23: ( product ( Carrier (p | ns))) is non empty by A21, YELLOW_1:def 4;

          

           A24: a is Element of ( product ( Carrier (p | ns))) by YELLOW_1:def 4;

          then

           A25: ex g be Function st (a = g) & (( dom g) = ( dom ( Carrier (p | ns)))) & (for i be object st i in ( dom ( Carrier (p | ns))) holds (g . i) in (( Carrier (p | ns)) . i)) by A23, CARD_3:def 5;

          reconsider a as Function by A24;

          set y = (a +* (n .--> b));

          now

            set g1 = y;

            reconsider g1 as Function;

            take g1;

            thus y = g1;

            

             A26: ( dom a) = ns by A25, PARTFUN1:def 2;

            

            thus ( dom g1) = (( dom a) \/ ( dom (n .--> b))) by FUNCT_4:def 1

            .= (( Segm n) \/ {n}) by A1, A26

            .= ( Segm (n + 1)) by AFINSQ_1: 2

            .= ( dom ( Carrier p)) by PARTFUN1:def 2;

            let x be object;

            assume x in ( dom ( Carrier p));

            then

             A27: x in ( Segm (n + 1));

            then

             A28: x in (( Segm n) \/ {n}) by AFINSQ_1: 2;

            per cases by A28, XBOOLE_0:def 3;

              suppose

               A29: x in n;

              x <> n

              proof

                assume

                 A: x = n;

                then

                reconsider x as set;

                 not x in x;

                hence thesis by A, A29;

              end;

              then not x in ( dom (n .--> b)) by TARSKI:def 1;

              then

               A30: (g1 . x) = (a . x) by FUNCT_4: 11;

              

               A31: x in ( dom ( Carrier (p | ns))) by A1, A29, PARTFUN1:def 2;

              

               A32: ex R be 1-sorted st (R = ((p | ns) . x)) & ((( Carrier (p | ns)) . x) = the carrier of R) by A1, A29, PRALG_1:def 15;

              ex R2 be 1-sorted st (R2 = (p . x)) & ((( Carrier p) . x) = the carrier of R2) by A27, PRALG_1:def 15;

              then (( Carrier (p | ns)) . x) = (( Carrier p) . x) by A1, A29, A32, FUNCT_1: 49;

              hence (g1 . x) in (( Carrier p) . x) by A25, A30, A31;

            end;

              suppose

               A33: x in {n};

              then

               A34: x = n by TARSKI:def 1;

              x in ( dom (n .--> b)) by A33;

              

              then

               A35: (g1 . x) = ((n .--> b) . n) by A34, FUNCT_4: 13

              .= b by FUNCOP_1: 72;

              ex R be 1-sorted st (R = (p . ne)) & ((( Carrier p) . ne) = the carrier of R) by PRALG_1:def 15;

              hence (g1 . x) in (( Carrier p) . x) by A2, A34, A35;

            end;

          end;

          then y in ( product ( Carrier p)) by CARD_3:def 5;

          then

          reconsider y as Element of CPP by YELLOW_1:def 4;

          take y, a, b;

          thus a in ppns2;

          thus x = [a, b] by MCART_1: 21;

          thus thesis;

        end;

        consider f be Function of CP9, CPP such that

         A36: for x be Element of CP9 holds P[x, (f . x)] from FUNCT_2:sch 3( A22);

        now

          the carrier of [:( product (p | ns)), (p . ne):] = [:the carrier of ( product (p | ns)), the carrier of (p . ne):] by YELLOW_3:def 2;

          then

          reconsider f as Function of [:( product (p | ns)), (p . ne):], ( product p);

          reconsider f9 = f as Function of S, T;

          take f;

          now

            let x1,x2 be object such that

             A37: x1 in ( dom f) and

             A38: x2 in ( dom f) and

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

            x1 is Element of [:the carrier of ( product (p | ns)), the carrier of (p . ne):] by A37, YELLOW_3:def 2;

            then

            consider a1 be Function, b1 be Element of pne2 such that

             A40: a1 in ppns2 and

             A41: x1 = [a1, b1] and

             A42: (f . x1) = (a1 +* (n .--> b1)) by A36;

            x2 is Element of [:the carrier of ( product (p | ns)), the carrier of (p . ne):] by A38, YELLOW_3:def 2;

            then

            consider a2 be Function, b2 be Element of pne2 such that

             A43: a2 in ppns2 and

             A44: x2 = [a2, b2] and

             A45: (f . x2) = (a2 +* (n .--> b2)) by A36;

            a1 in ( product ( Carrier (p | ns))) by A40, YELLOW_1:def 4;

            then

             A46: ex g1 be Function st (a1 = g1) & (( dom g1) = ( dom ( Carrier (p | ns)))) & (for x be object st x in ( dom ( Carrier (p | ns))) holds (g1 . x) in (( Carrier (p | ns)) . x)) by CARD_3:def 5;

            a2 in ( product ( Carrier (p | ns))) by A43, YELLOW_1:def 4;

            then

             A47: ex g2 be Function st (a2 = g2) & (( dom g2) = ( dom ( Carrier (p | ns)))) & (for x be object st x in ( dom ( Carrier (p | ns))) holds (g2 . x) in (( Carrier (p | ns)) . x)) by CARD_3:def 5;

            

             A50: ( dom a1) = n by A1, A46, PARTFUN1:def 2;

             A51:

            now

              assume not n misses {n};

              then (n /\ {n}) <> {} by XBOOLE_0:def 7;

              then

              consider x be object such that

               A52: x in (n /\ {n}) by XBOOLE_0:def 1;

              

               A53: x in n by A52, XBOOLE_0:def 4;

              x in {n} by A52, XBOOLE_0:def 4;

              then

               B: x = n by TARSKI:def 1;

              then

              reconsider x as set;

               not x in n by B;

              hence contradiction by A53;

            end;

            then

             A54: ( dom a1) misses ( dom (n .--> b1)) by A50;

            

             A55: ( dom a2) misses ( dom (n .--> b2)) by A46, A47, A50, A51;

             A56:

            now

              let a,b be object;

              hereby

                assume

                 A57: [a, b] in a1;

                then

                 A58: a in ( dom a1) by FUNCT_1: 1;

                

                 A59: b = (a1 . a) by A57, FUNCT_1: 1;

                

                 A60: a in (( dom a1) \/ ( dom (n .--> b1))) by A58, XBOOLE_0:def 3;

                then not a in ( dom (n .--> b1)) by A54, A58, XBOOLE_0: 5;

                then

                 A61: ((a2 +* (n .--> b2)) . a) = (a1 . a) by A39, A42, A45, A60, FUNCT_4:def 1;

                

                 A62: a in (( dom a2) \/ ( dom (n .--> b2))) by A46, A47, A58, XBOOLE_0:def 3;

                

                 A63: a in ( dom a2) by A46, A47, A57, FUNCT_1: 1;

                then not a in ( dom (n .--> b2)) by A55, A62, XBOOLE_0: 5;

                then b = (a2 . a) by A59, A61, A62, FUNCT_4:def 1;

                hence [a, b] in a2 by A63, FUNCT_1: 1;

              end;

              assume

               A64: [a, b] in a2;

              then

               A65: a in ( dom a2) by FUNCT_1: 1;

              

               A66: b = (a2 . a) by A64, FUNCT_1: 1;

              

               A67: a in (( dom a2) \/ ( dom (n .--> b2))) by A65, XBOOLE_0:def 3;

              then not a in ( dom (n .--> b2)) by A55, A65, XBOOLE_0: 5;

              then

               A68: ((a1 +* (n .--> b1)) . a) = (a2 . a) by A39, A42, A45, A67, FUNCT_4:def 1;

              

               A69: a in (( dom a1) \/ ( dom (n .--> b1))) by A46, A47, A65, XBOOLE_0:def 3;

              

               A70: a in ( dom a1) by A46, A47, A64, FUNCT_1: 1;

              then not a in ( dom (n .--> b1)) by A54, A69, XBOOLE_0: 5;

              then b = (a1 . a) by A66, A68, A69, FUNCT_4:def 1;

              hence [a, b] in a1 by A70, FUNCT_1: 1;

            end;

            

             A71: n in ( dom (n .--> b1)) by TARSKI:def 1;

            then

             A72: n in (( dom a1) \/ ( dom (n .--> b1))) by XBOOLE_0:def 3;

            

             A73: n in ( dom (n .--> b2)) by TARSKI:def 1;

            then n in (( dom a2) \/ ( dom (n .--> b2))) by XBOOLE_0:def 3;

            

            then ((a1 +* (n .--> b1)) . n) = ((n .--> b2) . n) by A39, A42, A45, A73, FUNCT_4:def 1

            .= b2 by FUNCOP_1: 72;

            

            then b2 = ((n .--> b1) . n) by A71, A72, FUNCT_4:def 1

            .= b1 by FUNCOP_1: 72;

            hence x1 = x2 by A41, A44, A56, RELAT_1:def 2;

          end;

          then

           A74: f is one-to-one by FUNCT_1:def 4;

          now

            let y be object;

            thus y in ( rng f) implies y in the carrier of ( product p);

            assume y in the carrier of ( product p);

            then y in ( product ( Carrier p)) by YELLOW_1:def 4;

            then

            consider g be Function such that

             A75: y = g and

             A76: ( dom g) = ( dom ( Carrier p)) and

             A77: for x be object st x in ( dom ( Carrier p)) holds (g . x) in (( Carrier p) . x) by CARD_3:def 5;

            

             A78: ( dom ( Carrier p)) = (n + 1) by PARTFUN1:def 2;

            

             A79: (n + 1) = { i where i be Nat : i < (n + 1) } by AXIOMS: 4;

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

            then

             A80: n in (n + 1) by A79;

            set a = (g | n), b = (g . n);

            set x = [a, b];

            

             A81: ( dom ( Carrier (p | ns))) = ns by PARTFUN1:def 2;

            

             A82: ( dom a) = (( dom g) /\ ( Segm n)) by RELAT_1: 61

            .= (( Segm (n + 1)) /\ ( Segm n)) by A76, PARTFUN1:def 2;

            then

             A83: ( dom a) = ( Segm n) by NAT_1: 63, XBOOLE_1: 28;

            

             A84: ( dom a) = ( dom ( Carrier (p | ns))) by A1, A81, A82, XBOOLE_1: 28;

            now

              let x be object;

              assume x in ( dom ( Carrier (p | ns)));

              then

               A85: x in n by A1;

              

               A86: ( Segm n) c= ( Segm (n + 1)) by NAT_1: 63;

              

               A87: (a . x) = (g . x) by A85, FUNCT_1: 49;

              

               A88: (g . x) in (( Carrier p) . x) by A77, A78, A85, A86;

              

               A89: ex R1 be 1-sorted st (R1 = (p . x)) & ((( Carrier p) . x) = the carrier of R1) by A85, A86, PRALG_1:def 15;

              ex R2 be 1-sorted st (R2 = ((p | ns) . x)) & ((( Carrier (p | ns)) . x) = the carrier of R2) by A1, A85, PRALG_1:def 15;

              hence (a . x) in (( Carrier (p | ns)) . x) by A1, A85, A87, A88, A89, FUNCT_1: 49;

            end;

            then a in ( product ( Carrier (p | ns))) by A84, CARD_3: 9;

            then

             A90: a in the carrier of ( product (p | ns)) by YELLOW_1:def 4;

            ex R1 be 1-sorted st (R1 = (p . n)) & ((( Carrier p) . n) = the carrier of R1) by A80, PRALG_1:def 15;

            then

             A91: b in the carrier of (p . ne) by A2, A77, A78;

            then [a, b] in [:the carrier of ( product (p | ns)), the carrier of (p . ne):] by A90, ZFMISC_1: 87;

            then

             A92: x in ( dom f) by FUNCT_2:def 1;

            x is Element of CP9 by A90, A91, ZFMISC_1: 87;

            then

            consider ta be Function, tb be Element of pne2 such that ta in ppns2 and

             A93: x = [ta, tb] and

             A94: (f . x) = (ta +* (n .--> tb)) by A36;

            

             A95: ta = a by A93, XTUPLE_0: 1;

            

             A96: tb = b by A93, XTUPLE_0: 1;

            now

              let i,j be object;

              hereby

                assume

                 A97: [i, j] in (a +* (n .--> b));

                then i in ( dom (a +* (n .--> b))) by FUNCT_1: 1;

                then

                 A98: i in (( dom a) \/ ( dom (n .--> b))) by FUNCT_4:def 1;

                then

                 A99: i in (( Segm n) \/ {n}) by A83;

                

                 A100: ((a +* (n .--> b)) . i) = j by A97, FUNCT_1: 1;

                per cases ;

                  suppose

                   A101: i in ( dom (n .--> b));

                  then i in {n};

                  then

                   A102: i = n by TARSKI:def 1;

                  ((a +* (n .--> b)) . i) = ((n .--> b) . i) by A98, A101, FUNCT_4:def 1

                  .= b by A102, FUNCOP_1: 72;

                  then

                   A103: (g . i) = j by A97, A102, FUNCT_1: 1;

                  i in ( dom g) by A76, A78, A99, AFINSQ_1: 2;

                  hence [i, j] in g by A103, FUNCT_1: 1;

                end;

                  suppose

                   A104: not i in ( dom (n .--> b));

                  then not i in {n};

                  then

                   A105: i in n by A99, XBOOLE_0:def 3;

                  ((a +* (n .--> b)) . i) = (a . i) by A98, A104, FUNCT_4:def 1;

                  then

                   A106: (g . i) = j by A100, A105, FUNCT_1: 49;

                  i in ( dom g) by A76, A78, A99, AFINSQ_1: 2;

                  hence [i, j] in g by A106, FUNCT_1: 1;

                end;

              end;

              assume

               A107: [i, j] in g;

              then

               A108: i in ( Segm (n + 1)) by A76, A78, FUNCT_1: 1;

              then

               A109: i in (( Segm n) \/ {n}) by AFINSQ_1: 2;

              ( dom (a +* (n .--> b))) = (( dom a) \/ ( dom (n .--> b))) by FUNCT_4:def 1

              .= (( Segm n) \/ {n}) by A83;

              then

               A110: i in ( dom (a +* (n .--> b))) by A108, AFINSQ_1: 2;

              then

               A111: i in (( dom a) \/ ( dom (n .--> b))) by FUNCT_4:def 1;

              per cases ;

                suppose

                 A112: i in ( dom (n .--> b));

                then i in {n};

                then

                 A113: i = n by TARSKI:def 1;

                ((a +* (n .--> b)) . i) = ((n .--> b) . i) by A111, A112, FUNCT_4:def 1

                .= b by A113, FUNCOP_1: 72

                .= j by A107, A113, FUNCT_1: 1;

                hence [i, j] in (a +* (n .--> b)) by A110, FUNCT_1: 1;

              end;

                suppose

                 A114: not i in ( dom (n .--> b));

                then not i in {n};

                then

                 A115: i in n by A109, XBOOLE_0:def 3;

                ((a +* (n .--> b)) . i) = (a . i) by A111, A114, FUNCT_4:def 1

                .= (g . i) by A115, FUNCT_1: 49

                .= j by A107, FUNCT_1: 1;

                hence [i, j] in (a +* (n .--> b)) by A110, FUNCT_1: 1;

              end;

            end;

            then (f . x) = y by A75, A94, A95, A96, RELAT_1:def 2;

            hence y in ( rng f) by A92, FUNCT_1:def 3;

          end;

          then

           A116: ( rng f) = the carrier of ( product p) by TARSKI: 2;

          now

            let x,y be Element of S;

            

             A117: x is Element of CP by YELLOW_3:def 2;

            then

            consider xa be Function, xb be Element of pne2 such that

             A118: xa in ppns2 and

             A119: x = [xa, xb] and

             A120: (f . x) = (xa +* (n .--> xb)) by A36;

            ( dom f) = CP9 by FUNCT_2:def 1;

            then (f . x) in the carrier of ( product p) by A116, A117, FUNCT_1:def 3;

            then

             A121: (f9 . x) in ( product ( Carrier p)) by YELLOW_1:def 4;

            y is Element of CP by YELLOW_3:def 2;

            then

            consider ya be Function, yb be Element of pne2 such that

             A122: ya in ppns2 and

             A123: y = [ya, yb] and

             A124: (f . y) = (ya +* (n .--> yb)) by A36;

            

             A125: xa in ( product ( Carrier (p | ns))) by A118, YELLOW_1:def 4;

            then

             A126: ex gx be Function st (xa = gx) & (( dom gx) = ( dom ( Carrier (p | ns)))) & (for x be object st x in ( dom ( Carrier (p | ns))) holds (gx . x) in (( Carrier (p | ns)) . x)) by CARD_3:def 5;

            then

             A127: ( dom xa) = n by A1, PARTFUN1:def 2;

            then

             A128: (( dom xa) \/ ( dom (n .--> xb))) = (( Segm n) \/ {n});

            ya in ( product ( Carrier (p | ns))) by A122, YELLOW_1:def 4;

            then

             A129: ex gy be Function st (ya = gy) & (( dom gy) = ( dom ( Carrier (p | ns)))) & (for x be object st x in ( dom ( Carrier (p | ns))) holds (gy . x) in (( Carrier (p | ns)) . x)) by CARD_3:def 5;

            then

             A130: ( dom ya) = n by A1, PARTFUN1:def 2;

            then

             A131: (( dom ya) \/ ( dom (n .--> yb))) = (( Segm n) \/ {n});

            reconsider xa9 = xa as Element of ( product (p | ns)) by A118;

            reconsider ya9 = ya as Element of ( product (p | ns)) by A122;

            hereby

              assume x <= y;

              then [x, y] in the InternalRel of S;

              then

               A132: [x, y] in ["the InternalRel of ( product (p | ns)), the InternalRel of (p . ne)"] by YELLOW_3:def 2;

              then

               A133: [(( [x, y] `1 ) `1 ), (( [x, y] `2 ) `1 )] in the InternalRel of ( product (p | ns)) by YELLOW_3: 10;

              

               A134: [(( [x, y] `1 ) `2 ), (( [x, y] `2 ) `2 )] in the InternalRel of (p . ne) by A132, YELLOW_3: 10;

              

               A135: [xa, ya] in the InternalRel of ( product (p | ns)) by A123, A133, A119;

              

               A136: xa in ( product ( Carrier (p | ns))) by A118, YELLOW_1:def 4;

              xa9 <= ya9 by A135;

              then

              consider ffx,ggx be Function such that

               A137: ffx = xa and

               A138: ggx = ya and

               A139: for i be object st i in n holds ex RR be RelStr, xxi,yyi be Element of RR st RR = ((p | ns) . i) & xxi = (ffx . i) & yyi = (ggx . i) & xxi <= yyi by A1, A136, YELLOW_1:def 4;

              

               A140: [xb, yb] in the InternalRel of (p . ne) by A123, A134, A119;

              reconsider xb9 = xb as Element of (p . ne);

              reconsider yb9 = yb as Element of (p . ne);

              

               A141: xb9 <= yb9 by A140;

              ex f1,g1 be Function st f1 = (f . x) & g1 = (f . y) & for i be object st i in ( Segm (n + 1)) holds ex R be RelStr, xi,yi be Element of R st R = (p . i) & xi = (f1 . i) & yi = (g1 . i) & xi <= yi

              proof

                set f1 = (xa +* (n .--> xb)), g1 = (ya +* (n .--> yb));

                take f1, g1;

                thus f1 = (f . x) by A120;

                thus g1 = (f . y) by A124;

                let i be object such that

                 A142: i in ( Segm (n + 1));

                

                 A143: i in (( Segm n) \/ {n}) by A142, AFINSQ_1: 2;

                set R = (p . i);

                set xi = (f1 . i);

                set yi = (g1 . i);

                i in ( dom p) by A142, PARTFUN1:def 2;

                then (p . i) in ( rng p) by FUNCT_1:def 3;

                then

                reconsider R as RelStr by YELLOW_1:def 3;

                

                 A144: i in (( dom xa) \/ ( dom (n .--> xb))) by A128, A142, AFINSQ_1: 2;

                now

                  per cases ;

                    suppose

                     A145: i in ( dom (n .--> xb));

                    then i in {n};

                    then

                     A146: i = n by TARSKI:def 1;

                    (f1 . i) = ((n .--> xb) . i) by A144, A145, FUNCT_4:def 1;

                    hence xi is Element of R by A2, A146, FUNCOP_1: 72;

                  end;

                    suppose

                     A147: not i in ( dom (n .--> xb));

                    then

                     A148: not i in {n};

                    then

                     A149: i in n by A143, XBOOLE_0:def 3;

                    

                     A150: i in ( dom ( Carrier (p | ns))) by A3, A143, A148, XBOOLE_0:def 3;

                    (f1 . i) = (xa . i) by A144, A147, FUNCT_4:def 1;

                    then

                     A151: xi in (( Carrier (p | ns)) . i) by A126, A150;

                    ex R2 be 1-sorted st (R2 = ((p | ns) . i)) & ((( Carrier (p | ns)) . i) = the carrier of R2) by A1, A149, PRALG_1:def 15;

                    hence xi is Element of R by A1, A149, A151, FUNCT_1: 49;

                  end;

                end;

                then

                reconsider xi as Element of R;

                

                 A152: i in (( dom ya) \/ ( dom (n .--> yb))) by A131, A142, AFINSQ_1: 2;

                now

                  per cases ;

                    suppose

                     A153: i in ( dom (n .--> yb));

                    then i in {n};

                    then

                     A154: i = n by TARSKI:def 1;

                    (g1 . i) = ((n .--> yb) . i) by A152, A153, FUNCT_4:def 1;

                    hence yi is Element of R by A2, A154, FUNCOP_1: 72;

                  end;

                    suppose

                     A155: not i in ( dom (n .--> yb));

                    then

                     A156: not i in {n};

                    then

                     A157: i in n by A143, XBOOLE_0:def 3;

                    

                     A158: i in ( dom ( Carrier (p | ns))) by A3, A143, A156, XBOOLE_0:def 3;

                    (g1 . i) = (ya . i) by A152, A155, FUNCT_4:def 1;

                    then

                     A159: yi in (( Carrier (p | ns)) . i) by A129, A158;

                    ex R2 be 1-sorted st (R2 = ((p | ns) . i)) & ((( Carrier (p | ns)) . i) = the carrier of R2) by A1, A157, PRALG_1:def 15;

                    hence yi is Element of R by A1, A157, A159, FUNCT_1: 49;

                  end;

                end;

                then

                reconsider yi as Element of R;

                take R, xi, yi;

                thus R = (p . i);

                thus xi = (f1 . i);

                thus yi = (g1 . i);

                per cases by A143, XBOOLE_0:def 3;

                  suppose

                   A160: i in n;

                  

                   A161: not i in {n}

                  proof

                    assume i in {n};

                    then n in n by A160, TARSKI:def 1;

                    hence contradiction;

                  end;

                  then

                   A162: not i in ( dom (n .--> xb));

                   not i in ( dom (n .--> yb)) by A161;

                  then

                   A163: yi = (ya . i) by A152, FUNCT_4:def 1;

                  consider RR be RelStr, xxi,yyi be Element of RR such that

                   A164: RR = ((p | ns) . i) and

                   A165: xxi = (ffx . i) and

                   A166: yyi = (ggx . i) and

                   A167: xxi <= yyi by A139, A160;

                  RR = R by A1, A160, A164, FUNCT_1: 49;

                  hence thesis by A137, A138, A144, A162, A163, A165, A166, A167, FUNCT_4:def 1;

                end;

                  suppose

                   A168: i in {n};

                  then

                   A169: i = n by TARSKI:def 1;

                  

                   A170: i in ( dom (n .--> xb)) by A168;

                  

                   A171: i in ( dom (n .--> yb)) by A168;

                  

                   A172: xi = ((n .--> xb) . i) by A144, A170, FUNCT_4:def 1

                  .= xb by A169, FUNCOP_1: 72;

                  yi = ((n .--> yb) . i) by A152, A171, FUNCT_4:def 1

                  .= yb by A169, FUNCOP_1: 72;

                  hence thesis by A2, A141, A168, A172, TARSKI:def 1;

                end;

              end;

              hence (f9 . x) <= (f9 . y) by A121, YELLOW_1:def 4;

            end;

            assume (f9 . x) <= (f9 . y);

            then

            consider f1,g1 be Function such that

             A173: f1 = (f . x) and

             A174: g1 = (f . y) and

             A175: for i be object st i in (n + 1) holds ex R be RelStr, xi,yi be Element of R st R = (p . i) & xi = (f1 . i) & yi = (g1 . i) & xi <= yi by A121, YELLOW_1:def 4;

            now

              set f2 = xa9, g2 = ya9;

              reconsider f2, g2 as Function;

              take f2, g2;

              thus f2 = xa9 & g2 = ya9;

              let i be object such that

               A176: i in ns;

              

               A177: not i in {n}

              proof

                assume i in {n};

                then

                 A: i = n by TARSKI:def 1;

                then

                reconsider i as set;

                 not i in i;

                hence contradiction by A, A1, A176;

              end;

              then

               A178: not i in ( dom (n .--> yb));

              

               A179: not i in ( dom (n .--> xb)) by A177;

              set R = ((p | ns) . i);

              i in ( dom (p | ns)) by A176, PARTFUN1:def 2;

              then ((p | ns) . i) in ( rng (p | ns)) by FUNCT_1:def 3;

              then

              reconsider R as RelStr by YELLOW_1:def 3;

              take R;

              set xi = (xa . i), yi = (ya . i);

              

               A180: i in (( dom xa) \/ ( dom (n .--> xb))) by A1, A127, A176, XBOOLE_0:def 3;

              

               A181: i in ( dom ( Carrier (p | ns))) by A176, PARTFUN1:def 2;

              ex R2 be 1-sorted st (R2 = ((p | ns) . i)) & ((( Carrier (p | ns)) . i) = the carrier of R2) by A176, PRALG_1:def 15;

              then

              reconsider xi as Element of R by A126, A181;

              

               A182: i in (( dom ya) \/ ( dom (n .--> yb))) by A1, A130, A176, XBOOLE_0:def 3;

              ex R2 be 1-sorted st (R2 = ((p | ns) . i)) & ((( Carrier (p | ns)) . i) = the carrier of R2) by A176, PRALG_1:def 15;

              then

              reconsider yi as Element of R by A129, A181;

              take xi, yi;

              thus R = ((p | ns) . i) & xi = (f2 . i) & yi = (g2 . i);

              consider R2 be RelStr, xi2,yi2 be Element of R2 such that

               A183: R2 = (p . i) and

               A184: xi2 = (f1 . i) and

               A185: yi2 = (g1 . i) and

               A186: xi2 <= yi2 by A175, A176;

              

               A187: R2 = R by A176, A183, FUNCT_1: 49;

              ((xa +* (n .--> xb)) . i) = xi by A179, A180, FUNCT_4:def 1;

              hence xi <= yi by A120, A124, A173, A174, A178, A182, A184, A185, A186, A187, FUNCT_4:def 1;

            end;

            then xa9 <= ya9 by A125, YELLOW_1:def 4;

            then

             A188: [xa, ya] in the InternalRel of ( product (p | ns));

            

             A189: [(( [x, y] `1 ) `1 ), (( [x, y] `2 ) `1 )] in the InternalRel of ( product (p | ns)) by A123, A119, A188;

            consider Rn be RelStr, xni,yni be Element of Rn such that

             A190: Rn = (p . ne) and

             A191: xni = (f1 . n) and

             A192: yni = (g1 . n) and

             A193: xni <= yni by A2, A175;

            

             A194: [xni, yni] in the InternalRel of (p . ne) by A190, A193;

            

             A195: n in ( dom (n .--> xb)) by TARSKI:def 1;

            then n in (( dom xa) \/ ( dom (n .--> xb))) by XBOOLE_0:def 3;

            

            then

             A196: ((xa +* (n .--> xb)) . n) = ((n .--> xb) . n) by A195, FUNCT_4:def 1

            .= xb by FUNCOP_1: 72;

            

             A197: n in ( dom (n .--> yb)) by TARSKI:def 1;

            then n in (( dom ya) \/ ( dom (n .--> yb))) by XBOOLE_0:def 3;

            

            then

             A198: ((ya +* (n .--> yb)) . n) = ((n .--> yb) . n) by A197, FUNCT_4:def 1

            .= yb by FUNCOP_1: 72;

            

             A199: [(( [x, y] `1 ) `2 ), (( [x, y] `2 ) `2 )] in the InternalRel of (p . ne) by A120, A123, A124, A173, A174, A191, A192, A194, A196, A198, A119;

            

             A200: ( [x, y] `1 ) = [xa, xb] by A119;

            ( [x, y] `2 ) = [ya, yb] by A123;

            then [x, y] in ["the InternalRel of ( product (p | ns)), the InternalRel of (p . ne)"] by A189, A199, A200, YELLOW_3: 10;

            then [x, y] in the InternalRel of S by YELLOW_3:def 2;

            hence x <= y;

          end;

          hence f is isomorphic by A74, A116, WAYBEL_0: 66;

        end;

        hence thesis by WAYBEL_1:def 8;

      end;

    end;

    theorem :: DICKSON:42

    

     Th41: for n be non zero Nat, p be RelStr-yielding ManySortedSet of ( Segm n) st for i be Element of ( Segm n) holds (p . i) is Dickson & (p . i) is quasi_ordered holds ( product p) is quasi_ordered & ( product p) is Dickson

    proof

      defpred P[ non zero Nat] means for p be RelStr-yielding ManySortedSet of ( Segm $1) st for i be Element of ( Segm $1) holds (p . i) is Dickson & (p . i) is quasi_ordered holds ( product p) is quasi_ordered & ( product p) is Dickson;

      

       A1: P[1]

      proof

        let p be RelStr-yielding ManySortedSet of ( Segm 1) such that

         A2: for i be Element of ( Segm 1) holds (p . i) is Dickson & (p . i) is quasi_ordered;

        reconsider z = 0 as Element of ( Segm 1) by CARD_1: 49, TARSKI:def 1;

        

         A3: (p . z) is Dickson by A2;

        

         A4: (p . z) is quasi_ordered by A2;

        ( Segm 1) = { 0 } by CARD_1: 49;

        then ((p . z),( product p)) are_isomorphic by Th38;

        hence thesis by A3, A4, Th37;

      end;

       A5:

      now

        let n be non zero Nat;

        assume

         A6: P[n];

        thus P[(n + 1)]

        proof

          let p be RelStr-yielding ManySortedSet of ( Segm (n + 1));

          assume

           A7: for i be Element of ( Segm (n + 1)) holds (p . i) is Dickson & (p . i) is quasi_ordered;

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

          then

          reconsider ns = ( Segm n) as Subset of ( Segm (n + 1)) by NAT_1: 39;

          

           A8: (n + 1) = { k where k be Nat : k < (n + 1) } by AXIOMS: 4;

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

          then n in (n + 1) by A8;

          then

          reconsider ne = n as Element of ( Segm (n + 1));

          reconsider pns = (p | ns) as RelStr-yielding ManySortedSet of ( Segm n);

          

           A9: for i be Element of ( Segm n) holds (pns . i) is Dickson & (pns . i) is quasi_ordered

          proof

            let i be Element of ( Segm n);

            

             A10: (pns . i) = (p . i) by FUNCT_1: 49;

            

             A11: n = { k where k be Nat : k < n } by AXIOMS: 4;

            i in n;

            then

            consider k be Nat such that

             A12: k = i and

             A13: k < n by A11;

            k < (n + 1) by A13, NAT_1: 13;

            then i in (n + 1) by A8, A12;

            then

            reconsider i9 = i as Element of (n + 1);

            i9 = i;

            hence thesis by A7, A10;

          end;

          then

           A14: ( product pns) is Dickson by A6;

          

           A15: ( product pns) is quasi_ordered by A6, A9;

          

           A16: (p . ne) is Dickson by A7;

          

           A17: (p . ne) is quasi_ordered by A7;

          then

           A18: [:( product (p | ns)), (p . ne):] is Dickson by A14, A15, A16, Th36;

          

           A19: [:( product (p | ns)), (p . ne):] is quasi_ordered by A15, A17;

          ( [:( product (p | ns)), (p . ne):],( product p)) are_isomorphic by Th40;

          hence thesis by A18, A19, Th37;

        end;

      end;

      thus for n be non zero Nat holds P[n] from NAT_1:sch 10( A1, A5);

    end;

    

     Lm1: for p be RelStr-yielding ManySortedSet of {} holds ( product p) is non empty & ( product p) is quasi_ordered & ( product p) is Dickson & ( product p) is antisymmetric

    proof

      let p be RelStr-yielding ManySortedSet of {} ;

      

       A1: ( product p) = RelStr (# { {} }, ( id { {} }) #) by YELLOW_1: 26;

      set pp = ( product p), cpp = the carrier of pp, ipp = the InternalRel of pp;

      

       A2: ipp = ( id { {} }) by YELLOW_1: 26;

      thus pp is non empty by YELLOW_1: 26;

      thus pp is quasi_ordered by YELLOW_1: 26;

      thus pp is Dickson

      proof

        let N be Subset of cpp;

        per cases by A1, ZFMISC_1: 33;

          suppose

           A3: N = {} ;

          take B = {} ;

          N = ( {} cpp) by A3;

          hence B is_Dickson-basis_of (N,pp);

          thus thesis;

        end;

          suppose

           A4: N = { {} };

          take B = { {} };

          thus B is_Dickson-basis_of (N,pp)

          proof

            thus B c= N by A4;

            let a be Element of pp;

            assume

             A5: a in N;

            take b = a;

            thus b in B by A4, A5;

             [b, a] in ( id { {} }) by A4, A5, RELAT_1:def 10;

            hence thesis by A2;

          end;

          thus thesis;

        end;

      end;

      thus thesis by YELLOW_1: 26;

    end;

    registration

      let p be RelStr-yielding ManySortedSet of {} ;

      cluster ( product p) -> non empty;

      coherence by Lm1;

      cluster ( product p) -> antisymmetric;

      coherence by Lm1;

      cluster ( product p) -> quasi_ordered;

      coherence by Lm1;

      ::$Notion-Name

      cluster ( product p) -> Dickson;

      coherence by Lm1;

    end

    definition

      :: DICKSON:def14

      func NATOrd -> Relation of NAT equals { [x, y] where x,y be Element of NAT : x <= y };

      correctness

      proof

        set NO = { [x, y] where x,y be Element of NAT : x <= y };

        now

          let z be object;

          assume z in NO;

          then ex x,y be Element of NAT st (z = [x, y]) & (x <= y);

          hence z in [: NAT , NAT :];

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: DICKSON:43

    

     Th42: NATOrd is_reflexive_in NAT ;

    theorem :: DICKSON:44

    

     Th43: NATOrd is_antisymmetric_in NAT

    proof

      let x,y be object such that x in NAT and y in NAT and

       A1: [x, y] in NATOrd and

       A2: [y, x] in NATOrd ;

      consider x9,y9 be Element of NAT such that

       A3: [x, y] = [x9, y9] and

       A4: x9 <= y9 by A1;

      

       A5: x = x9 by A3, XTUPLE_0: 1;

      

       A6: y = y9 by A3, XTUPLE_0: 1;

      consider y2,x2 be Element of NAT such that

       A7: [y, x] = [y2, x2] and

       A8: y2 <= x2 by A2;

      

       A9: y2 = y9 by A6, A7, XTUPLE_0: 1;

      x2 = x9 by A5, A7, XTUPLE_0: 1;

      hence thesis by A4, A5, A6, A8, A9, XXREAL_0: 1;

    end;

    theorem :: DICKSON:45

    

     Th44: NATOrd is_strongly_connected_in NAT

    proof

      now

        let x,y be object such that

         A1: x in NAT and

         A2: y in NAT ;

        thus [x, y] in NATOrd or [y, x] in NATOrd

        proof

          assume that

           A3: not [x, y] in NATOrd and

           A4: not [y, x] in NATOrd ;

          reconsider x, y as Element of NAT by A1, A2;

          per cases ;

            suppose x <= y;

            hence contradiction by A3;

          end;

            suppose y <= x;

            hence contradiction by A4;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: DICKSON:46

    

     Th45: NATOrd is_transitive_in NAT

    proof

      let x,y,z be object such that x in NAT and y in NAT and z in NAT and

       A1: [x, y] in NATOrd and

       A2: [y, z] in NATOrd ;

      consider x1,y1 be Element of NAT such that

       A3: [x, y] = [x1, y1] and

       A4: x1 <= y1 by A1;

      

       A5: x = x1 by A3, XTUPLE_0: 1;

      

       A6: y = y1 by A3, XTUPLE_0: 1;

      consider y2,z2 be Element of NAT such that

       A7: [y, z] = [y2, z2] and

       A8: y2 <= z2 by A2;

      

       A9: y = y2 by A7, XTUPLE_0: 1;

      

       A10: z = z2 by A7, XTUPLE_0: 1;

      x1 <= z2 by A4, A6, A8, A9, XXREAL_0: 2;

      hence thesis by A5, A10;

    end;

    definition

      :: DICKSON:def15

      func OrderedNAT -> non empty RelStr equals RelStr (# NAT , NATOrd #);

      correctness ;

    end

     Lm2:

    now

      for x,y be Element of OrderedNAT st not x <= y holds y <= x by Th44;

      hence OrderedNAT is connected by WAYBEL_0:def 29;

    end;

    registration

      cluster OrderedNAT -> connected;

      coherence by Lm2;

      cluster OrderedNAT -> Dickson;

      coherence

      proof

        set IR9 = the InternalRel of ( OrderedNAT \~ ), CR9 = the carrier of ( OrderedNAT \~ );

        now

          let N be set such that

           A1: N c= CR9 and

           A2: N <> {} ;

          

           A3: ex k be object st k in N by A2, XBOOLE_0:def 1;

          defpred P[ Nat] means $1 in N;

          

           A4: ex k be Nat st P[k] by A1, A3;

          consider m be Nat such that

           A5: P[m] and

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

          reconsider m as Element of OrderedNAT by ORDINAL1:def 12;

          thus ex m be object st m in N & (IR9 -Seg m) misses N

          proof

            take m;

            thus m in N by A5;

            now

              assume ((IR9 -Seg m) /\ N) <> {} ;

              then

              consider z be object such that

               A7: z in ((IR9 -Seg m) /\ N) by XBOOLE_0:def 1;

              

               A8: z in (IR9 -Seg m) by A7, XBOOLE_0:def 4;

              

               A9: z in N by A7, XBOOLE_0:def 4;

              

               A10: z <> m by A8, WELLORD1: 1;

              

               A11: [z, m] in IR9 by A8, WELLORD1: 1;

              then [z, m] in NATOrd ;

              then

              consider x,y be Element of NAT such that

               A12: [z, m] = [x, y] and x <= y;

              

               A13: z = x by A12, XTUPLE_0: 1;

              

               A14: m = y by A12, XTUPLE_0: 1;

              then y <= x by A6, A9, A13;

              then [y, x] in NATOrd ;

              hence contradiction by A10, A11, A13, A14, Th43;

            end;

            hence thesis by XBOOLE_0:def 7;

          end;

        end;

        then IR9 is_well_founded_in CR9 by WELLORD1:def 3;

        then ( OrderedNAT \~ ) is well_founded by WELLFND1:def 2;

        hence thesis by Th26;

      end;

      cluster OrderedNAT -> quasi_ordered;

      coherence

      proof

        

         A15: OrderedNAT is reflexive by Th42;

         OrderedNAT is transitive by Th45;

        hence thesis by A15;

      end;

      cluster OrderedNAT -> antisymmetric;

      coherence by Th43;

      cluster OrderedNAT -> transitive;

      coherence by Th45;

      cluster OrderedNAT -> well_founded;

      coherence

      proof

        set ir = the InternalRel of OrderedNAT ;

        now

          given f be sequence of OrderedNAT such that

           A16: f is descending;

          

           A17: ( dom f) = NAT by FUNCT_2:def 1;

          reconsider rf = ( rng f) as non empty Subset of NAT ;

          set m = ( min rf);

          m in ( rng f) by XXREAL_2:def 7;

          then

          consider d be object such that

           A18: d in ( dom f) and

           A19: m = (f . d) by FUNCT_1:def 3;

          reconsider d as Element of NAT by A18;

          

           A20: (f . (d + 1)) <> (f . d) by A16, WELLFND1:def 6;

           [(f . (d + 1)), (f . d)] in ir by A16, WELLFND1:def 6;

          then

          consider x,y be Element of NAT such that

           A21: [(f . (d + 1)), (f . d)] = [x, y] and

           A22: x <= y;

          reconsider fd1 = (f . (d + 1)), fd = (f . d) as Element of NAT ;

          

           A23: (f . (d + 1)) = x by A21, XTUPLE_0: 1;

          (f . d) = y by A21, XTUPLE_0: 1;

          then

           A24: fd1 < fd by A20, A22, A23, XXREAL_0: 1;

          (f . (d + 1)) in rf by A17, FUNCT_1: 3;

          hence contradiction by A19, A24, XXREAL_2:def 7;

        end;

        hence thesis by WELLFND1: 14;

      end;

    end

     Lm3:

    now

      let n be Element of NAT ;

      set pp = ( product (n --> OrderedNAT ));

      per cases ;

        suppose n is zero;

        then n = 0 ;

        then n is empty;

        hence pp is non empty & pp is Dickson & pp is quasi_ordered & pp is antisymmetric;

      end;

        suppose n is non zero;

        then

        reconsider n9 = n as non zero Element of NAT ;

        reconsider p = (n9 --> OrderedNAT ) as RelStr-yielding ManySortedSet of ( Segm n9);

        thus ( product (n --> OrderedNAT )) is non empty;

        for i be Element of ( Segm n9) holds (p . i) is Dickson & (p . i) is quasi_ordered;

        hence ( product (n --> OrderedNAT )) is Dickson & ( product (n --> OrderedNAT )) is quasi_ordered by Th41;

        ( product p) is antisymmetric;

        hence ( product (n --> OrderedNAT )) is antisymmetric;

      end;

    end;

    registration

      let n be Element of NAT ;

      cluster ( product (n --> OrderedNAT )) -> non empty;

      coherence ;

      cluster ( product (n --> OrderedNAT )) -> Dickson;

      coherence by Lm3;

      cluster ( product (n --> OrderedNAT )) -> quasi_ordered;

      coherence by Lm3;

      cluster ( product (n --> OrderedNAT )) -> antisymmetric;

      coherence by Lm3;

    end

    theorem :: DICKSON:47

    for M be RelStr st M is Dickson & M is quasi_ordered holds [:M, OrderedNAT :] is quasi_ordered & [:M, OrderedNAT :] is Dickson by Th36;

    theorem :: DICKSON:48

    

     Th47: for R,S be non empty RelStr st R is Dickson & S is quasi_ordered & the InternalRel of R c= the InternalRel of S & the carrier of R = the carrier of S holds (S \~ ) is well_founded

    proof

      let R,S be non empty RelStr such that

       A1: R is Dickson and

       A2: S is quasi_ordered and

       A3: the InternalRel of R c= the InternalRel of S and

       A4: the carrier of R = the carrier of S;

      S is Dickson by A1, A3, A4, Th27;

      hence thesis by A2, Th32;

    end;

    theorem :: DICKSON:49

    for R be non empty RelStr st R is quasi_ordered holds R is Dickson iff for S be non empty RelStr st S is quasi_ordered & the InternalRel of R c= the InternalRel of S & the carrier of R = the carrier of S holds (S \~ ) is well_founded

    proof

      let R be non empty RelStr such that

       A1: R is quasi_ordered;

      

       A2: R is reflexive by A1;

      

       A3: R is transitive by A1;

      set IR = the InternalRel of R, CR = the carrier of R;

      thus R is Dickson implies for S be non empty RelStr st S is quasi_ordered & IR c= the InternalRel of S & CR = the carrier of S holds (S \~ ) is well_founded by Th47;

      assume

       A4: for S be non empty RelStr st S is quasi_ordered & IR c= the InternalRel of S & CR = the carrier of S holds (S \~ ) is well_founded;

      now

        assume not R is Dickson;

        then not (for N be non empty Subset of R holds ( min-classes N) is finite & ( min-classes N) is non empty) by A1, Th31;

        then

        consider f be sequence of R such that

         A5: for i,j be Nat st i < j holds not (f . i) <= (f . j) by A1, Th30;

        defpred P[ object, object] means [$1, $2] in IR or ex i,j be Element of NAT st i < j & [$1, (f . j)] in IR & [(f . i), $2] in IR;

        consider QOE be Relation of CR, CR such that

         A6: for x,y be object holds [x, y] in QOE iff x in CR & y in CR & P[x, y] from RELSET_1:sch 1;

        set S = RelStr (# CR, QOE #);

        now

          let x,y be object such that

           A7: [x, y] in IR;

          

           A8: x in ( dom IR) by A7, XTUPLE_0:def 12;

          y in ( rng IR) by A7, XTUPLE_0:def 13;

          hence [x, y] in QOE by A6, A7, A8;

        end;

        then

         A9: IR c= the InternalRel of S by RELAT_1:def 3;

        

         A10: IR is_reflexive_in CR by A2;

        then for x be object st x in CR holds [x, x] in QOE by A6;

        then QOE is_reflexive_in CR;

        then

         A11: S is reflexive;

        

         A12: IR is_transitive_in CR by A3;

        now

          let x,y,z be object such that

           A13: x in CR and

           A14: y in CR and

           A15: z in CR and

           A16: [x, y] in QOE and

           A17: [y, z] in QOE;

          now

            per cases by A6, A16;

              suppose

               A18: [x, y] in IR;

              now

                per cases by A6, A17;

                  suppose [y, z] in IR;

                  then [x, z] in IR by A12, A13, A14, A15, A18;

                  hence [x, z] in QOE by A6, A13, A15;

                end;

                  suppose ex i,j be Element of NAT st i < j & [y, (f . j)] in IR & [(f . i), z] in IR;

                  then

                  consider i,j be Element of NAT such that

                   A19: i < j and

                   A20: [y, (f . j)] in IR and

                   A21: [(f . i), z] in IR;

                   [x, (f . j)] in IR by A12, A13, A14, A18, A20;

                  hence [x, z] in QOE by A6, A13, A15, A19, A21;

                end;

              end;

              hence [x, z] in QOE;

            end;

              suppose ex i,j be Element of NAT st i < j & [x, (f . j)] in IR & [(f . i), y] in IR;

              then

              consider i,j be Element of NAT such that

               A22: i < j and

               A23: [x, (f . j)] in IR and

               A24: [(f . i), y] in IR;

              now

                per cases by A6, A17;

                  suppose [y, z] in IR;

                  then [(f . i), z] in IR by A12, A14, A15, A24;

                  hence [x, z] in QOE by A6, A13, A15, A22, A23;

                end;

                  suppose ex a,b be Element of NAT st a < b & [y, (f . b)] in IR & [(f . a), z] in IR;

                  then

                  consider a,b be Element of NAT such that

                   A25: a < b and

                   A26: [y, (f . b)] in IR and

                   A27: [(f . a), z] in IR;

                   [(f . i), (f . b)] in IR by A12, A14, A24, A26;

                  then (f . i) <= (f . b);

                  then not i < b by A5;

                  then a <= i by A25, XXREAL_0: 2;

                  then a < j by A22, XXREAL_0: 2;

                  hence [x, z] in QOE by A6, A13, A15, A23, A27;

                end;

              end;

              hence [x, z] in QOE;

            end;

          end;

          hence [x, z] in QOE;

        end;

        then QOE is_transitive_in CR;

        then S is transitive;

        then S is quasi_ordered by A11;

        then

         A28: (S \~ ) is well_founded by A4, A9;

        reconsider f9 = f as sequence of (S \~ );

        now

          let n be Nat;

          reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

          

           A29: n < (n + 1) by NAT_1: 13;

          then not (f . n1) <= (f . (n1 + 1)) by A5;

          then

           A30: not [(f . n), (f . (n + 1))] in IR;

          hence (f9 . (n + 1)) <> (f9 . n) by A10;

          

           A31: [(f9 . (n + 1)), (f9 . (n + 1))] in IR by A10;

          

           A32: [(f9 . n), (f9 . n)] in IR by A10;

           A33:

          now

            assume [(f9 . n), (f9 . (n + 1))] in QOE;

            then ex i,j be Element of NAT st i < j & [(f9 . n), (f . j)] in IR & [(f . i), (f9 . (n + 1))] in IR by A6, A30;

            then

            consider l,k be Element of NAT such that

             A34: k < l and

             A35: [(f9 . n), (f . l)] in IR and

             A36: [(f . k), (f9 . (n + 1))] in IR;

            

             A37: (f . n) <= (f . l) by A35;

            

             A38: (f . k) <= (f . (n + 1)) by A36;

            

             A39: l <= n1 by A5, A37;

            

             A40: (n + 1) <= k by A5, A38;

            l < (n + 1) by A39, NAT_1: 13;

            hence contradiction by A34, A40, XXREAL_0: 2;

          end;

          

           A41: [(f9 . (n1 + 1)), (f9 . n1)] in QOE by A6, A29, A31, A32;

           not [(f9 . (n + 1)), (f9 . n)] in (QOE ~ ) by A33, RELAT_1:def 7;

          hence [(f9 . (n + 1)), (f9 . n)] in the InternalRel of (S \~ ) by A41, XBOOLE_0:def 5;

        end;

        then f9 is descending by WELLFND1:def 6;

        hence contradiction by A28, WELLFND1: 14;

      end;

      hence thesis;

    end;