bagorder.miz



    begin

    theorem :: BAGORDER:1

    

     Th1: for x,y,z be set st z in x & z in y holds (x \ {z}) = (y \ {z}) implies x = y

    proof

      let x,y,z be set;

      assume that

       A1: z in x and

       A2: z in y;

      assume

       A3: (x \ {z}) = (y \ {z});

      

      thus x = (x \/ {z}) by A1, ZFMISC_1: 40

      .= ((y \ {z}) \/ {z}) by A3, XBOOLE_1: 39

      .= (y \/ {z}) by XBOOLE_1: 39

      .= y by A2, ZFMISC_1: 40;

    end;

    theorem :: BAGORDER:2

    for n,k be Element of NAT holds k in ( Seg n) iff (k - 1) is Element of NAT & (k - 1) < n

    proof

      let n,k be Element of NAT ;

      

       A1: ( Seg n) = { x where x be Nat : 1 <= x & x <= n } by FINSEQ_1:def 1;

      hereby

        assume k in ( Seg n);

        then

        consider x be Nat such that

         A2: k = x and

         A3: 1 <= x and

         A4: x <= n by A1;

        set x1 = (k - 1), n1 = (n - 1);

         0 < x by A3;

        then

        reconsider x1 as Element of NAT by A2, NAT_1: 20;

        x1 = (k - 1);

        hence (k - 1) is Element of NAT ;

         0 < n by A3, A4;

        then

        reconsider n1 as Element of NAT by NAT_1: 20;

        (k + ( - 1)) <= (n + ( - 1)) by A2, A4, XREAL_1: 6;

        then x1 <= n1;

        then (k - 1) < (n1 + 1) by NAT_1: 13;

        hence (k - 1) < n;

      end;

      assume that

       A5: (k - 1) is Element of NAT and

       A6: (k - 1) < n;

      reconsider k1 = (k - 1) as Element of NAT by A5;

       0 <= k1;

      then

       A7: ( 0 qua Nat + 1) <= ((k - 1) + 1) by XREAL_1: 6;

      ((k - 1) + 1) <= ((n - 1) + 1) by A5, A6, NAT_1: 13;

      hence thesis by A1, A7;

    end;

    registration

      let f be finite-support Function, X be set;

      cluster (f | X) -> finite-support;

      coherence

      proof

        ( support (f | X)) c= ( support f)

        proof

          let x be object;

          assume

           A1: x in ( support (f | X));

          then

           A2: ((f | X) . x) <> 0 by PRE_POLY:def 7;

          ( support (f | X)) c= ( dom (f | X)) by PRE_POLY: 37;

          then (f . x) <> 0 by A1, A2, FUNCT_1: 47;

          hence thesis by PRE_POLY:def 7;

        end;

        hence thesis by PRE_POLY:def 8;

      end;

    end

    ::$Canceled

    theorem :: BAGORDER:4

    

     Th3: for fs be FinSequence of NAT holds ( Sum fs) = 0 iff fs = (( len fs) |-> 0 )

    proof

      let fs be FinSequence of NAT ;

      hereby

        assume

         A1: ( Sum fs) = 0 ;

        

         A2: ( Seg ( len fs)) = ( dom fs) by FINSEQ_1:def 3;

        

         A3: ( Seg ( len fs)) = ( dom (( len fs) |-> 0 )) by FUNCOP_1: 13;

        now

          let k be Nat such that

           A4: k in ( Seg ( len fs));

          now

            assume

             A5: (fs . k) <> 0 ;

            for k be Nat st k in ( dom fs) holds 0 <= (fs . k);

            hence contradiction by A1, A2, A4, A5, RVSUM_1: 85;

          end;

          hence (fs . k) = ((( len fs) |-> 0 ) . k) by A4, FUNCOP_1: 7;

        end;

        hence fs = (( len fs) |-> 0 ) by A2, A3, FINSEQ_1: 13;

      end;

      assume fs = (( len fs) |-> 0 );

      hence thesis by RVSUM_1: 81;

    end;

    definition

      let n,i,j be Nat, b be ManySortedSet of n;

      :: BAGORDER:def1

      func (i,j) -cut b -> ManySortedSet of (j -' i) means

      : Def1: for k be Element of NAT st k in (j -' i) holds (it . k) = (b . (i + k));

      existence

      proof

        defpred P[ object, object] means ex k1 be Element of NAT st k1 = $1 & $2 = (b . (i + k1));

        

         A1: for x be object st x in (j -' i) holds ex y be object st P[x, y]

        proof

          let x be object such that

           A2: x in (j -' i);

          (j -' i) = { k where k be Nat : k < (j -' i) } by AXIOMS: 4;

          then ex k be Nat st (x = k) & (k < (j -' i)) by A2;

          then

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

          consider y be set such that

           A3: y = (b . (i + x9));

          take y;

          thus P[x, y] by A3;

        end;

        consider f be Function such that

         A4: ( dom f) = (j -' i) and

         A5: for k be object st k in (j -' i) holds P[k, (f . k)] from CLASSES1:sch 1( A1);

        reconsider f as ManySortedSet of (j -' i) by A4, PARTFUN1:def 2, RELAT_1:def 18;

        take f;

        let k be Element of NAT ;

        assume k in (j -' i);

        then ex k9 be Element of NAT st (k9 = k) & ((f . k) = (b . (i + k9))) by A5;

        hence thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be ManySortedSet of (j -' i) such that

         A6: for k be Element of NAT st k in (j -' i) holds (IT1 . k) = (b . (i + k)) and

         A7: for k be Element of NAT st k in (j -' i) holds (IT2 . k) = (b . (i + k));

        

         A8: (j -' i) = ( dom IT1) by PARTFUN1:def 2;

        

         A9: (j -' i) = ( dom IT2) by PARTFUN1:def 2;

        now

          let x be object such that

           A10: x in (j -' i);

          (j -' i) = { k where k be Nat : k < (j -' i) } by AXIOMS: 4;

          then ex k be Nat st (x = k) & (k < (j -' i)) by A10;

          then

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

          (IT1 . x) = (b . (i + x9)) by A6, A10;

          hence (IT1 . x) = (IT2 . x) by A7, A10;

        end;

        hence IT1 = IT2 by A8, A9, FUNCT_1: 2;

      end;

    end

    registration

      let n,i,j be Nat, b be natural-valued ManySortedSet of n;

      cluster ((i,j) -cut b) -> natural-valued;

      coherence

      proof

        now

          let y be object;

          assume y in ( rng ((i,j) -cut b));

          then

          consider x be object such that

           A1: x in ( dom ((i,j) -cut b)) and

           A2: (((i,j) -cut b) . x) = y by FUNCT_1:def 3;

          

           A3: x in (j -' i) by A1;

          (j -' i) = { k where k be Nat : k < (j -' i) } by AXIOMS: 4;

          then ex k be Nat st (k = x) & (k < (j -' i)) by A3;

          then

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

          y = (b . (i + x)) by A2, A3, Def1;

          hence y in NAT ;

        end;

        then ( rng ((i,j) -cut b)) c= NAT ;

        hence thesis by VALUED_0:def 6;

      end;

    end

    registration

      let n,i,j be Element of NAT , b be finite-support ManySortedSet of n;

      cluster ((i,j) -cut b) -> finite-support;

      coherence ;

    end

    theorem :: BAGORDER:5

    

     Th4: for n,i be Nat, a,b be ManySortedSet of n holds a = b iff (( 0 ,(i + 1)) -cut a) = (( 0 ,(i + 1)) -cut b) & (((i + 1),n) -cut a) = (((i + 1),n) -cut b)

    proof

      let n,i be Nat, a,b be ManySortedSet of n;

      set CUTA1 = (( 0 ,(i + 1)) -cut a), CUTA2 = (((i + 1),n) -cut a);

      set CUTB1 = (( 0 ,(i + 1)) -cut b), CUTB2 = (((i + 1),n) -cut b);

      thus a = b implies CUTA1 = CUTB1 & CUTA2 = CUTB2;

      assume that

       A1: CUTA1 = CUTB1 and

       A2: CUTA2 = CUTB2;

       A3:

      now

        let k be Element of NAT such that

         A4: k in (i + 1);

        ((i + 1) -' 0 ) = (((i + 1) + 0 qua Nat) -' 0 );

        then

         A5: k in ((i + 1) -' 0 ) by A4, NAT_D: 34;

        then (CUTB1 . k) = (b . ( 0 qua Nat + k)) by Def1;

        hence (a . k) = (b . k) by A1, A5, Def1;

      end;

       A6:

      now

        let x be Element of NAT such that

         A7: x >= (i + 1) and

         A8: x < n;

        set k = (x -' (i + 1));

        (x - (i + 1)) >= ((i + 1) - (i + 1)) by A7, XREAL_1: 9;

        then

         A9: k = (x - (i + 1)) by XREAL_0:def 2;

        n >= (i + 1) by A7, A8, XXREAL_0: 2;

        then (n - (i + 1)) >= ((i + 1) - (i + 1)) by XREAL_1: 9;

        then

         A10: (n -' (i + 1)) = (n - (i + 1)) by XREAL_0:def 2;

        (x - (i + 1)) < (n - (i + 1)) by A8, XREAL_1: 14;

        then

         A11: k in ( Segm (n -' (i + 1))) by A9, A10, NAT_1: 44;

        then (CUTB2 . k) = (b . ((i + 1) + k)) by Def1;

        hence (a . x) = (b . x) by A2, A9, A11, Def1;

      end;

      now

        let x9 be object such that

         A12: x9 in n;

        n = { k where k be Nat : k < n } by AXIOMS: 4;

        then

         A13: ex k be Nat st (k = x9) & (k < n) by A12;

        then

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

        per cases ;

          suppose x in (i + 1);

          hence (a . x9) = (b . x9) by A3;

        end;

          suppose not x in ( Segm (i + 1));

          then x >= (i + 1) by NAT_1: 44;

          hence (a . x9) = (b . x9) by A6, A13;

        end;

      end;

      hence thesis by PBOOLE: 3;

    end;

    definition

      let x be non empty set, n be non zero Element of NAT ;

      :: BAGORDER:def2

      func Fin (x,n) -> set equals { y where y be Subset of x : y is finite & y is non empty & ( card y) c= n };

      coherence ;

    end

    registration

      let x be non empty set, n be non zero Element of NAT ;

      cluster ( Fin (x,n)) -> non empty;

      coherence

      proof

        set y = the Element of x;

        

         A1: ( 0 qua Nat + 1) < (n + 1) by XREAL_1: 8;

        now

          per cases by ORDINAL1: 16;

            suppose 1 c= n;

            hence ( card {y}) c= n by CARD_1: 30;

          end;

            suppose

             A2: n in 1;

            1 = { k where k be Nat : k < 1 } by AXIOMS: 4;

            then ex k be Nat st (k = n) & (k < 1) by A2;

            hence ( card {y}) c= n by A1, NAT_1: 13;

          end;

        end;

        then {y} in ( Fin (x,n));

        hence thesis;

      end;

    end

    theorem :: BAGORDER:6

    

     Th5: for R be antisymmetric transitive non empty RelStr, X be finite Subset of R st X <> {} holds ex x be Element of R st x in X & x is_maximal_wrt (X,the InternalRel of R)

    proof

      let R be antisymmetric transitive non empty RelStr, X be finite Subset of R;

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

      

       A1: IR is_transitive_in CR by ORDERS_2:def 3;

      

       A2: IR is_antisymmetric_in CR by ORDERS_2:def 4;

      

       A3: X is finite;

      defpred P[ set] means (($1 <> {} ) implies (ex x be Element of R st x in $1 & x is_maximal_wrt ($1,IR)));

      

       A4: P[ {} ];

      now

        let y,B be set such that

         A5: y in X and B c= X and

         A6: B <> {} implies ex x be Element of R st x in B & x is_maximal_wrt (B,IR);

        reconsider y9 = y as Element of R by A5;

        assume (B \/ {y}) <> {} ;

        per cases ;

          suppose

           A7: B = {} ;

          take y9;

          thus y9 in (B \/ {y}) by A7, TARSKI:def 1;

          

           A8: y9 in (B \/ {y}) by A7, TARSKI:def 1;

           not ex z be set st z in (B \/ {y9}) & z <> y9 & [y9, z] in IR by A7, TARSKI:def 1;

          hence y9 is_maximal_wrt ((B \/ {y}),IR) by A8, WAYBEL_4:def 23;

        end;

          suppose B <> {} ;

          then

          consider x be Element of R such that

           A9: x in B and

           A10: x is_maximal_wrt (B,IR) by A6;

          now

            per cases ;

              suppose

               A11: [x, y] in IR;

              take y9;

              

               A12: y in {y} by TARSKI:def 1;

              hence y9 in (B \/ {y}) by XBOOLE_0:def 3;

               A13:

              now

                given z be set such that

                 A14: z in (B \/ {y}) and

                 A15: z <> y and

                 A16: [y, z] in IR;

                

                 A17: y9 in CR;

                z in CR by A16, ZFMISC_1: 87;

                then

                 A18: [x, z] in IR by A1, A11, A16, A17;

                per cases by A14, XBOOLE_0:def 3;

                  suppose

                   A19: z in B;

                  now

                    per cases ;

                      suppose

                       A20: z = x;

                      then x = y9 by A2, A11, A16;

                      hence contradiction by A15, A20;

                    end;

                      suppose z <> x;

                      hence contradiction by A10, A18, A19, WAYBEL_4:def 23;

                    end;

                  end;

                  hence contradiction;

                end;

                  suppose z in {y};

                  hence contradiction by A15, TARSKI:def 1;

                end;

              end;

              y9 in (B \/ {y}) by A12, XBOOLE_0:def 3;

              hence y9 is_maximal_wrt ((B \/ {y}),IR) by A13, WAYBEL_4:def 23;

            end;

              suppose

               A21: [y, x] in IR;

              take x;

              thus x in (B \/ {y}) by A9, XBOOLE_0:def 3;

               A22:

              now

                assume ex z be set st z in (B \/ {y}) & z <> x & [x, z] in IR;

                then

                consider z be set such that

                 A23: z in (B \/ {y}) and

                 A24: z <> x and

                 A25: [x, z] in IR;

                per cases by A23, XBOOLE_0:def 3;

                  suppose z in B;

                  hence contradiction by A10, A24, A25, WAYBEL_4:def 23;

                end;

                  suppose z in {y};

                  then

                   A26: z = y by TARSKI:def 1;

                  z in CR by A25, ZFMISC_1: 87;

                  hence contradiction by A2, A21, A24, A25, A26;

                end;

              end;

              x in (B \/ {y}) by A9, XBOOLE_0:def 3;

              hence x is_maximal_wrt ((B \/ {y}),IR) by A22, WAYBEL_4:def 23;

            end;

              suppose

               A27: not [x, y] in IR & not [y, x] in IR;

              take x;

              thus x in (B \/ {y}) by A9, XBOOLE_0:def 3;

               A28:

              now

                assume ex z be set st z in (B \/ {y}) & z <> x & [x, z] in IR;

                then

                consider z be set such that

                 A29: z in (B \/ {y}) and

                 A30: z <> x and

                 A31: [x, z] in IR;

                per cases by A29, XBOOLE_0:def 3;

                  suppose z in B;

                  hence contradiction by A10, A30, A31, WAYBEL_4:def 23;

                end;

                  suppose z in {y};

                  hence contradiction by A27, A31, TARSKI:def 1;

                end;

              end;

              x in (B \/ {y}) by A9, XBOOLE_0:def 3;

              hence x is_maximal_wrt ((B \/ {y}),IR) by A28, WAYBEL_4:def 23;

            end;

          end;

          hence ex x be Element of R st x in (B \/ {y}) & x is_maximal_wrt ((B \/ {y}),IR);

        end;

      end;

      then

       A32: for y,B be set st y in X & B c= X & P[B] holds P[(B \/ {y})];

      thus P[X] from FINSET_1:sch 2( A3, A4, A32);

    end;

    theorem :: BAGORDER:7

    

     Th6: for R be antisymmetric transitive non empty RelStr, X be finite Subset of R st X <> {} holds ex x be Element of R st x in X & x is_minimal_wrt (X,the InternalRel of R)

    proof

      let R be antisymmetric transitive non empty RelStr, X be finite Subset of R;

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

      

       A1: IR is_transitive_in CR by ORDERS_2:def 3;

      

       A2: IR is_antisymmetric_in CR by ORDERS_2:def 4;

      

       A3: X is finite;

      defpred P[ set] means (($1 <> {} ) implies (ex x be Element of R st x in $1 & x is_minimal_wrt ($1,IR)));

      

       A4: P[ {} ];

      now

        let y,B be set such that

         A5: y in X and B c= X and

         A6: B <> {} implies ex x be Element of R st x in B & x is_minimal_wrt (B,IR);

        reconsider y9 = y as Element of R by A5;

        assume (B \/ {y}) <> {} ;

        per cases ;

          suppose

           A7: B = {} ;

          take y9;

          thus y9 in (B \/ {y}) by A7, TARSKI:def 1;

          

           A8: y9 in (B \/ {y}) by A7, TARSKI:def 1;

           not ex z be set st z in (B \/ {y9}) & z <> y9 & [z, y9] in IR by A7, TARSKI:def 1;

          hence y9 is_minimal_wrt ((B \/ {y}),IR) by A8, WAYBEL_4:def 25;

        end;

          suppose B <> {} ;

          then

          consider x be Element of R such that

           A9: x in B and

           A10: x is_minimal_wrt (B,IR) by A6;

          now

            per cases ;

              suppose

               A11: [y, x] in IR;

              take y9;

              

               A12: y in {y} by TARSKI:def 1;

              hence y9 in (B \/ {y}) by XBOOLE_0:def 3;

               A13:

              now

                assume ex z be set st z in (B \/ {y}) & z <> y & [z, y] in IR;

                then

                consider z be set such that

                 A14: z in (B \/ {y}) and

                 A15: z <> y and

                 A16: [z, y] in IR;

                

                 A17: y9 in CR;

                z in CR by A16, ZFMISC_1: 87;

                then

                 A18: [z, x] in IR by A1, A11, A16, A17;

                per cases by A14, XBOOLE_0:def 3;

                  suppose

                   A19: z in B;

                  now

                    per cases ;

                      suppose

                       A20: z = x;

                      then x = y9 by A2, A11, A16;

                      hence contradiction by A15, A20;

                    end;

                      suppose z <> x;

                      hence contradiction by A10, A18, A19, WAYBEL_4:def 25;

                    end;

                  end;

                  hence contradiction;

                end;

                  suppose z in {y};

                  hence contradiction by A15, TARSKI:def 1;

                end;

              end;

              y9 in (B \/ {y}) by A12, XBOOLE_0:def 3;

              hence y9 is_minimal_wrt ((B \/ {y}),IR) by A13, WAYBEL_4:def 25;

            end;

              suppose

               A21: [x, y] in IR;

              take x;

              thus x in (B \/ {y}) by A9, XBOOLE_0:def 3;

               A22:

              now

                assume ex z be set st z in (B \/ {y}) & z <> x & [z, x] in IR;

                then

                consider z be set such that

                 A23: z in (B \/ {y}) and

                 A24: z <> x and

                 A25: [z, x] in IR;

                per cases by A23, XBOOLE_0:def 3;

                  suppose z in B;

                  hence contradiction by A10, A24, A25, WAYBEL_4:def 25;

                end;

                  suppose z in {y};

                  then

                   A26: z = y by TARSKI:def 1;

                  z in CR by A25, ZFMISC_1: 87;

                  hence contradiction by A2, A21, A24, A25, A26;

                end;

              end;

              x in (B \/ {y}) by A9, XBOOLE_0:def 3;

              hence x is_minimal_wrt ((B \/ {y}),IR) by A22, WAYBEL_4:def 25;

            end;

              suppose

               A27: not [x, y] in IR & not [y, x] in IR;

              take x;

              thus x in (B \/ {y}) by A9, XBOOLE_0:def 3;

               A28:

              now

                assume ex z be set st z in (B \/ {y}) & z <> x & [z, x] in IR;

                then

                consider z be set such that

                 A29: z in (B \/ {y}) and

                 A30: z <> x and

                 A31: [z, x] in IR;

                per cases by A29, XBOOLE_0:def 3;

                  suppose z in B;

                  hence contradiction by A10, A30, A31, WAYBEL_4:def 25;

                end;

                  suppose z in {y};

                  hence contradiction by A27, A31, TARSKI:def 1;

                end;

              end;

              x in (B \/ {y}) by A9, XBOOLE_0:def 3;

              hence x is_minimal_wrt ((B \/ {y}),IR) by A28, WAYBEL_4:def 25;

            end;

          end;

          hence ex x be Element of R st x in (B \/ {y}) & x is_minimal_wrt ((B \/ {y}),IR);

        end;

      end;

      then

       A32: for y,B be set st y in X & B c= X & P[B] holds P[(B \/ {y})];

      thus P[X] from FINSET_1:sch 2( A3, A4, A32);

    end;

    theorem :: BAGORDER:8

    for R be non empty antisymmetric transitive RelStr, f be sequence of R st f is descending holds for j,i be Nat st i < j holds (f . i) <> (f . j) & [(f . j), (f . i)] in the InternalRel of R

    proof

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

       A1: f is descending;

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

      

       A2: IR is_transitive_in CR by ORDERS_2:def 3;

      

       A3: IR is_antisymmetric_in CR by ORDERS_2:def 4;

      defpred P[ Nat] means (for i be Nat st i < $1 holds (f . i) <> (f . $1) & [(f . $1), (f . i)] in IR);

      

       A4: P[ 0 ];

      now

        let j be Nat such that

         A5: for i be Nat st i < j holds (f . i) <> (f . j) & [(f . j), (f . i)] in IR;

        let i be Nat such that

         A6: i < (j + 1);

        now

          per cases by XXREAL_0: 1;

            suppose i > j;

            hence (f . i) <> (f . (j + 1)) & [(f . (j + 1)), (f . i)] in IR by A6, NAT_1: 13;

          end;

            suppose i = j;

            hence (f . i) <> (f . (j + 1)) & [(f . (j + 1)), (f . i)] in IR by A1;

          end;

            suppose i < j;

            then

             A7: [(f . j), (f . i)] in IR by A5;

            

             A8: (f . (j + 1)) <> (f . j) by A1;

             [(f . (j + 1)), (f . j)] in IR by A1;

            hence (f . i) <> (f . (j + 1)) & [(f . (j + 1)), (f . i)] in IR by A2, A3, A7, A8;

          end;

        end;

        hence (f . i) <> (f . (j + 1)) & [(f . (j + 1)), (f . i)] in IR;

      end;

      then

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

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

    end;

    definition

      let R be non empty RelStr, s be sequence of R;

      :: BAGORDER:def3

      attr s is non-increasing means for i be Nat holds [(s . (i + 1)), (s . i)] in the InternalRel of R;

    end

    theorem :: BAGORDER:9

    

     Th8: for R be non empty transitive RelStr, f be sequence of R st f is non-increasing holds for j,i be Nat st i < j holds [(f . j), (f . i)] in the InternalRel of R

    proof

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

       A1: f is non-increasing;

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

      

       A2: IR is_transitive_in CR by ORDERS_2:def 3;

      defpred P[ Nat] means (for i be Nat st i < $1 holds [(f . $1), (f . i)] in IR);

      

       A3: P[ 0 ];

      now

        let j be Nat such that

         A4: for i be Nat st i < j holds [(f . j), (f . i)] in IR;

        let i be Nat such that

         A5: i < (j + 1);

        now

          per cases by XXREAL_0: 1;

            suppose i > j;

            hence [(f . (j + 1)), (f . i)] in IR by A5, NAT_1: 13;

          end;

            suppose i = j;

            hence [(f . (j + 1)), (f . i)] in IR by A1;

          end;

            suppose i < j;

            then

             A6: [(f . j), (f . i)] in IR by A4;

             [(f . (j + 1)), (f . j)] in IR by A1;

            hence [(f . (j + 1)), (f . i)] in IR by A2, A6;

          end;

        end;

        hence [(f . (j + 1)), (f . i)] in IR;

      end;

      then

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

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

    end;

    theorem :: BAGORDER:10

    

     Th9: for R be non empty transitive RelStr, s be sequence of R st R is well_founded & s is non-increasing holds ex p be Nat st for r be Nat st p <= r holds (s . p) = (s . r)

    proof

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

       A1: R is well_founded and

       A2: s is non-increasing;

      set cr = the carrier of R, ir = the InternalRel of R;

      

       A3: ir is_well_founded_in cr by A1;

      

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

      ( rng s) c= cr by RELAT_1:def 19;

      then

      consider a be object such that

       A5: a in ( rng s) and

       A6: (ir -Seg a) misses ( rng s) by A3, WELLORD1:def 3;

      

       A7: ((ir -Seg a) /\ ( rng s)) = {} by A6, XBOOLE_0:def 7;

      consider i be object such that

       A8: i in ( dom s) and

       A9: (s . i) = a by A5, FUNCT_1:def 3;

      reconsider i as Nat by A8;

      assume not thesis;

      then

      consider r be Nat such that

       A10: i <= r and

       A11: (s . i) <> (s . r);

      i < r by A10, A11, XXREAL_0: 1;

      then [(s . r), (s . i)] in ir by A2, Th8;

      then

       A12: (s . r) in (ir -Seg a) by A9, A11, WELLORD1: 1;

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

      (s . r) in ( rng s) by A4, FUNCT_1: 3;

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

    end;

    theorem :: BAGORDER:11

    

     Th10: for X be set, R be Order of X, B be finite Subset of X, x be object st B = {x} holds ( SgmX (R,B)) = <*x*>

    proof

      let X be set, R be Order of X, B be finite Subset of X, x be object;

      assume

       A1: B = {x};

      set fin = <*x*>;

      

       A2: ( rng fin) = B by A1, FINSEQ_1: 38;

      then

      reconsider fin as FinSequence of X by FINSEQ_1:def 4;

      for n,m be Nat st n in ( dom fin) & m in ( dom fin) & n < m holds (fin /. n) <> (fin /. m) & [(fin /. n), (fin /. m)] in R

      proof

        let n,m be Nat;

        assume that

         A3: n in ( dom fin) and

         A4: m in ( dom fin) and

         A5: n < m;

        assume not ((fin /. n) <> (fin /. m) & [(fin /. n), (fin /. m)] in R);

        n in ( Seg 1) & m in ( Seg 1) by A3, A4, FINSEQ_1: 38;

        then n = 1 & m = 1 by FINSEQ_1: 2, TARSKI:def 1;

        hence contradiction by A5;

      end;

      hence ( SgmX (R,B)) = <*x*> by A2, PRE_POLY: 9;

    end;

    begin

    definition

      let n be Ordinal, b be bag of n;

      :: BAGORDER:def4

      func TotDegree b -> Nat means

      : Def4: ex f be FinSequence of NAT st it = ( Sum f) & f = (b * ( SgmX (( RelIncl n),( support b))));

      existence

      proof

        set f = (b * ( SgmX (( RelIncl n),( support b))));

        

         A1: ( dom b) = n by PARTFUN1:def 2;

        ( rng b) c= NAT by VALUED_0:def 6;

        then

        reconsider bb = b as Function of n, NAT by A1, FUNCT_2: 2;

        bb = b;

        then

        reconsider f as FinSequence of NAT by FINSEQ_2: 32;

        reconsider x = ( Sum f) as Nat;

        take x;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: BAGORDER:12

    

     Th11: for n be Ordinal, b be bag of n, s be finite Subset of n, f,g be FinSequence of NAT st f = (b * ( SgmX (( RelIncl n),( support b)))) & g = (b * ( SgmX (( RelIncl n),(( support b) \/ s)))) holds ( Sum f) = ( Sum g)

    proof

      let n be Ordinal, b be bag of n, s be finite Subset of n, f,g be FinSequence of NAT such that

       A1: f = (b * ( SgmX (( RelIncl n),( support b)))) and

       A2: g = (b * ( SgmX (( RelIncl n),(( support b) \/ s))));

      set sb = ( support b);

      set sbs = (sb \/ s);

      set sbs9b = (sbs \ sb);

      set xsb = ( SgmX (( RelIncl n),sb)), xsbs = ( SgmX (( RelIncl n),sbs));

      set xsbs9b = ( SgmX (( RelIncl n),sbs9b));

      set xs = (xsb ^ xsbs9b);

      set h = (b * xs);

      

       A3: ( dom b) = n by PARTFUN1:def 2;

      

       A4: ( field ( RelIncl n)) = n by WELLORD2:def 1;

      

       A5: ( RelIncl n) is being_linear-order by ORDERS_1: 19;

      

       A6: ( RelIncl n) linearly_orders n by A4, ORDERS_1: 19, ORDERS_1: 37;

      

       A7: ( RelIncl n) linearly_orders sbs by A4, A5, ORDERS_1: 37, ORDERS_1: 38;

      

       A8: ( RelIncl n) linearly_orders sb by A4, A5, ORDERS_1: 37, ORDERS_1: 38;

      

       A9: ( RelIncl n) linearly_orders sbs9b by A4, A5, ORDERS_1: 37, ORDERS_1: 38;

      

       A10: ( rng xsbs) = sbs by A7, PRE_POLY:def 2;

      

       A11: ( rng xsb) = sb by A8, PRE_POLY:def 2;

      

       A12: ( rng xsbs9b) = sbs9b by A9, PRE_POLY:def 2;

      then

       A13: ( rng xs) = (sb \/ sbs9b) by A11, FINSEQ_1: 31;

      then

      reconsider h as FinSequence by A3, FINSEQ_1: 16;

      per cases ;

        suppose n = {} ;

        hence thesis by A1, A2;

      end;

        suppose n <> {} ;

        then

        reconsider n as non empty Ordinal;

        reconsider xsb, xsbs9b as FinSequence of n;

        ( rng b) c= REAL ;

        then

        reconsider b as Function of n, REAL by A3, FUNCT_2: 2;

        ( rng h) c= ( rng b) by RELAT_1: 26;

        then ( rng h) c= REAL by XBOOLE_1: 1;

        then

        reconsider h as FinSequence of REAL by FINSEQ_1:def 4;

        reconsider gr = g as FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

        

         A14: sb misses sbs9b by XBOOLE_1: 79;

        

         A15: sbs = ((sb \/ sb) \/ s)

        .= (sb \/ sbs) by XBOOLE_1: 4

        .= (sb \/ sbs9b) by XBOOLE_1: 39;

        ( len xs) = (( len xsb) + ( len xsbs9b)) by FINSEQ_1: 22

        .= (( card sb) + ( len xsbs9b)) by A6, ORDERS_1: 38, PRE_POLY: 11

        .= (( card sb) + ( card sbs9b)) by A6, ORDERS_1: 38, PRE_POLY: 11

        .= ( card sbs) by A15, CARD_2: 40, XBOOLE_1: 79

        .= ( len xsbs) by A6, ORDERS_1: 38, PRE_POLY: 11;

        then

         A16: ( dom xsbs) = ( dom xs) by FINSEQ_3: 29;

        

         A17: xsbs is one-to-one by A6, ORDERS_1: 38, PRE_POLY: 10;

        

         A18: ( rng xsb) = sb by A8, PRE_POLY:def 2;

        

         A19: ( rng xsbs9b) = sbs9b by A9, PRE_POLY:def 2;

        

         A20: xsb is one-to-one by A6, ORDERS_1: 38, PRE_POLY: 10;

        xsbs9b is one-to-one by A6, ORDERS_1: 38, PRE_POLY: 10;

        then xs is one-to-one by A14, A18, A19, A20, FINSEQ_3: 91;

        then

         A21: (gr,h) are_fiberwise_equipotent by A2, A3, A10, A13, A15, A16, A17, CLASSES1: 83, RFINSEQ: 26;

        now

          thus ( dom xsbs9b) = ( dom (b * xsbs9b)) by A3, A12, RELAT_1: 27;

          

           A22: ( dom xsbs9b) = ( Seg ( len xsbs9b)) by FINSEQ_1:def 3;

          hence ( dom xsbs9b) = ( dom (( len xsbs9b) |-> 0 )) by FUNCOP_1: 13;

          let x be object;

          assume

           A23: x in ( dom xsbs9b);

          then (xsbs9b . x) in ( rng xsbs9b) by FUNCT_1: 3;

          then not (xsbs9b . x) in sb by A12, XBOOLE_0:def 5;

          then (b . (xsbs9b . x)) = 0 by PRE_POLY:def 7;

          

          hence ((b * xsbs9b) . x) = 0 by A23, FUNCT_1: 13

          .= ((( len xsbs9b) |-> 0 ) . x) by A22, A23, FUNCOP_1: 7;

        end;

        then

         A24: (b * xsbs9b) = (( len xsbs9b) |-> 0 qua Real) by FUNCT_1: 2;

        h = ((b * xsb) ^ (b * xsbs9b)) by FINSEQOP: 9;

        

        then ( Sum h) = (( Sum (b * xsb)) + ( Sum (b * xsbs9b))) by RVSUM_1: 75

        .= (( Sum f) + 0 qua Nat) by A1, A24, RVSUM_1: 81;

        hence thesis by A21, RFINSEQ: 9;

      end;

    end;

    theorem :: BAGORDER:13

    

     Th12: for n be Ordinal, a,b be bag of n holds ( TotDegree (a + b)) = (( TotDegree a) + ( TotDegree b))

    proof

      let n be Ordinal, a,b be bag of n;

      

       A1: ( field ( RelIncl n)) = n by WELLORD2:def 1;

      

       A2: ( RelIncl n) is being_linear-order by ORDERS_1: 19;

      consider fab be FinSequence of NAT such that

       A3: ( TotDegree (a + b)) = ( Sum fab) and

       A4: fab = ((a + b) * ( SgmX (( RelIncl n),( support (a + b))))) by Def4;

      consider fa be FinSequence of NAT such that

       A5: ( TotDegree a) = ( Sum fa) and

       A6: fa = (a * ( SgmX (( RelIncl n),( support a)))) by Def4;

      consider fb be FinSequence of NAT such that

       A7: ( TotDegree b) = ( Sum fb) and

       A8: fb = (b * ( SgmX (( RelIncl n),( support b)))) by Def4;

      reconsider fab9 = fab as FinSequence of REAL by FINSEQ_2: 24, NUMBERS: 19;

      set sasb = (( support a) \/ ( support b));

      reconsider sasb as finite Subset of n;

      set s = ( SgmX (( RelIncl n),sasb));

      set fa9b = (a * s), fb9a = (b * s);

      ( RelIncl n) linearly_orders sasb by A1, A2, ORDERS_1: 37, ORDERS_1: 38;

      then

       A9: ( rng s) = sasb by PRE_POLY:def 2;

      

       A10: ( support (a + b)) = sasb by PRE_POLY: 38;

      

       A11: ( dom a) = n by PARTFUN1:def 2;

      

       A12: ( dom b) = n by PARTFUN1:def 2;

      then

      reconsider fa9b, fb9a as FinSequence by A9, A11, FINSEQ_1: 16;

      

       A13: ( rng fa9b) c= ( rng a) by RELAT_1: 26;

      

       A14: ( rng fb9a) c= ( rng b) by RELAT_1: 26;

      

       A15: ( rng fa9b) c= NAT by VALUED_0:def 6;

      

       A16: ( rng fb9a) c= NAT by VALUED_0:def 6;

      

       A17: ( rng fa9b) c= REAL by A13, XBOOLE_1: 1;

      ( rng fb9a) c= REAL by A14, XBOOLE_1: 1;

      then

      reconsider fa9b, fb9a as FinSequence of REAL by A17, FINSEQ_1:def 4;

      reconsider fa9bn = fa9b, fb9an = fb9a as FinSequence of NAT by A15, A16, FINSEQ_1:def 4;

      set ln = ( len fab);

      

       A18: ( dom (a + b)) = n by PARTFUN1:def 2;

      

       A19: ( Seg ln) = ( dom fab) by FINSEQ_1:def 3

      .= ( dom s) by A4, A9, A10, A18, RELAT_1: 27;

      then

       A20: ( Seg ln) = ( dom fa9b) by A9, A11, RELAT_1: 27;

      

       A21: ( Seg ln) = ( dom fb9a) by A9, A12, A19, RELAT_1: 27;

      

       A22: ( Sum fa) = ( Sum fa9bn) by A6, Th11;

      

       A23: ( Sum fb) = ( Sum fb9an) by A8, Th11;

      

       A24: ( len fa9b) = ( len fb9a) by A20, A21, FINSEQ_3: 29;

      then

       A25: ( len (fa9b + fb9a)) = ( len fa9b) by INTEGRA5: 2;

      then

       A26: ( Seg ln) = ( dom (fa9b + fb9a)) by A20, FINSEQ_3: 29;

      reconsider fa9b9 = fa9b as natural-valued ManySortedSet of ( Seg ln) by A20, PARTFUN1:def 2, RELAT_1:def 18;

      now

        thus ( Seg ln) = ( dom fab9) by FINSEQ_1:def 3;

        thus ( Seg ln) = ( dom (fa9b + fb9a)) by A20, A25, FINSEQ_3: 29;

        let k be Nat such that

         A27: k in ( Seg ln);

        reconsider k1 = k as Nat;

        reconsider fa9bk = (fa9b . k1), fb9ak = (fb9a . k1) as Real;

        

        thus (fab9 . k) = ((a + b) . (( SgmX (( RelIncl n),( support (a + b)))) . k)) by A4, A10, A19, A27, FUNCT_1: 13

        .= ((a . (( SgmX (( RelIncl n),( support (a + b)))) . k)) + (b . (( SgmX (( RelIncl n),( support (a + b)))) . k))) by PRE_POLY:def 5

        .= ((fa9b9 . k) + (b . (( SgmX (( RelIncl n),( support (a + b)))) . k))) by A10, A19, A27, FUNCT_1: 13

        .= (fa9bk + fb9ak) by A10, A19, A27, FUNCT_1: 13

        .= ((fa9b + fb9a) . k) by A26, A27, VALUED_1:def 1;

      end;

      then fab9 = (fa9b + fb9a) by FINSEQ_1: 13;

      hence thesis by A3, A5, A7, A22, A23, A24, INTEGRA5: 2;

    end;

    theorem :: BAGORDER:14

    for n be Ordinal, a,b be bag of n st b divides a holds ( TotDegree (a -' b)) = (( TotDegree a) - ( TotDegree b))

    proof

      let n be Ordinal, a,b be bag of n;

      assume b divides a;

      then

       A1: ((a -' b) + b) = a by PRE_POLY: 47;

      ( TotDegree ((a -' b) + b)) = (( TotDegree (a -' b)) + ( TotDegree b)) by Th12;

      hence thesis by A1;

    end;

    theorem :: BAGORDER:15

    

     Th14: for n be Ordinal, b be bag of n holds ( TotDegree b) = 0 iff b = ( EmptyBag n)

    proof

      let n be Ordinal, b be bag of n;

      

       A1: ( field ( RelIncl n)) = n by WELLORD2:def 1;

      ( RelIncl n) is being_linear-order by ORDERS_1: 19;

      then

       A2: ( RelIncl n) linearly_orders ( support b) by A1, ORDERS_1: 37, ORDERS_1: 38;

      

       A3: ( dom b) = n by PARTFUN1:def 2;

      hereby

        assume

         A4: ( TotDegree b) = 0 ;

        consider f be FinSequence of NAT such that

         A5: ( TotDegree b) = ( Sum f) and

         A6: f = (b * ( SgmX (( RelIncl n),( support b)))) by Def4;

        

         A7: f = (( len f) |-> 0 ) by A4, A5, Th3;

        now

          let z be object such that z in ( dom b) and

           A8: (b . z) <> 0 ;

          

           A9: ( rng ( SgmX (( RelIncl n),( support b)))) = ( support b) by A2, PRE_POLY:def 2;

          z in ( support b) by A8, PRE_POLY:def 7;

          then

          consider x be object such that

           A10: x in ( dom ( SgmX (( RelIncl n),( support b)))) and

           A11: (( SgmX (( RelIncl n),( support b))) . x) = z by A9, FUNCT_1:def 3;

          x in ( dom f) by A3, A6, A9, A10, RELAT_1: 27;

          then x in ( Seg ( len f)) by A7, FUNCOP_1: 13;

          then (f . x) = 0 by A7, FUNCOP_1: 7;

          hence contradiction by A6, A8, A10, A11, FUNCT_1: 13;

        end;

        then b = (n --> 0 ) by A3, FUNCOP_1: 11;

        hence b = ( EmptyBag n) by PBOOLE:def 3;

      end;

      assume b = ( EmptyBag n);

      then

       A12: b = (n --> 0 ) by PBOOLE:def 3;

      

       A13: ex f be FinSequence of NAT st (( TotDegree b) = ( Sum f)) & (f = (b * ( SgmX (( RelIncl n),( support b))))) by Def4;

      now

        assume ( support b) <> {} ;

        then

        consider x be object such that

         A14: x in ( support b) by XBOOLE_0:def 1;

        (b . x) = 0 by A12, A14, FUNCOP_1: 7;

        hence contradiction by A14, PRE_POLY:def 7;

      end;

      then ( rng ( SgmX (( RelIncl n),( support b)))) = {} by A2, PRE_POLY:def 2;

      then ( dom ( SgmX (( RelIncl n),( support b)))) = {} by RELAT_1: 42;

      then ( dom (b * ( SgmX (( RelIncl n),( support b))))) = {} by RELAT_1: 25, XBOOLE_1: 3;

      hence thesis by A13, RELAT_1: 41, RVSUM_1: 72;

    end;

    theorem :: BAGORDER:16

    

     Th15: for i,j,n be Nat holds ((i,j) -cut ( EmptyBag n)) = ( EmptyBag (j -' i))

    proof

      let i,j,n be Nat;

      set CUT1 = ((i,j) -cut ( EmptyBag n));

      

       A1: ( dom CUT1) = (j -' i) by PARTFUN1:def 2;

      now

        let k be object;

        per cases ;

          suppose

           A2: k in ( dom CUT1);

          (j -' i) = { x where x be Nat : x < (j -' i) } by AXIOMS: 4;

          then ex x be Nat st (k = x) & (x < (j -' i)) by A1, A2;

          then

          reconsider k9 = k as Element of NAT by ORDINAL1:def 12;

          (CUT1 . k) = (( EmptyBag n) . (i + k9)) by A2, Def1

          .= 0 by PBOOLE: 5;

          hence (CUT1 . k) <= (( EmptyBag (j -' i)) . k);

        end;

          suppose not k in ( dom CUT1);

          hence (CUT1 . k) <= (( EmptyBag (j -' i)) . k) by FUNCT_1:def 2;

        end;

      end;

      then CUT1 divides ( EmptyBag (j -' i)) by PRE_POLY:def 11;

      hence thesis by PRE_POLY: 58;

    end;

    theorem :: BAGORDER:17

    

     Th16: for i,j,n be Nat, a,b be bag of n holds ((i,j) -cut (a + b)) = (((i,j) -cut a) + ((i,j) -cut b))

    proof

      let i,j,n be Nat, a,b be bag of n;

      set CUTAB = ((i,j) -cut (a + b)), CUTA = ((i,j) -cut a), CUTB = ((i,j) -cut b);

      now

        let x be object such that

         A1: x in (j -' i);

        (j -' i) = { k where k be Nat : k < (j -' i) } by AXIOMS: 4;

        then ex k be Nat st (k = x) & (k < (j -' i)) by A1;

        then

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

        (CUTAB . x) = ((a + b) . (i + x9)) by A1, Def1;

        then

         A2: (CUTAB . x) = ((a . (i + x9)) + (b . (i + x9))) by PRE_POLY:def 5;

        

         A3: (CUTA . x) = (a . (i + x9)) by A1, Def1;

        (CUTB . x) = (b . (i + x9)) by A1, Def1;

        hence (CUTAB . x) = ((CUTA + CUTB) . x) by A2, A3, PRE_POLY:def 5;

      end;

      hence thesis by PBOOLE: 3;

    end;

    ::$Canceled

    theorem :: BAGORDER:20

    

     Th17: for n,m be Ordinal, b be bag of n st m in n holds (b | m) is bag of m

    proof

      let n,m be Ordinal, b be bag of n;

      assume m in n;

      then

       A1: m c= n by ORDINAL1:def 2;

      ( dom b) = n by PARTFUN1:def 2;

      then ( dom (b | m)) = m by A1, RELAT_1: 62;

      hence thesis by PARTFUN1:def 2;

    end;

    theorem :: BAGORDER:21

    for n be set, a,b be bag of n st b divides a holds ( support b) c= ( support a)

    proof

      let n be set, a,b be bag of n such that

       A1: b divides a;

      let x be object;

      assume x in ( support b);

      then (b . x) <> 0 by PRE_POLY:def 7;

      then (a . x) <> 0 by A1, PRE_POLY:def 11;

      hence thesis by PRE_POLY:def 7;

    end;

    begin

    definition

      let n be set;

      mode TermOrder of n is Order of ( Bags n);

    end

    notation

      let n be Ordinal;

      synonym LexOrder n for BagOrder n;

    end

    definition

      let n be Ordinal, T be TermOrder of n;

      :: BAGORDER:def5

      attr T is admissible means

      : Def5: T is_strongly_connected_in ( Bags n) & (for a be bag of n holds [( EmptyBag n), a] in T) & for a,b,c be bag of n st [a, b] in T holds [(a + c), (b + c)] in T;

    end

    theorem :: BAGORDER:22

    

     Th19: for n be Ordinal holds ( LexOrder n) is admissible

    proof

      let n be Ordinal;

      now

        let a,b be object such that

         A1: a in ( Bags n) and

         A2: b in ( Bags n);

        reconsider a9 = a, b9 = b as bag of n by A1, A2;

        a9 <=' b9 or b9 <=' a9 by PRE_POLY: 45;

        hence [a, b] in ( BagOrder n) or [b, a] in ( BagOrder n) by PRE_POLY:def 14;

      end;

      hence ( LexOrder n) is_strongly_connected_in ( Bags n);

      now

        let a be bag of n;

        ( EmptyBag n) <=' a by PRE_POLY: 60;

        hence [( EmptyBag n), a] in ( BagOrder n) by PRE_POLY:def 14;

      end;

      hence for a be bag of n holds [( EmptyBag n), a] in ( LexOrder n);

      now

        let a,b,c be bag of n;

        assume [a, b] in ( BagOrder n);

        then

         A3: a <=' b by PRE_POLY:def 14;

        now

          per cases by A3, PRE_POLY:def 10;

            suppose a < b;

            then

            consider k be Ordinal such that

             A4: (a . k) < (b . k) and

             A5: for l be Ordinal st l in k holds (a . l) = (b . l) by PRE_POLY:def 9;

            now

              take k;

              

               A6: ((a + c) . k) = ((a . k) + (c . k)) by PRE_POLY:def 5;

              ((b + c) . k) = ((b . k) + (c . k)) by PRE_POLY:def 5;

              hence ((a + c) . k) < ((b + c) . k) by A4, A6, XREAL_1: 6;

              let l be Ordinal such that

               A7: l in k;

              

               A8: ((a + c) . l) = ((a . l) + (c . l)) by PRE_POLY:def 5;

              ((b + c) . l) = ((b . l) + (c . l)) by PRE_POLY:def 5;

              hence ((a + c) . l) = ((b + c) . l) by A5, A7, A8;

            end;

            then (a + c) < (b + c) by PRE_POLY:def 9;

            hence (a + c) <=' (b + c) by PRE_POLY:def 10;

          end;

            suppose a = b;

            hence (a + c) <=' (b + c);

          end;

        end;

        hence [(a + c), (b + c)] in ( BagOrder n) by PRE_POLY:def 14;

      end;

      hence thesis;

    end;

    registration

      let n be Ordinal;

      cluster ( LexOrder n) -> admissible;

      coherence by Th19;

    end

    registration

      let n be Ordinal;

      cluster admissible for TermOrder of n;

      existence

      proof

        ( LexOrder n) is admissible;

        hence thesis;

      end;

    end

    theorem :: BAGORDER:23

    for o be infinite Ordinal holds ( LexOrder o) is non well-ordering

    proof

      let o be infinite Ordinal;

      set R = ( LexOrder o);

      set r = RelStr (# ( Bags o), R #);

      set ir = the InternalRel of r, cr = the carrier of r;

      assume R is well-ordering;

      then

       A1: R is well_founded;

      cr = ( field ir) by ORDERS_1: 15;

      then ir is_well_founded_in cr by A1, WELLORD1: 3;

      then

       A2: r is well_founded;

      defpred P[ set, set] means $2 = ((o --> 0 ) +* ($1,1));

       A3:

      now

        let n be Element of NAT ;

        set y = ((o --> 0 ) +* (n,1));

        

         A4: ( dom (o --> 0 )) = o by FUNCOP_1: 13;

        reconsider y as ManySortedSet of o;

        

         A5: omega c= o by CARD_3: 85;

        now

          let x be object;

          hereby

            assume x in {n};

            then x = n by TARSKI:def 1;

            hence (y . x) <> 0 by A4, A5, FUNCT_7: 31;

          end;

          assume that

           A6: (y . x) <> 0 and

           A7: not x in {n};

          x <> n by A7, TARSKI:def 1;

          then

           A8: (y . x) = ((o --> 0 ) . x) by FUNCT_7: 32;

          per cases ;

            suppose x in ( dom (o --> 0 ));

            hence contradiction by A6, A8, FUNCOP_1: 7;

          end;

            suppose not x in ( dom (o --> 0 ));

            hence contradiction by A6, A8, FUNCT_1:def 2;

          end;

        end;

        then ( support y) = {n} by PRE_POLY:def 7;

        then y is finite-support by PRE_POLY:def 8;

        then

        reconsider y as Element of cr by PRE_POLY:def 12;

        take y;

        thus P[n, y];

      end;

      consider f be sequence of cr such that

       A9: for n be Element of NAT holds P[n, (f . n)] from FUNCT_2:sch 3( A3);

      reconsider f as sequence of r;

      f is descending

      proof

        let n be Nat;

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

        set fn1 = (f . (n0 + 1)), fn = (f . n0);

        

         A10: fn1 = ((o --> 0 ) +* ((n + 1),1)) by A9;

        

         A11: fn = ((o --> 0 ) +* (n,1)) by A9;

        reconsider fn1 as bag of o;

        reconsider fn as bag of o;

        

         A12: n0 in omega ;

        

         A13: omega c= o by CARD_3: 85;

        n <> (n + 1);

        

        then

         A14: (fn1 . n) = ((o --> 0 ) . n) by A10, FUNCT_7: 32

        .= 0 by A12, A13, FUNCOP_1: 7;

        

         A15: ( dom (o --> 0 )) = o by FUNCOP_1: 13;

        then

         A16: (fn . n) = 1 by A11, A13, FUNCT_7: 31;

        now

          let l be Ordinal;

          assume

           A17: l in n;

          then

           A18: l <> n;

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

          then n in { i where i be Nat : i < (n0 + 1) };

          then n in (n + 1) by AXIOMS: 4;

          then n c= (n + 1) by ORDINAL1:def 2;

          then l in (n + 1) by A17;

          then l <> (n + 1);

          

          hence (fn1 . l) = ((o --> 0 ) . l) by A10, FUNCT_7: 32

          .= (fn . l) by A11, A18, FUNCT_7: 32;

        end;

        then

         A19: fn1 < fn by A14, A16, PRE_POLY:def 9;

        thus (f . (n + 1)) <> (f . n) by A11, A13, A14, A15, FUNCT_7: 31;

        fn1 <=' fn by A19, PRE_POLY:def 10;

        hence [(f . (n + 1)), (f . n)] in ir by PRE_POLY:def 14;

      end;

      hence contradiction by A2, WELLFND1: 14;

    end;

    definition

      let n be Ordinal;

      :: BAGORDER:def6

      func InvLexOrder n -> TermOrder of n means

      : Def6: for p,q be bag of n holds [p, q] in it iff p = q or ex i be Ordinal st i in n & (p . i) < (q . i) & for k be Ordinal st i in k & k in n holds (p . k) = (q . k);

      existence

      proof

        defpred P[ object, object] means ($1 = $2 or ex p,q be Element of ( Bags n) st $1 = p & $2 = q & ex i be Ordinal st i in n & (p . i) < (q . i) & for k be Ordinal st i in k & k in n holds (p . k) = (q . k));

        consider ILO be Relation of ( Bags n), ( Bags n) such that

         A1: for x,y be object holds [x, y] in ILO iff x in ( Bags n) & y in ( Bags n) & P[x, y] from RELSET_1:sch 1;

        

         A2: ILO is_reflexive_in ( Bags n) by A1;

        

         A3: ILO is_antisymmetric_in ( Bags n)

        proof

          let x,y be object;

          assume that x in ( Bags n) and y in ( Bags n) and

           A4: [x, y] in ILO and

           A5: [y, x] in ILO;

          per cases ;

            suppose x = y;

            hence thesis;

          end;

            suppose

             A6: not x = y;

            then

            consider p,q be Element of ( Bags n) such that

             A7: x = p and

             A8: y = q and

             A9: ex i be Ordinal st i in n & (p . i) < (q . i) & for k be Ordinal st i in k & k in n holds (p . k) = (q . k) by A1, A4;

            ex q9,p9 be Element of ( Bags n) st (y = q9) & (x = p9) & (ex i be Ordinal st i in n & (q9 . i) < (p9 . i) & for k be Ordinal st i in k & k in n holds (q9 . k) = (p9 . k)) by A1, A5, A6;

            then

            consider i be Ordinal such that

             A10: i in n and

             A11: (q . i) < (p . i) and

             A12: for k be Ordinal st i in k & k in n holds (q . k) = (p . k) by A7, A8;

            consider j be Ordinal such that

             A13: j in n and

             A14: (p . j) < (q . j) and

             A15: for k be Ordinal st j in k & k in n holds (p . k) = (q . k) by A9;

            now

              per cases by ORDINAL1: 14;

                suppose i in j;

                hence i = j by A12, A13, A14;

              end;

                suppose i = j;

                hence i = j;

              end;

                suppose j in i;

                hence i = j by A10, A11, A15;

              end;

            end;

            hence thesis by A11, A14;

          end;

        end;

        

         A16: ILO is_transitive_in ( Bags n)

        proof

          let x,y,z be object such that x in ( Bags n) and y in ( Bags n) and z in ( Bags n) and

           A17: [x, y] in ILO and

           A18: [y, z] in ILO;

          per cases ;

            suppose x = y;

            hence thesis by A18;

          end;

            suppose x <> y;

            then

            consider p,q be Element of ( Bags n) such that

             A19: x = p and

             A20: y = q and

             A21: ex i be Ordinal st i in n & (p . i) < (q . i) & for k be Ordinal st i in k & k in n holds (p . k) = (q . k) by A1, A17;

            consider i be Ordinal such that

             A22: i in n and

             A23: (p . i) < (q . i) and

             A24: for k be Ordinal st i in k & k in n holds (p . k) = (q . k) by A21;

            now

              per cases ;

                suppose y = z;

                hence thesis by A17;

              end;

                suppose y <> z;

                then

                consider q9,r be Element of ( Bags n) such that

                 A25: y = q9 and

                 A26: z = r and

                 A27: ex i be Ordinal st i in n & (q9 . i) < (r . i) & for k be Ordinal st i in k & k in n holds (q9 . k) = (r . k) by A1, A18;

                consider j be Ordinal such that

                 A28: j in n and

                 A29: (q9 . j) < (r . j) and

                 A30: for k be Ordinal st j in k & k in n holds (q9 . k) = (r . k) by A27;

                now

                  per cases by ORDINAL1: 14;

                    suppose

                     A31: i in j;

                    then

                     A32: (p . j) < (r . j) by A20, A24, A25, A28, A29;

                    now

                      let k be Ordinal such that

                       A33: j in k and

                       A34: k in n;

                      

                       A35: (q . k) = (r . k) by A20, A25, A30, A33, A34;

                      i in k by A31, A33, ORDINAL1: 10;

                      hence (p . k) = (r . k) by A24, A34, A35;

                    end;

                    hence thesis by A1, A19, A26, A28, A32;

                  end;

                    suppose

                     A36: i = j;

                    now

                      take p, r;

                      thus x = p & z = r by A19, A26;

                      take j;

                      thus j in n by A28;

                      thus (p . j) < (r . j) by A20, A23, A25, A29, A36, XXREAL_0: 2;

                      now

                        let k be Ordinal such that

                         A37: j in k and

                         A38: k in n;

                        (p . k) = (q . k) by A24, A36, A37, A38;

                        hence (p . k) = (r . k) by A20, A25, A30, A37, A38;

                      end;

                      hence for k be Ordinal st j in k & k in n holds (p . k) = (r . k);

                    end;

                    hence thesis by A1;

                  end;

                    suppose

                     A39: j in i;

                    then

                     A40: (p . i) < (r . i) by A20, A22, A23, A25, A30;

                    now

                      let k be Ordinal such that

                       A41: i in k and

                       A42: k in n;

                      

                       A43: (p . k) = (q . k) by A24, A41, A42;

                      j in k by A39, A41, ORDINAL1: 10;

                      hence (p . k) = (r . k) by A20, A25, A30, A42, A43;

                    end;

                    hence thesis by A1, A19, A22, A26, A40;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        

         A44: ( dom ILO) = ( Bags n) by A2, ORDERS_1: 13;

        ( field ILO) = ( Bags n) by A2, ORDERS_1: 13;

        then

        reconsider ILO as TermOrder of n by A2, A3, A16, A44, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

        take ILO;

        let x,y be bag of n;

        hereby

          assume

           A45: [x, y] in ILO;

          now

            assume x <> y;

            then ex p,q be Element of ( Bags n) st (x = p) & (y = q) & (ex i be Ordinal st i in n & (p . i) < (q . i) & for k be Ordinal st i in k & k in n holds (p . k) = (q . k)) by A1, A45;

            hence ex i be Ordinal st i in n & (x . i) < (y . i) & for k be Ordinal st i in k & k in n holds (x . k) = (y . k);

          end;

          hence x = y or ex i be Ordinal st i in n & (x . i) < (y . i) & for k be Ordinal st i in k & k in n holds (x . k) = (y . k);

        end;

        assume

         A46: x = y or ex i be Ordinal st i in n & (x . i) < (y . i) & for k be Ordinal st i in k & k in n holds (x . k) = (y . k);

         A47:

        now

          assume

           A48: x <> y;

          thus ex p,q be Element of ( Bags n) st x = p & y = q & ex i be Ordinal st i in n & (p . i) < (q . i) & for k be Ordinal st i in k & k in n holds (p . k) = (q . k)

          proof

            reconsider x9 = x, y9 = y as Element of ( Bags n) by PRE_POLY:def 12;

            take x9, y9;

            thus x = x9 & y = y9;

            thus thesis by A46, A48;

          end;

        end;

        x in ( Bags n) by PRE_POLY:def 12;

        hence thesis by A1, A47;

      end;

      uniqueness

      proof

        let IT1,IT2 be TermOrder of n such that

         A49: for p,q be bag of n holds [p, q] in IT1 iff p = q or ex i be Ordinal st i in n & (p . i) < (q . i) & for k be Ordinal st i in k & k in n holds (p . k) = (q . k) and

         A50: for p,q be bag of n holds [p, q] in IT2 iff p = q or ex i be Ordinal st i in n & (p . i) < (q . i) & for k be Ordinal st i in k & k in n holds (p . k) = (q . k);

        now

          let a,b be object;

          hereby

            assume

             A51: [a, b] in IT1;

            then

            consider p,q be object such that

             A52: [a, b] = [p, q] and

             A53: p in ( Bags n) and

             A54: q in ( Bags n) by RELSET_1: 2;

            reconsider p, q as bag of n by A53, A54;

            per cases ;

              suppose p = q;

              hence [a, b] in IT2 by A50, A52;

            end;

              suppose p <> q;

              then ex i be Ordinal st i in n & (p . i) < (q . i) & for k be Ordinal st i in k & k in n holds (p . k) = (q . k) by A49, A51, A52;

              hence [a, b] in IT2 by A50, A52;

            end;

          end;

          assume

           A55: [a, b] in IT2;

          then

          consider p,q be object such that

           A56: [a, b] = [p, q] and

           A57: p in ( Bags n) and

           A58: q in ( Bags n) by RELSET_1: 2;

          reconsider p, q as bag of n by A57, A58;

          per cases ;

            suppose p = q;

            hence [a, b] in IT1 by A49, A56;

          end;

            suppose p <> q;

            then ex i be Ordinal st i in n & (p . i) < (q . i) & for k be Ordinal st i in k & k in n holds (p . k) = (q . k) by A50, A55, A56;

            hence [a, b] in IT1 by A49, A56;

          end;

        end;

        hence IT1 = IT2 by RELAT_1:def 2;

      end;

    end

    theorem :: BAGORDER:24

    

     Th21: for n be Ordinal holds ( InvLexOrder n) is admissible

    proof

      let n be Ordinal;

      set ILO = ( InvLexOrder n);

      now

        let x,y be object such that

         A1: x in ( Bags n) and

         A2: y in ( Bags n);

        reconsider p = x, q = y as bag of n by A1, A2;

        now

          assume

           A3: not [p, q] in ILO;

          then

           A4: p <> q by Def6;

          set s = ( SgmX (( RelIncl n),(( support p) \/ ( support q))));

          

           A5: ( dom p) = n by PARTFUN1:def 2;

          

           A6: ( dom q) = n by PARTFUN1:def 2;

          

           A7: ( field ( RelIncl n)) = n by WELLORD2:def 1;

          ( RelIncl n) is being_linear-order by ORDERS_1: 19;

          then

           A8: ( RelIncl n) linearly_orders (( support p) \/ ( support q)) by A7, ORDERS_1: 37, ORDERS_1: 38;

          then

           A9: ( rng s) = (( support p) \/ ( support q)) by PRE_POLY:def 2;

          defpred P[ Nat] means $1 in ( dom s) & (q . (s . $1)) <> (p . (s . $1));

          

           A10: for k be Nat st P[k] holds k <= ( len s) by FINSEQ_3: 25;

          

           A11: ex k be Nat st P[k]

          proof

            assume

             A12: not thesis;

            now

              let x be object;

              assume x in n;

              per cases ;

                suppose (p . x) <> 0 ;

                then x in ( support p) by PRE_POLY:def 7;

                then x in (( support p) \/ ( support q)) by XBOOLE_0:def 3;

                then ex k be Nat st (k in ( dom s)) & ((s . k) = x) by A9, FINSEQ_2: 10;

                hence (p . x) = (q . x) by A12;

              end;

                suppose (q . x) <> 0 ;

                then x in ( support q) by PRE_POLY:def 7;

                then x in (( support p) \/ ( support q)) by XBOOLE_0:def 3;

                then ex k be Nat st (k in ( dom s)) & ((s . k) = x) by A9, FINSEQ_2: 10;

                hence (p . x) = (q . x) by A12;

              end;

                suppose (p . x) = 0 & (q . x) = 0 ;

                hence (p . x) = (q . x);

              end;

            end;

            hence contradiction by A4, A5, A6, FUNCT_1: 2;

          end;

          consider j be Nat such that

           A13: P[j] and

           A14: for k be Nat st P[k] holds k <= j from NAT_1:sch 6( A10, A11);

          

           A15: (s . j) in ( rng s) by A13, FUNCT_1: 3;

          then

          reconsider J = (s . j) as Ordinal by A9;

          now

            take J;

            thus J in n by A9, A15;

             A16:

            now

              let k be Ordinal such that

               A17: J in k and

               A18: k in n and

               A19: (q . k) <> (p . k);

              now

                assume that

                 A20: not k in ( support p) and

                 A21: not k in ( support q);

                (p . k) = 0 by A20, PRE_POLY:def 7;

                hence contradiction by A19, A21, PRE_POLY:def 7;

              end;

              then k in (( support p) \/ ( support q)) by XBOOLE_0:def 3;

              then

              consider m be Nat such that

               A22: m in ( dom s) and

               A23: (s . m) = k by A9, FINSEQ_2: 10;

              

               A24: m <= j by A14, A19, A22, A23;

              m <> j by A17, A23;

              then m < j by A24, XXREAL_0: 1;

              then [(s /. m), (s /. j)] in ( RelIncl n) by A8, A13, A22, PRE_POLY:def 2;

              then [(s . m), (s /. j)] in ( RelIncl n) by A22, PARTFUN1:def 6;

              then [(s . m), (s . j)] in ( RelIncl n) by A13, PARTFUN1:def 6;

              then (s . m) c= (s . j) by A9, A15, A18, A23, WELLORD2:def 1;

              hence contradiction by A17, A23, ORDINAL1: 5;

            end;

            then (q . J) <= (p . J) by A3, A9, A15, Def6;

            hence (q . J) < (p . J) by A13, XXREAL_0: 1;

            thus for k be Ordinal st J in k & k in n holds (q . k) = (p . k) by A16;

          end;

          hence [q, p] in ILO by Def6;

        end;

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

      end;

      hence ILO is_strongly_connected_in ( Bags n);

      now

        let a be bag of n;

        per cases ;

          suppose ( EmptyBag n) = a;

          hence [( EmptyBag n), a] in ILO by Def6;

        end;

          suppose

           A25: ( EmptyBag n) <> a;

          set s = ( SgmX (( RelIncl n),( support a)));

          

           A26: ( field ( RelIncl n)) = n by WELLORD2:def 1;

          ( RelIncl n) is being_linear-order by ORDERS_1: 19;

          then

           A27: ( RelIncl n) linearly_orders ( support a) by A26, ORDERS_1: 37, ORDERS_1: 38;

          then

           A28: ( rng s) = ( support a) by PRE_POLY:def 2;

          then ( rng s) <> {} by A25, PRE_POLY: 81;

          then

           A29: ( len s) in ( dom s) by FINSEQ_5: 6, RELAT_1: 38;

          then

           A30: (s . ( len s)) in ( rng s) by FUNCT_1: 3;

          then

          reconsider j = (s . ( len s)) as Ordinal by A28;

          now

            take j;

            thus j in n by A28, A30;

            

             A31: (a . j) <> 0 by A28, A30, PRE_POLY:def 7;

            (( EmptyBag n) . j) = 0 by PBOOLE: 5;

            hence (( EmptyBag n) . j) < (a . j) by A31;

            let k be Ordinal such that

             A32: j in k and

             A33: k in n;

            

             A34: j c= k by A32, ORDINAL1:def 2;

            now

              assume (( EmptyBag n) . k) <> (a . k);

              then (a . k) <> 0 by PBOOLE: 5;

              then k in ( support a) by PRE_POLY:def 7;

              then

              consider i be Nat such that

               A35: i in ( dom s) and

               A36: (s . i) = k by A28, FINSEQ_2: 10;

              

               A37: i <= ( len s) by A35, FINSEQ_3: 25;

              per cases by A37, XXREAL_0: 1;

                suppose i = ( len s);

                hence contradiction by A32, A36;

              end;

                suppose i < ( len s);

                then [(s /. i), (s /. ( len s))] in ( RelIncl n) by A27, A29, A35, PRE_POLY:def 2;

                then [(s . i), (s /. ( len s))] in ( RelIncl n) by A35, PARTFUN1:def 6;

                then [(s . i), (s . ( len s))] in ( RelIncl n) by A29, PARTFUN1:def 6;

                then k c= j by A28, A30, A33, A36, WELLORD2:def 1;

                then j = k by A34, XBOOLE_0:def 10;

                hence contradiction by A32;

              end;

            end;

            hence (( EmptyBag n) . k) = (a . k);

          end;

          hence [( EmptyBag n), a] in ILO by Def6;

        end;

      end;

      hence for a be bag of n holds [( EmptyBag n), a] in ILO;

      now

        let a,b,c be bag of n such that

         A38: [a, b] in ILO;

        per cases ;

          suppose

           A39: a = b;

          (a + c) in ( Bags n) by PRE_POLY:def 12;

          hence [(a + c), (b + c)] in ILO by A39, ORDERS_1: 3;

        end;

          suppose a <> b;

          then

          consider i be Ordinal such that

           A40: i in n and

           A41: (a . i) < (b . i) and

           A42: for k be Ordinal st i in k & k in n holds (a . k) = (b . k) by A38, Def6;

          now

            take i;

            thus i in n by A40;

            

             A43: ((a + c) . i) = ((a . i) + (c . i)) by PRE_POLY:def 5;

            ((b + c) . i) = ((b . i) + (c . i)) by PRE_POLY:def 5;

            hence ((a + c) . i) < ((b + c) . i) by A41, A43, XREAL_1: 6;

            let k be Ordinal such that

             A44: i in k and

             A45: k in n;

            

             A46: ((a + c) . k) = ((a . k) + (c . k)) by PRE_POLY:def 5;

            ((b + c) . k) = ((b . k) + (c . k)) by PRE_POLY:def 5;

            hence ((a + c) . k) = ((b + c) . k) by A42, A44, A45, A46;

          end;

          hence [(a + c), (b + c)] in ILO by Def6;

        end;

      end;

      hence thesis;

    end;

    registration

      let n be Ordinal;

      cluster ( InvLexOrder n) -> admissible;

      coherence by Th21;

    end

    theorem :: BAGORDER:25

    

     Th22: for o be Ordinal holds ( InvLexOrder o) is well-ordering

    proof

      defpred P[ Ordinal] means ( InvLexOrder $1) is well-ordering;

       A1:

      now

        let o be Ordinal such that

         A2: for n be Ordinal st n in o holds P[n];

        set ilo = ( InvLexOrder o);

        

         A3: ilo is_strongly_connected_in ( Bags o) by Def5;

        then ilo is_reflexive_in ( Bags o);

        then

         A4: ( field ilo) = ( Bags o) by PARTIT_2: 9;

         A5:

        now

          assume ilo is non well_founded;

          then

           A6: not ilo is_well_founded_in ( Bags o) by A4, WELLORD1: 3;

          set R = RelStr (# ( Bags o), ilo #);

          set ir = the InternalRel of R;

          R is non well_founded by A6;

          then

          consider f be sequence of R such that

           A7: f is descending by WELLFND1: 14;

          reconsider a = (f . 0 ) as bag of o;

          set s = ( SgmX (( RelIncl o),( support a)));

          

           A8: ( field ( RelIncl o)) = o by WELLORD2:def 1;

          ( RelIncl o) is being_linear-order by ORDERS_1: 19;

          then

           A9: ( RelIncl o) linearly_orders ( support a) by A8, ORDERS_1: 37, ORDERS_1: 38;

          then

           A10: ( rng s) = ( support a) by PRE_POLY:def 2;

          now

            assume ( rng s) = {} ;

            then

             A11: a = ( EmptyBag o) by A10, PRE_POLY: 81;

            reconsider b = (f . ( 0 qua Nat + 1)) as bag of o;

            

             A12: b <> a by A7;

             [b, a] in ir by A7;

            then ex i be Ordinal st (i in o) & ((b . i) < (a . i)) & (for k be Ordinal st i in k & k in o holds (b . k) = (a . k)) by A12, Def6;

            hence contradiction by A11, PBOOLE: 5;

          end;

          then

           A13: ( len s) in ( dom s) by FINSEQ_5: 6, RELAT_1: 38;

          then

           A14: (s . ( len s)) in ( rng s) by FUNCT_1: 3;

          then

          reconsider j = (s . ( len s)) as Ordinal by A10;

          defpred P[ set, set] means ex b be bag of o st (f . $1) = b & $2 = (b . j);

           A15:

          now

            let x be Element of NAT ;

            reconsider b = (f . x) as bag of o;

            take y = (b . j);

            thus P[x, y];

          end;

          consider t be sequence of NAT such that

           A16: for i be Element of NAT holds P[i, (t . i)] from FUNCT_2:sch 3( A15);

          defpred P[ Nat] means for i be Ordinal, b be bag of o st j in i & i in o & (f . $1) = b holds (b . i) = 0 ;

          

           A17: P[ 0 ]

          proof

            let i be Ordinal, b be bag of o such that

             A18: j in i and

             A19: i in o and

             A20: (f . 0 ) = b;

            assume (b . i) <> 0 ;

            then i in ( support a) by A20, PRE_POLY:def 7;

            then

            consider k be Nat such that

             A21: k in ( dom s) and

             A22: (s . k) = i by A10, FINSEQ_2: 10;

            

             A23: k <= ( len s) by A21, FINSEQ_3: 25;

            per cases by A23, XXREAL_0: 1;

              suppose k = ( len s);

              hence contradiction by A18, A22;

            end;

              suppose k < ( len s);

              then [(s /. k), (s /. ( len s))] in ( RelIncl o) by A9, A13, A21, PRE_POLY:def 2;

              then [(s . k), (s /. ( len s))] in ( RelIncl o) by A21, PARTFUN1:def 6;

              then [(s . k), (s . ( len s))] in ( RelIncl o) by A13, PARTFUN1:def 6;

              then (s . k) c= (s . ( len s)) by A10, A14, A19, A22, WELLORD2:def 1;

              hence contradiction by A18, A22, ORDINAL1: 5;

            end;

          end;

          

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

          proof

            let n be Nat;

            assume

             A25: for i be Ordinal, b be bag of o st j in i & i in o & (f . n) = b holds (b . i) = 0 ;

            let i be Ordinal, b1 be bag of o such that

             A26: j in i and

             A27: i in o and

             A28: (f . (n + 1)) = b1;

            reconsider b = (f . n) as bag of o;

            

             A29: (b . i) = 0 by A25, A26, A27;

            

             A30: b1 <> b by A7, A28;

             [b1, b] in ilo by A7, A28;

            then

            consider i1 be Ordinal such that

             A31: i1 in o and

             A32: (b1 . i1) < (b . i1) and

             A33: for k be Ordinal st i1 in k & k in o holds (b1 . k) = (b . k) by A30, Def6;

            per cases by ORDINAL1: 14;

              suppose i1 in i;

              hence thesis by A27, A29, A33;

            end;

              suppose i1 = i;

              hence thesis by A25, A26, A27, A32;

            end;

              suppose

               A34: i in i1;

              assume (b1 . i) <> 0 ;

              j in i1 by A26, A34, ORDINAL1: 10;

              hence contradiction by A25, A31, A32;

            end;

          end;

          

           A35: for n be Nat holds P[n] from NAT_1:sch 2( A17, A24);

          reconsider t as sequence of OrderedNAT by DICKSON:def 15;

          

           A36: t is non-increasing

          proof

            let n be Nat;

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

            reconsider tn = (t . n0), tn1 = (t . (n0 + 1)) as Nat;

            reconsider fn = (f . n0), fn1 = (f . (n0 + 1)) as bag of o;

            

             A37: fn1 <> fn by A7;

             [fn1, fn] in ilo by A7;

            then

            consider i be Ordinal such that

             A38: i in o and

             A39: (fn1 . i) < (fn . i) and

             A40: for k be Ordinal st i in k & k in o holds (fn1 . k) = (fn . k) by A37, Def6;

            

             A41: ex bn be bag of o st (fn = bn) & (tn = (bn . j)) by A16;

            

             A42: ex bn1 be bag of o st (fn1 = bn1) & (tn1 = (bn1 . j)) by A16;

            now

              per cases by ORDINAL1: 14;

                suppose i = j;

                hence tn1 <= tn by A39, A41, A42;

              end;

                suppose j in i;

                hence tn1 <= tn by A35, A38, A39;

              end;

                suppose i in j;

                hence tn1 <= tn by A10, A14, A40, A41, A42;

              end;

            end;

            hence thesis by DICKSON:def 14, DICKSON:def 15;

          end;

          set n = j;

          set iln = ( InvLexOrder n);

          set S = RelStr (# ( Bags n), iln #);

          iln is_strongly_connected_in ( Bags n) by Def5;

          then iln is_reflexive_in ( Bags n);

          then

           A43: ( field iln) = ( Bags n) by PARTIT_2: 9;

          consider p be Nat such that

           A44: for r be Nat st p <= r holds (t . p) = (t . r) by A36, Th9;

          defpred P[ Nat, set] means ex b be bag of o st b = (f . (p + $1)) & $2 = (b | j);

           A45:

          now

            let x be Element of NAT ;

            reconsider b = (f . (p + x)) as bag of o;

            reconsider y = (b | j) as bag of n by A10, A14, Th17;

            reconsider y as Element of ( Bags n) by PRE_POLY:def 12;

            take y;

            thus P[x, y];

          end;

          consider g be sequence of ( Bags n) such that

           A46: for x be Element of NAT holds P[x, (g . x)] from FUNCT_2:sch 3( A45);

          reconsider g as sequence of S;

          now

            let k be Nat;

            reconsider k0 = k as Element of NAT by ORDINAL1:def 12;

            consider b be bag of o such that

             A47: b = (f . (p + k)) and

             A48: (g . k0) = (b | j) by A46;

            consider b1 be bag of o such that

             A49: b1 = (f . (p + (k + 1))) and

             A50: (g . (k + 1)) = (b1 | j) by A46;

            (p + (k + 1)) = ((p + k) + 1);

            then

             A51: b <> b1 by A7, A47, A49;

            

             A52: ex bb be bag of o st ((f . (p + k)) = bb) & ((t . (p + k0)) = (bb . j)) by A16;

            

             A53: ex bb1 be bag of o st ((f . (p + (k + 1))) = bb1) & ((t . (p + (k + 1))) = (bb1 . j)) by A16;

            

             A54: (t . (p + k)) = (t . p) by A44, NAT_1: 11;

            thus (g . (k + 1)) <> (g . k)

            proof

              assume

               A55: not thesis;

              

               A56: o = ( dom b) by PARTFUN1:def 2;

              

               A57: o = ( dom b1) by PARTFUN1:def 2;

              now

                let m be object such that

                 A58: m in o;

                reconsider mm = m as set by TARSKI: 1;

                per cases by A58, ORDINAL1: 14;

                  suppose

                   A59: m in j;

                  then ((b | j) . m) = (b . m) by FUNCT_1: 49;

                  hence (b . m) = (b1 . m) by A48, A50, A55, A59, FUNCT_1: 49;

                end;

                  suppose m = j;

                  hence (b . m) = (b1 . m) by A44, A47, A49, A52, A53, A54, NAT_1: 11;

                end;

                  suppose

                   A60: j in mm;

                  then (b . m) = 0 by A35, A47, A58;

                  hence (b . m) = (b1 . m) by A35, A49, A58, A60;

                end;

              end;

              hence contradiction by A51, A56, A57, FUNCT_1: 2;

            end;

             [(f . ((p + k) + 1)), (f . (p + k))] in ilo by A7;

            then

            consider i be Ordinal such that

             A61: i in o and

             A62: (b1 . i) < (b . i) and

             A63: for k be Ordinal st i in k & k in o holds (b . k) = (b1 . k) by A47, A49, A51, Def6;

             A64:

            now

              assume

               A65: not i in j;

              per cases by A65, ORDINAL1: 14;

                suppose i = j;

                hence contradiction by A44, A47, A49, A52, A53, A54, A62, NAT_1: 11;

              end;

                suppose

                 A66: j in i;

                

                then (b . i) = 0 by A35, A47, A61

                .= (b1 . i) by A35, A49, A61, A66;

                hence contradiction by A62;

              end;

            end;

            reconsider bj = (b | j), b1j = (b1 | j) as bag of n by A10, A14, Th17;

            

             A67: (b1j . i) = (b1 . i) by A64, FUNCT_1: 49;

            

             A68: (bj . i) = (b . i) by A64, FUNCT_1: 49;

            now

              let k be Ordinal such that

               A69: i in k and

               A70: k in n;

              k in o by A10, A14, A70, ORDINAL1: 10;

              then

               A71: (b . k) = (b1 . k) by A63, A69;

              

              thus (bj . k) = (b . k) by A70, FUNCT_1: 49

              .= (b1j . k) by A70, A71, FUNCT_1: 49;

            end;

            hence [(g . (k + 1)), (g . k)] in iln by A48, A50, A62, A64, A67, A68, Def6;

          end;

          then g is descending;

          then S is non well_founded by WELLFND1: 14;

          then not iln is_well_founded_in the carrier of S;

          then not iln well_orders ( field iln) by A43, WELLORD1:def 5;

          then iln is non well-ordering by WELLORD1: 4;

          hence contradiction by A2, A10, A14;

        end;

        

         A72: ( field ilo) = ( Bags o) by ORDERS_1: 12;

        then

         A73: ilo is_reflexive_in ( Bags o) by RELAT_2:def 9;

        

         A74: ilo is_transitive_in ( Bags o) by A72, RELAT_2:def 16;

        

         A75: ilo is_antisymmetric_in ( Bags o) by A72, RELAT_2:def 12;

        

         A76: ilo is_connected_in ( field ilo) by A3, A4;

        ilo is_well_founded_in ( field ilo) by A5, WELLORD1: 3;

        then ilo well_orders ( field ilo) by A4, A73, A74, A75, A76, WELLORD1:def 5;

        hence P[o] by WELLORD1: 4;

      end;

      thus for o be Ordinal holds P[o] from ORDINAL1:sch 2( A1);

    end;

    definition

      let n be Ordinal, o be TermOrder of n;

      :: BAGORDER:def7

      func Graded o -> TermOrder of n means

      : Def7: for a,b be bag of n holds [a, b] in it iff (( TotDegree a) < ( TotDegree b) or ( TotDegree a) = ( TotDegree b) & [a, b] in o);

      existence

      proof

        defpred P[ object, object] means (ex x9,y9 be bag of n st x9 = $1 & y9 = $2 & ((( TotDegree x9) < ( TotDegree y9)) or (( TotDegree x9) = ( TotDegree y9) & [x9, y9] in o)));

        consider R be Relation of ( Bags n) such that

         A2: for x,y be object holds [x, y] in R iff x in ( Bags n) & y in ( Bags n) & P[x, y] from RELSET_1:sch 1;

         A3:

        now

          let x be object such that

           A4: x in ( Bags n);

          reconsider x9 = x as bag of n by A4;

          now

            take x9;

            thus x9 = x;

            thus ( TotDegree x9) = ( TotDegree x9);

             [( EmptyBag n), ( EmptyBag n)] in o by ORDERS_1: 3;

            then [(( EmptyBag n) + x9), (( EmptyBag n) + x9)] in o by A1;

            then [x9, (( EmptyBag n) + x9)] in o by PRE_POLY: 53;

            hence [x9, x9] in o by PRE_POLY: 53;

          end;

          hence [x, x] in R by A2, A4;

        end;

         A5:

        now

          let x,y be object such that

           A6: x in ( Bags n) and

           A7: y in ( Bags n) and

           A8: [x, y] in R and

           A9: [y, x] in R;

          consider x9,y9 be bag of n such that

           A10: x9 = x and

           A11: y9 = y and

           A12: ( TotDegree x9) < ( TotDegree y9) or ( TotDegree x9) = ( TotDegree y9) & [x9, y9] in o by A2, A8;

          

           A13: ex y99,x99 be bag of n st (y99 = y) & (x99 = x) & (( TotDegree y99) < ( TotDegree x99) or ( TotDegree y99) = ( TotDegree x99) & [y99, x99] in o) by A2, A9;

          now

            per cases by A12;

              suppose

               A14: ( TotDegree x9) < ( TotDegree y9);

              now

                per cases by A10, A11, A13;

                  suppose ( TotDegree y9) < ( TotDegree x9);

                  hence contradiction by A14;

                end;

                  suppose ( TotDegree y9) = ( TotDegree x9) & [y9, x9] in o;

                  hence contradiction by A14;

                end;

              end;

              hence ( TotDegree x9) = ( TotDegree y9) & [x9, y9] in o & ( TotDegree y9) = ( TotDegree x9) & [y9, x9] in o;

            end;

              suppose

               A15: ( TotDegree x9) = ( TotDegree y9) & [x9, y9] in o;

              now

                per cases by A10, A11, A13;

                  suppose ( TotDegree y9) < ( TotDegree x9);

                  hence ( TotDegree x9) = ( TotDegree y9) & [x9, y9] in o & ( TotDegree y9) = ( TotDegree x9) & [y9, x9] in o by A15;

                end;

                  suppose ( TotDegree y9) = ( TotDegree x9) & [y9, x9] in o;

                  hence ( TotDegree x9) = ( TotDegree y9) & [x9, y9] in o & ( TotDegree y9) = ( TotDegree x9) & [y9, x9] in o by A15;

                end;

              end;

              hence ( TotDegree x9) = ( TotDegree y9) & [x9, y9] in o & ( TotDegree y9) = ( TotDegree x9) & [y9, x9] in o;

            end;

          end;

          hence x = y by A6, A7, A10, A11, ORDERS_1: 4;

        end;

         A16:

        now

          let x,y,z be object such that

           A17: x in ( Bags n) and

           A18: y in ( Bags n) and

           A19: z in ( Bags n) and

           A20: [x, y] in R and

           A21: [y, z] in R;

          consider x9,y9 be bag of n such that

           A22: x9 = x and

           A23: y9 = y and

           A24: ( TotDegree x9) < ( TotDegree y9) or ( TotDegree x9) = ( TotDegree y9) & [x9, y9] in o by A2, A20;

          consider y99,z9 be bag of n such that

           A25: y99 = y and

           A26: z9 = z and

           A27: ( TotDegree y99) < ( TotDegree z9) or ( TotDegree y99) = ( TotDegree z9) & [y99, z9] in o by A2, A21;

          per cases by A24;

            suppose

             A28: ( TotDegree x9) < ( TotDegree y9);

            now

              per cases by A23, A25, A27;

                suppose ( TotDegree y9) < ( TotDegree z9);

                then ( TotDegree x9) < ( TotDegree z9) by A28, XXREAL_0: 2;

                hence [x, z] in R by A2, A17, A19, A22, A26;

              end;

                suppose ( TotDegree y9) = ( TotDegree z9) & [y9, z9] in o;

                hence [x, z] in R by A2, A17, A19, A22, A26, A28;

              end;

            end;

            hence [x, z] in R;

          end;

            suppose

             A29: ( TotDegree x9) = ( TotDegree y9) & [x9, y9] in o;

            now

              per cases by A23, A25, A27;

                suppose ( TotDegree y9) < ( TotDegree z9);

                hence [x, z] in R by A2, A17, A19, A22, A26, A29;

              end;

                suppose ( TotDegree y9) = ( TotDegree z9) & [y9, z9] in o;

                then [x9, z9] in o by A17, A18, A19, A22, A23, A26, A29, ORDERS_1: 5;

                hence [x, z] in R by A2, A17, A19, A22, A23, A25, A26, A27, A29;

              end;

            end;

            hence [x, z] in R;

          end;

        end;

        

         A30: R is_reflexive_in ( Bags n) by A3;

        

         A31: R is_antisymmetric_in ( Bags n) by A5;

        

         A32: R is_transitive_in ( Bags n) by A16;

        

         A33: ( dom R) = ( Bags n) by A30, ORDERS_1: 13;

        ( field R) = ( Bags n) by A30, ORDERS_1: 13;

        then

        reconsider R as TermOrder of n by A30, A31, A32, A33, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

        take R;

        let a,b be bag of n;

        hereby

          assume [a, b] in R;

          then ex x9,y9 be bag of n st (x9 = a) & (y9 = b) & (( TotDegree x9) < ( TotDegree y9) or ( TotDegree x9) = ( TotDegree y9) & [x9, y9] in o) by A2;

          hence ( TotDegree a) < ( TotDegree b) or ( TotDegree a) = ( TotDegree b) & [a, b] in o;

        end;

        assume

         A34: ( TotDegree a) < ( TotDegree b) or ( TotDegree a) = ( TotDegree b) & [a, b] in o;

        

         A35: a in ( Bags n) by PRE_POLY:def 12;

        b in ( Bags n) by PRE_POLY:def 12;

        hence thesis by A2, A34, A35;

      end;

      uniqueness

      proof

        let IT1,IT2 be TermOrder of n such that

         A36: for a,b be bag of n holds [a, b] in IT1 iff (( TotDegree a) < ( TotDegree b) or ( TotDegree a) = ( TotDegree b) & [a, b] in o) and

         A37: for a,b be bag of n holds [a, b] in IT2 iff (( TotDegree a) < ( TotDegree b) or ( TotDegree a) = ( TotDegree b) & [a, b] in o);

        now

          let a,b be object;

          hereby

            assume

             A38: [a, b] in IT1;

            then

             A39: a in ( dom IT1) by XTUPLE_0:def 12;

            b in ( rng IT1) by A38, XTUPLE_0:def 13;

            then

            reconsider a9 = a, b9 = b as bag of n by A39;

            ( TotDegree a9) < ( TotDegree b9) or ( TotDegree a9) = ( TotDegree b9) & [a9, b9] in o by A36, A38;

            hence [a, b] in IT2 by A37;

          end;

          assume

           A40: [a, b] in IT2;

          then

           A41: a in ( dom IT2) by XTUPLE_0:def 12;

          b in ( rng IT2) by A40, XTUPLE_0:def 13;

          then

          reconsider a9 = a, b9 = b as bag of n by A41;

          ( TotDegree a9) < ( TotDegree b9) or ( TotDegree a9) = ( TotDegree b9) & [a9, b9] in o by A37, A40;

          hence [a, b] in IT1 by A36;

        end;

        hence IT1 = IT2 by RELAT_1:def 2;

      end;

    end

    theorem :: BAGORDER:26

    

     Th23: for n be Ordinal, o be TermOrder of n st (for a,b,c be bag of n st [a, b] in o holds [(a + c), (b + c)] in o) & o is_strongly_connected_in ( Bags n) holds ( Graded o) is admissible

    proof

      let n be Ordinal, o be TermOrder of n such that

       A1: for a,b,c be bag of n st [a, b] in o holds [(a + c), (b + c)] in o and

       A2: o is_strongly_connected_in ( Bags n);

      now

        let x,y be object such that

         A3: x in ( Bags n) and

         A4: y in ( Bags n);

        reconsider x9 = x, y9 = y as bag of n by A3, A4;

        assume

         A5: not [x, y] in ( Graded o);

        then

         A6: ( TotDegree x9) >= ( TotDegree y9) by A1, Def7;

        per cases by A6, XXREAL_0: 1;

          suppose ( TotDegree y9) < ( TotDegree x9);

          hence [y, x] in ( Graded o) by A1, Def7;

        end;

          suppose

           A7: ( TotDegree y9) = ( TotDegree x9);

          then not [x, y] in o by A1, A5, Def7;

          then [y, x] in o by A2, A3, A4;

          hence [y, x] in ( Graded o) by A1, A7, Def7;

        end;

      end;

      hence ( Graded o) is_strongly_connected_in ( Bags n);

      now

        let a be bag of n;

        

         A8: ( TotDegree ( EmptyBag n)) = 0 by Th14;

        per cases ;

          suppose a = ( EmptyBag n);

          hence [( EmptyBag n), a] in ( Graded o) by ORDERS_1: 3;

        end;

          suppose a <> ( EmptyBag n);

          then ( TotDegree a) <> 0 by Th14;

          hence [( EmptyBag n), a] in ( Graded o) by A1, A8, Def7;

        end;

      end;

      hence for a be bag of n holds [( EmptyBag n), a] in ( Graded o);

      now

        let a,b,c be bag of n such that

         A9: [a, b] in ( Graded o);

        per cases by A1, A9, Def7;

          suppose

           A10: ( TotDegree a) < ( TotDegree b);

          

           A11: ( TotDegree (a + c)) = (( TotDegree a) + ( TotDegree c)) by Th12;

          ( TotDegree (b + c)) = (( TotDegree b) + ( TotDegree c)) by Th12;

          then ( TotDegree (a + c)) < ( TotDegree (b + c)) by A10, A11, XREAL_1: 8;

          hence [(a + c), (b + c)] in ( Graded o) by A1, Def7;

        end;

          suppose

           A12: ( TotDegree a) = ( TotDegree b) & [a, b] in o;

          then ( TotDegree (a + c)) = (( TotDegree b) + ( TotDegree c)) by Th12;

          then

           A13: ( TotDegree (a + c)) = ( TotDegree (b + c)) by Th12;

           [(a + c), (b + c)] in o by A1, A12;

          hence [(a + c), (b + c)] in ( Graded o) by A1, A13, Def7;

        end;

      end;

      hence thesis;

    end;

    definition

      let n be Ordinal;

      :: BAGORDER:def8

      func GrLexOrder n -> TermOrder of n equals ( Graded ( LexOrder n));

      coherence ;

      :: BAGORDER:def9

      func GrInvLexOrder n -> TermOrder of n equals ( Graded ( InvLexOrder n));

      coherence ;

    end

    theorem :: BAGORDER:27

    

     Th24: for n be Ordinal holds ( GrLexOrder n) is admissible

    proof

      let n be Ordinal;

      

       A1: for a,b,c be bag of n st [a, b] in ( LexOrder n) holds [(a + c), (b + c)] in ( LexOrder n) by Def5;

      ( LexOrder n) is_strongly_connected_in ( Bags n) by Def5;

      hence thesis by A1, Th23;

    end;

    registration

      let n be Ordinal;

      cluster ( GrLexOrder n) -> admissible;

      coherence by Th24;

    end

    theorem :: BAGORDER:28

    for o be infinite Ordinal holds ( GrLexOrder o) is non well-ordering

    proof

      let o be infinite Ordinal;

      set R = ( GrLexOrder o);

      set r = RelStr (# ( Bags o), R #);

      set ir = the InternalRel of r, cr = the carrier of r;

      assume R is well-ordering;

      then

       A1: R is well_founded;

      cr = ( field ir) by ORDERS_1: 15;

      then ir is_well_founded_in cr by A1, WELLORD1: 3;

      then

       A2: r is well_founded;

      defpred P[ Nat, set] means $2 = ((o --> 0 ) +* ($1,1));

       A3:

      now

        let n be Element of NAT ;

        set y = ((o --> 0 ) +* (n,1));

        

         A4: ( dom (o --> 0 )) = o by FUNCOP_1: 13;

        reconsider y as ManySortedSet of o;

        

         A5: omega c= o by CARD_3: 85;

        now

          let x be object;

          hereby

            assume x in {n};

            then x = n by TARSKI:def 1;

            hence (y . x) <> 0 by A4, A5, FUNCT_7: 31;

          end;

          assume that

           A6: (y . x) <> 0 and

           A7: not x in {n};

          x <> n by A7, TARSKI:def 1;

          then

           A8: (y . x) = ((o --> 0 ) . x) by FUNCT_7: 32;

          per cases ;

            suppose x in ( dom (o --> 0 ));

            hence contradiction by A6, A8, FUNCOP_1: 7;

          end;

            suppose not x in ( dom (o --> 0 ));

            hence contradiction by A6, A8, FUNCT_1:def 2;

          end;

        end;

        then ( support y) = {n} by PRE_POLY:def 7;

        then y is finite-support by PRE_POLY:def 8;

        then

        reconsider y as Element of cr by PRE_POLY:def 12;

        take y;

        thus P[n, y];

      end;

      consider f be sequence of cr such that

       A9: for n be Element of NAT holds P[n, (f . n)] from FUNCT_2:sch 3( A3);

      reconsider f as sequence of r;

      f is descending

      proof

        let n be Nat;

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

        set fn1 = (f . (n0 + 1)), fn = (f . n0);

        

         A10: fn1 = ((o --> 0 ) +* ((n + 1),1)) by A9;

        

         A11: fn = ((o --> 0 ) +* (n,1)) by A9;

        reconsider fn1 as bag of o;

        reconsider fn as bag of o;

        

         A12: n0 in omega ;

        

         A13: omega c= o by CARD_3: 85;

        n <> (n + 1);

        

        then

         A14: (fn1 . n) = ((o --> 0 ) . n) by A10, FUNCT_7: 32

        .= 0 by A12, A13, FUNCOP_1: 7;

        

         A15: ( dom (o --> 0 )) = o by FUNCOP_1: 13;

        then

         A16: (fn . n) = 1 by A11, A13, FUNCT_7: 31;

        now

          let l be Ordinal;

          assume

           A17: l in n;

          then

           A18: l <> n;

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

          then n in { i where i be Nat : i < (n0 + 1) };

          then n in (n + 1) by AXIOMS: 4;

          then n c= (n + 1) by ORDINAL1:def 2;

          then l in (n + 1) by A17;

          then l <> (n + 1);

          

          hence (fn1 . l) = ((o --> 0 ) . l) by A10, FUNCT_7: 32

          .= (fn . l) by A11, A18, FUNCT_7: 32;

        end;

        then

         A19: fn1 < fn by A14, A16, PRE_POLY:def 9;

        thus (f . (n + 1)) <> (f . n) by A11, A13, A14, A15, FUNCT_7: 31;

        fn1 <=' fn by A19, PRE_POLY:def 10;

        then

         A20: [(f . (n + 1)), (f . n)] in ( LexOrder o) by PRE_POLY:def 14;

        consider tn be FinSequence of NAT such that

         A21: ( TotDegree fn) = ( Sum tn) and

         A22: tn = (fn * ( SgmX (( RelIncl o),( support fn)))) by Def4;

        consider tn1 be FinSequence of NAT such that

         A23: ( TotDegree fn1) = ( Sum tn1) and

         A24: tn1 = (fn1 * ( SgmX (( RelIncl o),( support fn1)))) by Def4;

         omega c= o by CARD_3: 85;

        then

        reconsider nn = n, n1n = (n + 1) as Element of o by A12;

        now

          let x be object;

          hereby

            assume

             A27: x in ( support fn1);

            now

              assume x <> n1n;

              then (fn1 . x) = ((o --> 0 ) . x) by A10, FUNCT_7: 32;

              then (fn1 . x) = 0 by A27, FUNCOP_1: 7;

              hence contradiction by A27, PRE_POLY:def 7;

            end;

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

          end;

          assume x in {n1n};

          then x = n1n by TARSKI:def 1;

          then (fn1 . x) = 1 by A10, A15, FUNCT_7: 31;

          hence x in ( support fn1) by PRE_POLY:def 7;

        end;

        then ( support fn1) = {n1n} by TARSKI: 2;

        then

         A28: ( SgmX (( RelIncl o),( support fn1))) = <*n1n*> by Th10;

        

         A29: ( dom fn) = o by A11, A15, FUNCT_7: 30;

        

         A30: ( dom fn1) = o by A10, A15, FUNCT_7: 30;

        now

          let x be object;

          hereby

            assume

             A31: x in ( support fn);

            now

              assume x <> nn;

              then (fn . x) = ((o --> 0 ) . x) by A11, FUNCT_7: 32;

              then (fn . x) = 0 by A31, FUNCOP_1: 7;

              hence contradiction by A31, PRE_POLY:def 7;

            end;

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

          end;

          assume x in {nn};

          then x = nn by TARSKI:def 1;

          then (fn . x) = 1 by A11, A15, FUNCT_7: 31;

          hence x in ( support fn) by PRE_POLY:def 7;

        end;

        then ( support fn) = {nn} by TARSKI: 2;

        then ( SgmX (( RelIncl o),( support fn))) = <*nn*> by Th10;

        

        then

         A32: tn = <*(fn . n)*> by A22, A29, FINSEQ_2: 34

        .= <*1*> by A11, A13, A15, FUNCT_7: 31

        .= <*(fn1 . n1n)*> by A10, A15, FUNCT_7: 31

        .= tn1 by A24, A28, A30, FINSEQ_2: 34;

        for a,b,c be bag of o st [a, b] in ( LexOrder o) holds [(a + c), (b + c)] in ( LexOrder o) by Def5;

        hence [(f . (n + 1)), (f . n)] in ir by A20, A21, A23, A32, Def7;

      end;

      hence contradiction by A2, WELLFND1: 14;

    end;

    theorem :: BAGORDER:29

    

     Th26: for n be Ordinal holds ( GrInvLexOrder n) is admissible

    proof

      let n be Ordinal;

      

       A1: for a,b,c be bag of n st [a, b] in ( InvLexOrder n) holds [(a + c), (b + c)] in ( InvLexOrder n) by Def5;

      ( InvLexOrder n) is_strongly_connected_in ( Bags n) by Def5;

      hence thesis by A1, Th23;

    end;

    registration

      let n be Ordinal;

      cluster ( GrInvLexOrder n) -> admissible;

      coherence by Th26;

    end

    theorem :: BAGORDER:30

    for o be Ordinal holds ( GrInvLexOrder o) is well-ordering

    proof

      let o be Ordinal;

      set gilo = ( GrInvLexOrder o), ilo = ( InvLexOrder o);

      

       A1: gilo is_strongly_connected_in ( Bags o) by Def5;

      

       A2: ( field gilo) = ( Bags o) by ORDERS_1: 12;

      then

       A3: gilo is_reflexive_in ( Bags o) by RELAT_2:def 9;

      

       A4: gilo is_transitive_in ( Bags o) by A2, RELAT_2:def 16;

      

       A5: gilo is_antisymmetric_in ( Bags o) by A2, RELAT_2:def 12;

      

       A6: gilo is_connected_in ( field gilo) by A1, A2;

      

       A7: for a,b,c be bag of o st [a, b] in ilo holds [(a + c), (b + c)] in ilo by Def5;

      now

        let Y be set such that

         A8: Y c= ( field gilo) and

         A9: Y <> {} ;

        set TD = { ( TotDegree y) where y be Element of ( Bags o) : y in Y };

        consider x be object such that

         A10: x in Y by A9, XBOOLE_0:def 1;

        reconsider x as Element of ( Bags o) by A8, A10, ORDERS_1: 12;

        

         A11: ( TotDegree x) in TD by A10;

        TD c= NAT

        proof

          let x be object;

          assume x in TD;

          then ex y be Element of ( Bags o) st (x = ( TotDegree y)) & (y in Y);

          hence thesis by ORDINAL1:def 12;

        end;

        then

        reconsider TD as non empty Subset of NAT by A11;

        set mTD = { y where y be Element of ( Bags o) : y in Y & ( TotDegree y) = ( min TD) };

        

         A12: mTD c= ( field gilo)

        proof

          let x be object;

          assume x in mTD;

          then ex y be Element of ( Bags o) st (x = y) & (y in Y) & (( TotDegree y) = ( min TD));

          hence thesis by A2;

        end;

        ( min TD) in TD by XXREAL_2:def 7;

        then

        consider y be Element of ( Bags o) such that

         A13: ( TotDegree y) = ( min TD) and

         A14: y in Y;

        

         A15: y in mTD by A13, A14;

        

         A16: ( field ilo) = ( Bags o) by ORDERS_1: 12;

        ilo is well-ordering by Th22;

        then ilo well_orders ( field ilo) by WELLORD1: 4;

        then ilo is_well_founded_in ( field ilo) by WELLORD1:def 5;

        then

        consider a be object such that

         A17: a in mTD and

         A18: (ilo -Seg a) misses mTD by A2, A12, A15, A16, WELLORD1:def 3;

        

         A19: ((ilo -Seg a) /\ mTD) = {} by A18, XBOOLE_0:def 7;

        

         A20: ex a9 be Element of ( Bags o) st (a9 = a) & (a9 in Y) & (( TotDegree a9) = ( min TD)) by A17;

        take a;

        thus a in Y by A20;

        now

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

          then

          consider z be object such that

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

          

           A22: z in (gilo -Seg a) by A21, XBOOLE_0:def 4;

          

           A23: z in Y by A21, XBOOLE_0:def 4;

          

           A24: z <> a by A22, WELLORD1: 1;

          

           A25: [z, a] in gilo by A22, WELLORD1: 1;

          reconsider a, z as Element of ( Bags o) by A8, A20, A23, ORDERS_1: 12;

          per cases by XXREAL_0: 1;

            suppose

             A26: ( TotDegree z) < ( TotDegree a);

            ( TotDegree z) in TD by A23;

            hence contradiction by A20, A26, XXREAL_2:def 7;

          end;

            suppose

             A27: ( TotDegree z) = ( TotDegree a);

            then [z, a] in ilo by A7, A25, Def7;

            then

             A28: z in (ilo -Seg a) by A24, WELLORD1: 1;

            z in mTD by A20, A23, A27;

            hence contradiction by A19, A28, XBOOLE_0:def 4;

          end;

            suppose ( TotDegree z) > ( TotDegree a);

            hence contradiction by A7, A25, Def7;

          end;

        end;

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

      end;

      then gilo is_well_founded_in ( field gilo) by WELLORD1:def 3;

      then gilo well_orders ( field gilo) by A2, A3, A4, A5, A6, WELLORD1:def 5;

      hence thesis by WELLORD1: 4;

    end;

    definition

      let i,n be Nat, o1 be TermOrder of (i + 1), o2 be TermOrder of (n -' (i + 1));

      :: BAGORDER:def10

      func BlockOrder (i,n,o1,o2) -> TermOrder of n means

      : Def10: for p,q be bag of n holds [p, q] in it iff (( 0 ,(i + 1)) -cut p) <> (( 0 ,(i + 1)) -cut q) & [(( 0 ,(i + 1)) -cut p), (( 0 ,(i + 1)) -cut q)] in o1 or (( 0 ,(i + 1)) -cut p) = (( 0 ,(i + 1)) -cut q) & [(((i + 1),n) -cut p), (((i + 1),n) -cut q)] in o2;

      existence

      proof

        

         A1: (i + 1) = ((i + 1) -' 0 ) by NAT_D: 40;

        defpred P[ object, object] means (ex p,q be bag of n st $1 = p & $2 = q & (((( 0 ,(i + 1)) -cut p) <> (( 0 ,(i + 1)) -cut q) & [(( 0 ,(i + 1)) -cut p), (( 0 ,(i + 1)) -cut q)] in o1) or ((( 0 ,(i + 1)) -cut p) = (( 0 ,(i + 1)) -cut q) & [(((i + 1),n) -cut p), (((i + 1),n) -cut q)] in o2)));

        consider BO be Relation of ( Bags n), ( Bags n) such that

         A2: for x,y be object holds [x, y] in BO iff x in ( Bags n) & y in ( Bags n) & P[x, y] from RELSET_1:sch 1;

        now

          let x be object such that

           A3: x in ( Bags n);

          reconsider x9 = x as bag of n by A3;

          

           A4: (( 0 ,(i + 1)) -cut x9) = (( 0 ,(i + 1)) -cut x9);

          (((i + 1),n) -cut x9) in ( Bags (n -' (i + 1))) by PRE_POLY:def 12;

          then [(((i + 1),n) -cut x9), (((i + 1),n) -cut x9)] in o2 by ORDERS_1: 3;

          hence [x, x] in BO by A2, A3, A4;

        end;

        then

         A5: BO is_reflexive_in ( Bags n);

        now

          let x,y be object such that x in ( Bags n) and y in ( Bags n) and

           A6: [x, y] in BO and

           A7: [y, x] in BO;

          consider p,q be bag of n such that

           A8: x = p and

           A9: y = q and

           A10: (( 0 ,(i + 1)) -cut p) <> (( 0 ,(i + 1)) -cut q) & [(( 0 ,(i + 1)) -cut p), (( 0 ,(i + 1)) -cut q)] in o1 or (( 0 ,(i + 1)) -cut p) = (( 0 ,(i + 1)) -cut q) & [(((i + 1),n) -cut p), (((i + 1),n) -cut q)] in o2 by A2, A6;

          

           A11: ex q9,p9 be bag of n st (y = q9) & (x = p9) & ((( 0 ,(i + 1)) -cut q9) <> (( 0 ,(i + 1)) -cut p9) & [(( 0 ,(i + 1)) -cut q9), (( 0 ,(i + 1)) -cut p9)] in o1 or (( 0 ,(i + 1)) -cut q9) = (( 0 ,(i + 1)) -cut p9) & [(((i + 1),n) -cut q9), (((i + 1),n) -cut p9)] in o2) by A2, A7;

          set CUTP1 = (( 0 ,(i + 1)) -cut p), CUTP2 = (((i + 1),n) -cut p);

          set CUTQ1 = (( 0 ,(i + 1)) -cut q), CUTQ2 = (((i + 1),n) -cut q);

          

           A12: CUTP1 in ( Bags ((i + 1) -' 0 )) by PRE_POLY:def 12;

          

           A13: CUTQ1 in ( Bags ((i + 1) -' 0 )) by PRE_POLY:def 12;

          

           A14: CUTP2 in ( Bags (n -' (i + 1))) by PRE_POLY:def 12;

          

           A15: CUTQ2 in ( Bags (n -' (i + 1))) by PRE_POLY:def 12;

          per cases by A10;

            suppose

             A16: CUTP1 <> CUTQ1 & [CUTP1, CUTQ1] in o1;

            now

              per cases by A8, A9, A11;

                suppose CUTQ1 <> CUTP1 & [CUTQ1, CUTP1] in o1;

                hence x = y by A1, A12, A13, A16, ORDERS_1: 4;

              end;

                suppose CUTQ1 = CUTP1 & [CUTQ2, CUTP2] in o2;

                hence x = y by A16;

              end;

            end;

            hence x = y;

          end;

            suppose

             A17: CUTP1 = CUTQ1 & [CUTP2, CUTQ2] in o2;

            now

              per cases by A8, A9, A11;

                suppose CUTQ1 <> CUTP1 & [CUTQ1, CUTP1] in o1;

                hence x = y by A17;

              end;

                suppose CUTQ1 = CUTP1 & [CUTQ2, CUTP2] in o2;

                then CUTQ2 = CUTP2 by A14, A15, A17, ORDERS_1: 4;

                hence x = y by A8, A9, A17, Th4;

              end;

            end;

            hence x = y;

          end;

        end;

        then

         A18: BO is_antisymmetric_in ( Bags n);

        now

          let x,y,z be object such that

           A19: x in ( Bags n) and y in ( Bags n) and

           A20: z in ( Bags n) and

           A21: [x, y] in BO and

           A22: [y, z] in BO;

          consider x9,y9 be bag of n such that

           A23: x9 = x and

           A24: y9 = y and

           A25: (( 0 ,(i + 1)) -cut x9) <> (( 0 ,(i + 1)) -cut y9) & [(( 0 ,(i + 1)) -cut x9), (( 0 ,(i + 1)) -cut y9)] in o1 or (( 0 ,(i + 1)) -cut x9) = (( 0 ,(i + 1)) -cut y9) & [(((i + 1),n) -cut x9), (((i + 1),n) -cut y9)] in o2 by A2, A21;

          consider y99,z9 be bag of n such that

           A26: y99 = y and

           A27: z9 = z and

           A28: (( 0 ,(i + 1)) -cut y99) <> (( 0 ,(i + 1)) -cut z9) & [(( 0 ,(i + 1)) -cut y99), (( 0 ,(i + 1)) -cut z9)] in o1 or (( 0 ,(i + 1)) -cut y99) = (( 0 ,(i + 1)) -cut z9) & [(((i + 1),n) -cut y99), (((i + 1),n) -cut z9)] in o2 by A2, A22;

          set CUTX1 = (( 0 ,(i + 1)) -cut x9), CUTX2 = (((i + 1),n) -cut x9);

          set CUTY1 = (( 0 ,(i + 1)) -cut y9), CUTY2 = (((i + 1),n) -cut y9);

          set CUTZ1 = (( 0 ,(i + 1)) -cut z9), CUTZ2 = (((i + 1),n) -cut z9);

          

           A29: CUTX1 in ( Bags ((i + 1) -' 0 )) by PRE_POLY:def 12;

          

           A30: CUTY1 in ( Bags ((i + 1) -' 0 )) by PRE_POLY:def 12;

          

           A31: CUTZ1 in ( Bags ((i + 1) -' 0 )) by PRE_POLY:def 12;

          

           A32: CUTX2 in ( Bags (n -' (i + 1))) by PRE_POLY:def 12;

          

           A33: CUTY2 in ( Bags (n -' (i + 1))) by PRE_POLY:def 12;

          

           A34: CUTZ2 in ( Bags (n -' (i + 1))) by PRE_POLY:def 12;

          per cases by A25;

            suppose

             A35: CUTX1 <> CUTY1 & [CUTX1, CUTY1] in o1;

            now

              per cases by A24, A26, A28;

                suppose

                 A36: CUTY1 <> CUTZ1 & [CUTY1, CUTZ1] in o1;

                then

                 A37: [CUTX1, CUTZ1] in o1 by A1, A29, A30, A31, A35, ORDERS_1: 5;

                now

                  per cases ;

                    suppose CUTX1 <> CUTZ1;

                    hence [x, z] in BO by A2, A19, A20, A23, A27, A37;

                  end;

                    suppose CUTX1 = CUTZ1;

                    hence [x, z] in BO by A1, A29, A30, A35, A36, ORDERS_1: 4;

                  end;

                end;

                hence [x, z] in BO;

              end;

                suppose CUTY1 = CUTZ1 & [CUTY2, CUTZ2] in o2;

                hence [x, z] in BO by A2, A19, A20, A23, A27, A35;

              end;

            end;

            hence [x, z] in BO;

          end;

            suppose

             A38: CUTX1 = CUTY1 & [CUTX2, CUTY2] in o2;

            now

              per cases by A24, A26, A28;

                suppose CUTY1 <> CUTZ1 & [CUTY1, CUTZ1] in o1;

                hence [x, z] in BO by A2, A19, A20, A23, A27, A38;

              end;

                suppose

                 A39: CUTY1 = CUTZ1 & [CUTY2, CUTZ2] in o2;

                then [CUTX2, CUTZ2] in o2 by A32, A33, A34, A38, ORDERS_1: 5;

                hence [x, z] in BO by A2, A19, A20, A23, A27, A38, A39;

              end;

            end;

            hence [x, z] in BO;

          end;

        end;

        then

         A40: BO is_transitive_in ( Bags n);

        

         A41: ( dom BO) = ( Bags n) by A5, ORDERS_1: 13;

        ( field BO) = ( Bags n) by A5, ORDERS_1: 13;

        then

        reconsider BO as TermOrder of n by A5, A18, A40, A41, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

        take BO;

        let p,q be bag of n;

        hereby

          assume [p, q] in BO;

          then ex p9,q9 be bag of n st (p9 = p) & (q9 = q) & ((( 0 ,(i + 1)) -cut p9) <> (( 0 ,(i + 1)) -cut q9) & [(( 0 ,(i + 1)) -cut p9), (( 0 ,(i + 1)) -cut q9)] in o1 or (( 0 ,(i + 1)) -cut p9) = (( 0 ,(i + 1)) -cut q9) & [(((i + 1),n) -cut p9), (((i + 1),n) -cut q9)] in o2) by A2;

          hence (( 0 ,(i + 1)) -cut p) <> (( 0 ,(i + 1)) -cut q) & [(( 0 ,(i + 1)) -cut p), (( 0 ,(i + 1)) -cut q)] in o1 or (( 0 ,(i + 1)) -cut p) = (( 0 ,(i + 1)) -cut q) & [(((i + 1),n) -cut p), (((i + 1),n) -cut q)] in o2;

        end;

        assume that

         A42: (( 0 ,(i + 1)) -cut p) <> (( 0 ,(i + 1)) -cut q) & [(( 0 ,(i + 1)) -cut p), (( 0 ,(i + 1)) -cut q)] in o1 or (( 0 ,(i + 1)) -cut p) = (( 0 ,(i + 1)) -cut q) & [(((i + 1),n) -cut p), (((i + 1),n) -cut q)] in o2;

        

         A43: p in ( Bags n) by PRE_POLY:def 12;

        q in ( Bags n) by PRE_POLY:def 12;

        hence thesis by A2, A42, A43;

      end;

      uniqueness

      proof

        let IT1,IT2 be TermOrder of n such that

         A44: for p,q be bag of n holds [p, q] in IT1 iff (( 0 ,(i + 1)) -cut p) <> (( 0 ,(i + 1)) -cut q) & [(( 0 ,(i + 1)) -cut p), (( 0 ,(i + 1)) -cut q)] in o1 or (( 0 ,(i + 1)) -cut p) = (( 0 ,(i + 1)) -cut q) & [(((i + 1),n) -cut p), (((i + 1),n) -cut q)] in o2 and

         A45: for p,q be bag of n holds [p, q] in IT2 iff (( 0 ,(i + 1)) -cut p) <> (( 0 ,(i + 1)) -cut q) & [(( 0 ,(i + 1)) -cut p), (( 0 ,(i + 1)) -cut q)] in o1 or (( 0 ,(i + 1)) -cut p) = (( 0 ,(i + 1)) -cut q) & [(((i + 1),n) -cut p), (((i + 1),n) -cut q)] in o2;

        now

          let a,b be object;

          hereby

            assume

             A46: [a, b] in IT1;

            then

             A47: a in ( dom IT1) by XTUPLE_0:def 12;

            b in ( rng IT1) by A46, XTUPLE_0:def 13;

            then

            reconsider p = a, q = b as bag of n by A47;

            (( 0 ,(i + 1)) -cut p) <> (( 0 ,(i + 1)) -cut q) & [(( 0 ,(i + 1)) -cut p), (( 0 ,(i + 1)) -cut q)] in o1 or (( 0 ,(i + 1)) -cut p) = (( 0 ,(i + 1)) -cut q) & [(((i + 1),n) -cut p), (((i + 1),n) -cut q)] in o2 by A44, A46;

            hence [a, b] in IT2 by A45;

          end;

          assume

           A48: [a, b] in IT2;

          then

           A49: a in ( dom IT2) by XTUPLE_0:def 12;

          b in ( rng IT2) by A48, XTUPLE_0:def 13;

          then

          reconsider p = a, q = b as bag of n by A49;

          (( 0 ,(i + 1)) -cut p) <> (( 0 ,(i + 1)) -cut q) & [(( 0 ,(i + 1)) -cut p), (( 0 ,(i + 1)) -cut q)] in o1 or (( 0 ,(i + 1)) -cut p) = (( 0 ,(i + 1)) -cut q) & [(((i + 1),n) -cut p), (((i + 1),n) -cut q)] in o2 by A45, A48;

          hence [a, b] in IT1 by A44;

        end;

        hence IT1 = IT2 by RELAT_1:def 2;

      end;

    end

    theorem :: BAGORDER:31

    for i,n be Nat, o1 be TermOrder of (i + 1), o2 be TermOrder of (n -' (i + 1)) st o1 is admissible & o2 is admissible holds ( BlockOrder (i,n,o1,o2)) is admissible

    proof

      let i,n be Nat, o1 be TermOrder of (i + 1), o2 be TermOrder of (n -' (i + 1)) such that

       A1: o1 is admissible and

       A2: o2 is admissible;

      

       A3: (i + 1) = ((i + 1) -' 0 ) by NAT_D: 40;

      then

       A4: o1 is_strongly_connected_in ( Bags ((i + 1) -' 0 )) by A1;

      

       A5: o2 is_strongly_connected_in ( Bags (n -' (i + 1))) by A2;

      set BO = ( BlockOrder (i,n,o1,o2));

      now

        now

          let x,y be object such that

           A6: x in ( Bags n) and

           A7: y in ( Bags n);

          reconsider p = x, q = y as bag of n by A6, A7;

          set CUTP1 = (( 0 ,(i + 1)) -cut p), CUTP2 = (((i + 1),n) -cut p);

          set CUTQ1 = (( 0 ,(i + 1)) -cut q), CUTQ2 = (((i + 1),n) -cut q);

          

           A8: CUTP1 in ( Bags ((i + 1) -' 0 )) by PRE_POLY:def 12;

          

           A9: CUTQ1 in ( Bags ((i + 1) -' 0 )) by PRE_POLY:def 12;

          

           A10: CUTP2 in ( Bags (n -' (i + 1))) by PRE_POLY:def 12;

          

           A11: CUTQ2 in ( Bags (n -' (i + 1))) by PRE_POLY:def 12;

          assume

           A12: not [x, y] in BO;

          per cases by A12, Def10;

            suppose

             A13: CUTP1 = CUTQ1;

            now

              per cases by A12, Def10;

                suppose CUTP1 <> CUTQ1;

                hence [y, x] in BO by A13;

              end;

                suppose not [CUTP2, CUTQ2] in o2;

                then [CUTQ2, CUTP2] in o2 by A5, A10, A11;

                hence [y, x] in BO by A13, Def10;

              end;

            end;

            hence [y, x] in BO;

          end;

            suppose not [CUTP1, CUTQ1] in o1;

            then

             A14: [CUTQ1, CUTP1] in o1 by A4, A8, A9;

            now

              per cases by A12, Def10;

                suppose CUTP1 <> CUTQ1;

                hence [y, x] in BO by A14, Def10;

              end;

                suppose not [CUTP2, CUTQ2] in o2;

                then

                 A15: [CUTQ2, CUTP2] in o2 by A5, A10, A11;

                per cases ;

                  suppose CUTP1 = CUTQ1;

                  hence [y, x] in BO by A15, Def10;

                end;

                  suppose CUTP1 <> CUTQ1;

                  hence [y, x] in BO by A14, Def10;

                end;

              end;

            end;

            hence [y, x] in BO;

          end;

        end;

        hence BO is_strongly_connected_in ( Bags n);

        let a be bag of n;

        set CUTE1 = (( 0 ,(i + 1)) -cut ( EmptyBag n)), CUTA1 = (( 0 ,(i + 1)) -cut a);

        set CUTE2 = (((i + 1),n) -cut ( EmptyBag n)), CUTA2 = (((i + 1),n) -cut a);

        now

          per cases ;

            suppose

             A16: CUTE1 <> CUTA1;

            CUTE1 = ( EmptyBag ((i + 1) -' 0 )) by Th15;

            then [CUTE1, CUTA1] in o1 by A1, A3;

            hence [( EmptyBag n), a] in BO by A16, Def10;

          end;

            suppose

             A17: CUTE1 = CUTA1;

            CUTE2 = ( EmptyBag (n -' (i + 1))) by Th15;

            then [CUTE2, CUTA2] in o2 by A2;

            hence [( EmptyBag n), a] in BO by A17, Def10;

          end;

        end;

        hence [( EmptyBag n), a] in BO;

        let a,b,c be bag of n such that

         A18: [a, b] in BO;

        set CUTA1 = (( 0 ,(i + 1)) -cut a), CUTA2 = (((i + 1),n) -cut a);

        set CUTB1 = (( 0 ,(i + 1)) -cut b), CUTB2 = (((i + 1),n) -cut b);

        set CUTC1 = (( 0 ,(i + 1)) -cut c), CUTC2 = (((i + 1),n) -cut c);

        set CUTAC1 = (( 0 ,(i + 1)) -cut (a + c)), CUTBC1 = (( 0 ,(i + 1)) -cut (b + c));

        set CUTAC2 = (((i + 1),n) -cut (a + c)), CUTBC2 = (((i + 1),n) -cut (b + c));

        per cases by A18, Def10;

          suppose

           A19: CUTA1 <> CUTB1 & [CUTA1, CUTB1] in o1;

          then [(CUTA1 + CUTC1), (CUTB1 + CUTC1)] in o1 by A1, A3;

          then [CUTAC1, (CUTB1 + CUTC1)] in o1 by Th16;

          then

           A20: [CUTAC1, CUTBC1] in o1 by Th16;

          now

            assume

             A21: (CUTA1 + CUTC1) = (CUTB1 + CUTC1);

            ((CUTA1 + CUTC1) -' CUTC1) = CUTA1 by PRE_POLY: 48;

            hence contradiction by A19, A21, PRE_POLY: 48;

          end;

          then CUTAC1 <> (CUTB1 + CUTC1) by Th16;

          then CUTAC1 <> CUTBC1 by Th16;

          hence [(a + c), (b + c)] in BO by A20, Def10;

        end;

          suppose

           A22: CUTA1 = CUTB1 & [CUTA2, CUTB2] in o2;

          then [(CUTA2 + CUTC2), (CUTB2 + CUTC2)] in o2 by A2;

          then [CUTAC2, (CUTB2 + CUTC2)] in o2 by Th16;

          then

           A23: [CUTAC2, CUTBC2] in o2 by Th16;

          CUTAC1 = (CUTB1 + CUTC1) by A22, Th16;

          then CUTAC1 = CUTBC1 by Th16;

          hence [(a + c), (b + c)] in BO by A23, Def10;

        end;

      end;

      hence thesis;

    end;

    definition

      let n be Nat;

      :: BAGORDER:def11

      func NaivelyOrderedBags n -> strict RelStr means

      : Def11: the carrier of it = ( Bags n) & for x,y be bag of n holds [x, y] in the InternalRel of it iff x divides y;

      existence

      proof

        defpred P[ object, object] means (ex x9,y9 be bag of n st x9 = $1 & y9 = $2 & x9 divides y9);

        consider IR be Relation of ( Bags n), ( Bags n) such that

         A1: for x,y be object holds [x, y] in IR iff x in ( Bags n) & y in ( Bags n) & P[x, y] from RELSET_1:sch 1;

        set IT = RelStr (# ( Bags n), IR #);

        reconsider IT as strict RelStr;

        take IT;

        thus the carrier of IT = ( Bags n);

        let x,y be bag of n;

        hereby

          assume [x, y] in the InternalRel of IT;

          then ex x9,y9 be bag of n st (x9 = x) & (y9 = y) & (x9 divides y9) by A1;

          hence x divides y;

        end;

        assume

         A2: x divides y;

        

         A3: x in ( Bags n) by PRE_POLY:def 12;

        y in ( Bags n) by PRE_POLY:def 12;

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        let IT1,IT2 be strict RelStr such that

         A4: the carrier of IT1 = ( Bags n) and

         A5: for x,y be bag of n holds [x, y] in the InternalRel of IT1 iff x divides y and

         A6: the carrier of IT2 = ( Bags n) and

         A7: for x,y be bag of n holds [x, y] in the InternalRel of IT2 iff x divides y;

        now

          let a,b be object;

          set z = [a, b];

          hereby

            assume

             A8: z in the InternalRel of IT1;

            then

            consider a9,b9 be object such that

             A9: z = [a9, b9] and

             A10: a9 in ( Bags n) and

             A11: b9 in ( Bags n) by A4, RELSET_1: 2;

            reconsider a9, b9 as bag of n by A10, A11;

            a9 divides b9 by A5, A8, A9;

            hence [a, b] in the InternalRel of IT2 by A7, A9;

          end;

          assume

           A12: [a, b] in the InternalRel of IT2;

          set z = [a, b];

          consider a9,b9 be object such that

           A13: z = [a9, b9] and

           A14: a9 in ( Bags n) and

           A15: b9 in ( Bags n) by A6, A12, RELSET_1: 2;

          reconsider a9, b9 as bag of n by A14, A15;

          a9 divides b9 by A7, A12, A13;

          hence [a, b] in the InternalRel of IT1 by A5, A13;

        end;

        hence thesis by A4, A6, RELAT_1:def 2;

      end;

    end

    theorem :: BAGORDER:32

    

     Th29: for n be Nat holds the carrier of ( product (n --> OrderedNAT )) = ( Bags n)

    proof

      let n be Nat;

      set X = the carrier of ( product (n --> OrderedNAT ));

      

       A1: X = ( product ( Carrier (n --> OrderedNAT ))) by YELLOW_1:def 4;

      now

        let x be object;

        hereby

          assume x in X;

          then

          consider g be Function such that

           A2: x = g and

           A3: ( dom g) = ( dom ( Carrier (n --> OrderedNAT ))) and

           A4: for i be object st i in ( dom ( Carrier (n --> OrderedNAT ))) holds (g . i) in (( Carrier (n --> OrderedNAT )) . i) by A1, CARD_3:def 5;

          

           A5: ( dom g) = n by A3, PARTFUN1:def 2;

          

           A6: ( rng g) c= NAT

          proof

            let z be object;

            assume z in ( rng g);

            then

            consider y be object such that

             A7: y in ( dom g) and

             A8: z = (g . y) by FUNCT_1:def 3;

            

             A9: z in (( Carrier (n --> OrderedNAT )) . y) by A3, A4, A7, A8;

            ex R be 1-sorted st (R = ((n --> OrderedNAT ) . y)) & ((( Carrier (n --> OrderedNAT )) . y) = the carrier of R) by A5, A7, PRALG_1:def 15;

            hence thesis by A5, A7, A9, DICKSON:def 15, FUNCOP_1: 7;

          end;

          

           A10: ( dom g) = ( dom ( Carrier (n --> OrderedNAT ))) by A3

          .= n by PARTFUN1:def 2;

          

           A11: g is natural-valued by A6, VALUED_0:def 6;

          g is ManySortedSet of n by A10, PARTFUN1:def 2, RELAT_1:def 18;

          hence x in ( Bags n) by A2, A11, PRE_POLY:def 12;

        end;

        assume x in ( Bags n);

        then

        reconsider g = x as natural-valued finite-support ManySortedSet of n;

        

         A12: ( dom g) = n by PARTFUN1:def 2;

        now

          take g;

          thus x = g;

          thus ( dom g) = ( dom ( Carrier (n --> OrderedNAT ))) by A12, PARTFUN1:def 2;

          let i be object;

          assume i in ( dom ( Carrier (n --> OrderedNAT )));

          then

           A13: i in n;

          reconsider ii = i as set by TARSKI: 1;

          consider R be 1-sorted such that

           A14: R = ((n --> OrderedNAT ) . ii) and

           A15: (( Carrier (n --> OrderedNAT )) . ii) = the carrier of R by PRALG_1:def 15, A13;

          R = OrderedNAT by A13, A14, FUNCOP_1: 7

          .= RelStr (# NAT , NATOrd #) by DICKSON:def 15;

          then (g . ii) in (( Carrier (n --> OrderedNAT )) . ii) by A15;

          hence (g . i) in (( Carrier (n --> OrderedNAT )) . i);

        end;

        then x in ( product ( Carrier (n --> OrderedNAT ))) by CARD_3:def 5;

        hence x in X by YELLOW_1:def 4;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: BAGORDER:33

    

     Th30: for n be Nat holds ( NaivelyOrderedBags n) = ( product (n --> OrderedNAT ))

    proof

      let n be Nat;

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

      set CNOB = the carrier of ( NaivelyOrderedBags n);

      set IROB = the InternalRel of ( NaivelyOrderedBags n);

      set CP = the carrier of ( product (n --> OrderedNAT ));

      set IP = the InternalRel of ( product (n --> OrderedNAT ));

      CNOB = ( Bags n) by Def11;

      then

       A1: CNOB = CP by Th29;

      now

        let a,b be object;

        hereby

          assume

           A2: [a, b] in IROB;

          then

           A3: a in ( dom IROB) by XTUPLE_0:def 12;

          

           A4: b in ( rng IROB) by A2, XTUPLE_0:def 13;

          

           A5: a in CNOB by A3;

          

           A6: b in CNOB by A4;

          

           A7: a in ( Bags n) by A5, Def11;

          

           A8: b in ( Bags n) by A6, Def11;

          then

          reconsider a9 = a, b9 = b as Element of CP by A7, Th29;

          a9 in the carrier of ( product (n0 --> OrderedNAT ));

          then

           A9: a9 in ( product ( Carrier (n --> OrderedNAT ))) by YELLOW_1:def 4;

          now

            set f = a9, g = b9;

            

             A10: a9 is bag of n by A7;

            

             A11: b is bag of n by A8;

            reconsider f, g as Function by A7, A8;

            take f, g;

            thus f = a9 & g = b9;

            let i be object;

            assume

             A12: i in n;

            set R = ((n --> OrderedNAT ) . i);

            

             A13: R = OrderedNAT by A12, FUNCOP_1: 7;

            reconsider R as RelStr by A12, FUNCOP_1: 7;

            take R;

            set xi = (f . i);

            set yi = (g . i);

            ( dom f) = n by A10, PARTFUN1:def 2;

            then

             A14: (f . i) in ( rng f) by A12, FUNCT_1: 3;

            

             A15: ( rng f) c= NAT by A10, VALUED_0:def 6;

            ( dom g) = n by A11, PARTFUN1:def 2;

            then

             A16: (g . i) in ( rng g) by A12, FUNCT_1: 3;

            

             A17: ( rng g) c= NAT by A11, VALUED_0:def 6;

            then

            reconsider xi, yi as Element of R by A12, A14, A15, A16, DICKSON:def 15, FUNCOP_1: 7;

            take xi, yi;

            thus R = ((n --> OrderedNAT ) . i) & xi = (f . i) & yi = (g . i);

            reconsider a99 = a9, b99 = b9 as bag of n by A7, A8;

            

             A18: xi in NAT & yi in NAT by A15, A17, A14, A16;

            a99 divides b99 by A2, Def11;

            then (a99 . i) <= (b99 . i) by PRE_POLY:def 11;

            then [xi, yi] in NATOrd by DICKSON:def 14, A18;

            hence xi <= yi by A13, DICKSON:def 15, ORDERS_2:def 5;

          end;

          then a9 <= b9 by A9, YELLOW_1:def 4;

          hence [a, b] in IP by ORDERS_2:def 5;

        end;

        assume

         A19: [a, b] in IP;

        then

         A20: a in ( dom IP) by XTUPLE_0:def 12;

        

         A21: b in ( rng IP) by A19, XTUPLE_0:def 13;

        

         A22: a in CP by A20;

        

         A23: b in CP by A21;

        

         A24: a in ( Bags n) by A22, Th29;

        b in ( Bags n) by A23, Th29;

        then

        reconsider a9 = a, b9 = b as bag of n by A24;

        reconsider a2 = a9, b2 = b9 as Element of CP by A20, A21;

        a2 in the carrier of ( product (n0 --> OrderedNAT ));

        then

         A25: a2 in ( product ( Carrier (n --> OrderedNAT ))) by YELLOW_1:def 4;

        a2 <= b2 by A19, ORDERS_2:def 5;

        then

        consider f,g be Function such that

         A26: f = a2 and

         A27: g = b2 and

         A28: for i be object st i in n holds ex R be RelStr, xi,yi be Element of R st R = ((n --> OrderedNAT ) . i) & xi = (f . i) & yi = (g . i) & xi <= yi by A25, YELLOW_1:def 4;

        now

          let k be object such that

           A29: k in n;

          consider R be RelStr, xi,yi be Element of R such that

           A30: R = ((n --> OrderedNAT ) . k) and

           A31: xi = (f . k) and

           A32: yi = (g . k) and

           A33: xi <= yi by A28, A29;

          R = OrderedNAT by A29, A30, FUNCOP_1: 7;

          then [xi, yi] in NATOrd by A33, DICKSON:def 15, ORDERS_2:def 5;

          then

          consider xii,yii be Element of NAT such that

           A34: [xii, yii] = [xi, yi] and

           A35: xii <= yii by DICKSON:def 14;

          xii = xi by A34, XTUPLE_0: 1;

          hence (a9 . k) <= (b9 . k) by A26, A27, A31, A32, A34, A35, XTUPLE_0: 1;

        end;

        then a9 divides b9 by PRE_POLY: 46;

        hence [a, b] in IROB by Def11;

      end;

      hence thesis by A1, RELAT_1:def 2;

    end;

    theorem :: BAGORDER:34

    for n be Nat, o be TermOrder of n st o is admissible holds the InternalRel of ( NaivelyOrderedBags n) c= o & o is well-ordering

    proof

      let n be Nat, o be TermOrder of n such that

       A1: o is admissible;

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

      set IRN = the InternalRel of ( NaivelyOrderedBags n);

      now

        let a,b be object such that

         A2: [a, b] in IRN;

        

         A3: a in ( dom IRN) by A2, XTUPLE_0:def 12;

        b in ( rng IRN) by A2, XTUPLE_0:def 13;

        then

        reconsider a1 = a, b1 = b as Element of ( Bags n) by A3, Def11;

        

         A4: a1 divides b1 by A2, Def11;

        set l = (b1 -' a1);

        now

          let i be object such that i in n;

          

           A5: ((l + a1) . i) = ((l . i) + (a1 . i)) by PRE_POLY:def 5

          .= (((b1 . i) -' (a1 . i)) + (a1 . i)) by PRE_POLY:def 6;

          (a1 . i) <= (b1 . i) by A4, PRE_POLY:def 11;

          then ((a1 . i) - (a1 . i)) <= ((b1 . i) - (a1 . i)) by XREAL_1: 9;

          

          hence ((l + a1) . i) = (((b1 . i) + ( - (a1 . i))) + (a1 . i)) by A5, XREAL_0:def 2

          .= (b1 . i);

        end;

        then

         A6: (l + a1) = b1 by PBOOLE: 3;

         [( EmptyBag n), l] in o by A1;

        then [(( EmptyBag n) + a1), (l + a1)] in o by A1;

        hence [a, b] in o by A6, PRE_POLY: 53;

      end;

      hence

       A7: the InternalRel of ( NaivelyOrderedBags n) c= o by RELAT_1:def 3;

      set R = ( product (n0 --> OrderedNAT )), S = RelStr (# ( Bags n), o #);

      

       A8: S is quasi_ordered by DICKSON:def 3;

      

       A9: the InternalRel of R c= the InternalRel of S by A7, Th30;

      the carrier of R = the carrier of S by Th29;

      then

       A10: (S \~ ) is well_founded by A8, A9, DICKSON: 49;

      o is_strongly_connected_in ( Bags n) by A1;

      then

       A11: o is_connected_in ( Bags n);

      

       A12: ( field o) = ( Bags n) by ORDERS_1: 12;

      S is well_founded by A10, DICKSON: 16;

      then

       A13: o is_well_founded_in ( field o) by A12;

      

       A14: o is connected by A11, A12;

      o is well_founded by A13, WELLORD1: 3;

      hence thesis by A14;

    end;

    begin

    definition

      let R be connected non empty Poset, X be Element of ( Fin the carrier of R);

      :: BAGORDER:def12

      func PosetMin X -> Element of R means it in X & it is_minimal_wrt (X,the InternalRel of R);

      existence

      proof

        set IR = the InternalRel of R;

        X c= the carrier of R by FINSUB_1:def 5;

        then

        consider x be Element of R such that

         A2: x in X and

         A3: x is_minimal_wrt (X,IR) by A1, Th6;

        take x;

        thus thesis by A2, A3;

      end;

      uniqueness

      proof

        let IT1,IT2 be Element of R such that

         A4: IT1 in X and

         A5: IT1 is_minimal_wrt (X,the InternalRel of R) and

         A6: IT2 in X and

         A7: IT2 is_minimal_wrt (X,the InternalRel of R);

        set IR = the InternalRel of R;

        

         A8: IT1 <= IT2 or IT2 <= IT1 by WAYBEL_0:def 29;

        per cases by A8, ORDERS_2:def 5;

          suppose [IT1, IT2] in IR;

          hence thesis by A4, A7, WAYBEL_4:def 25;

        end;

          suppose [IT2, IT1] in IR;

          hence thesis by A5, A6, WAYBEL_4:def 25;

        end;

      end;

      :: BAGORDER:def13

      func PosetMax X -> Element of R means

      : Def13: it in X & it is_maximal_wrt (X,the InternalRel of R);

      existence

      proof

        set IR = the InternalRel of R;

        X c= the carrier of R by FINSUB_1:def 5;

        then

        consider x be Element of R such that

         A9: x in X and

         A10: x is_maximal_wrt (X,IR) by A1, Th5;

        take x;

        thus thesis by A9, A10;

      end;

      uniqueness

      proof

        let IT1,IT2 be Element of R such that

         A11: IT1 in X and

         A12: IT1 is_maximal_wrt (X,the InternalRel of R) and

         A13: IT2 in X and

         A14: IT2 is_maximal_wrt (X,the InternalRel of R);

        set IR = the InternalRel of R;

        

         A15: IT1 <= IT2 or IT2 <= IT1 by WAYBEL_0:def 29;

        per cases by A15, ORDERS_2:def 5;

          suppose [IT1, IT2] in IR;

          hence thesis by A12, A13, WAYBEL_4:def 23;

        end;

          suppose [IT2, IT1] in IR;

          hence thesis by A11, A14, WAYBEL_4:def 23;

        end;

      end;

    end

    definition

      let R be connected non empty Poset;

      :: BAGORDER:def14

      func FinOrd-Approx R -> sequence of ( bool [:( Fin the carrier of R), ( Fin the carrier of R):]) means

      : Def14: ( dom it ) = NAT & (it . 0 ) = { [x, y] where x,y be Element of ( Fin the carrier of R) : x = {} or (x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in the InternalRel of R) } & for n be Nat holds (it . (n + 1)) = { [x, y] where x,y be Element of ( Fin the carrier of R) : x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in (it . n) };

      existence

      proof

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

        set FBCP = [:( Fin CR), ( Fin CR):];

        defpred P[ Nat, set, set] means $3 = { [x, y] where x,y be Element of ( Fin CR) : x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in $2 };

        

         A1: for n be Nat holds for x be set holds ex y be set st P[n, x, y];

        consider f be Function such that

         A2: ( dom f) = NAT and

         A3: (f . 0 ) = { [x, y] where x,y be Element of ( Fin CR) : x = {} or (x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in IR) } and

         A4: for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 1( A1);

        

         A5: for n be Nat holds P[n, (f . n), (f . (n + 1))] by A4;

        now

          thus ( dom f) = NAT by A2;

          let x be object;

          assume x in NAT ;

          then

          reconsider x9 = x as Element of NAT ;

          per cases ;

            suppose

             A6: x9 = 0 ;

            set F0 = { [a, b] where a,b be Element of ( Fin the carrier of R) : a = {} or (a <> {} & b <> {} & ( PosetMax a) <> ( PosetMax b) & [( PosetMax a), ( PosetMax b)] in IR) };

            now

              let z be object;

              assume z in F0;

              then ex a,b be Element of ( Fin CR) st (z = [a, b]) & (a = {} or a <> {} & b <> {} & ( PosetMax a) <> ( PosetMax b) & [( PosetMax a), ( PosetMax b)] in IR);

              hence z in FBCP;

            end;

            then F0 c= FBCP;

            hence (f . x) in ( bool [:( Fin CR), ( Fin CR):]) by A3, A6;

          end;

            suppose

             A7: x9 > 0 ;

            

             A8: x9 = ((x9 - 1) + 1);

            reconsider x1 = (x9 - 1) as Element of NAT by A7, NAT_1: 20;

            set FX = { [a, b] where a,b be Element of ( Fin CR) : a <> {} & b <> {} & ( PosetMax a) = ( PosetMax b) & [(a \ {( PosetMax a)}), (b \ {( PosetMax b)})] in (f . x1) };

            

             A9: FX = (f . x9) by A4, A8;

            now

              let z be object;

              assume z in FX;

              then ex a,b be Element of ( Fin CR) st (z = [a, b]) & (a <> {} ) & (b <> {} ) & (( PosetMax a) = ( PosetMax b)) & ( [(a \ {( PosetMax a)}), (b \ {( PosetMax b)})] in (f . x1));

              hence z in FBCP;

            end;

            then FX c= FBCP;

            hence (f . x) in ( bool [:( Fin CR), ( Fin CR):]) by A9;

          end;

        end;

        then

        reconsider f as sequence of ( bool FBCP) by FUNCT_2: 3;

        take f;

        thus thesis by A2, A3, A5;

      end;

      uniqueness

      proof

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

        set FBCP = [:( Fin CR), ( Fin CR):];

        let IT1,IT2 be sequence of ( bool FBCP) such that

         A10: ( dom IT1) = NAT and

         A11: (IT1 . 0 ) = { [x, y] where x,y be Element of ( Fin CR) : x = {} or (x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in IR) } and

         A12: for n be Nat holds (IT1 . (n + 1)) = { [x, y] where x,y be Element of ( Fin CR) : x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in (IT1 . n) } and

         A13: ( dom IT2) = NAT and

         A14: (IT2 . 0 ) = { [x, y] where x,y be Element of ( Fin CR) : x = {} or (x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in IR) } and

         A15: for n be Nat holds (IT2 . (n + 1)) = { [x, y] where x,y be Element of ( Fin CR) : x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in (IT2 . n) };

        defpred P[ Nat, set, set] means $3 = { [x, y] where x,y be Element of ( Fin CR) : x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in $2 };

        

         A16: ( dom IT1) = NAT by A10;

        

         A17: (IT1 . 0 ) = { [x, y] where x,y be Element of ( Fin CR) : x = {} or (x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in IR) } by A11;

        

         A18: for n be Nat holds P[n, (IT1 . n), (IT1 . (n + 1))] by A12;

        

         A19: ( dom IT2) = NAT by A13;

        

         A20: (IT2 . 0 ) = { [x, y] where x,y be Element of ( Fin CR) : x = {} or (x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in IR) } by A14;

        

         A21: for n be Nat holds P[n, (IT2 . n), (IT2 . (n + 1))] by A15;

        

         A22: for n be Nat, x,y1,y2 be set st P[n, x, y1] & P[n, x, y2] holds y1 = y2;

        thus IT1 = IT2 from NAT_1:sch 13( A16, A17, A18, A19, A20, A21, A22);

      end;

    end

    theorem :: BAGORDER:35

    

     Th32: for R be connected non empty Poset, x,y be Element of ( Fin the carrier of R) holds [x, y] in ( union ( rng ( FinOrd-Approx R))) iff x = {} or x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in the InternalRel of R or x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( union ( rng ( FinOrd-Approx R)))

    proof

      let R be connected non empty Poset, x,y be Element of ( Fin the carrier of R);

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

      set FOAR = ( FinOrd-Approx R);

      

       A1: (FOAR . 0 ) = { [a, b] where a,b be Element of ( Fin CR) : a = {} or (a <> {} & b <> {} & ( PosetMax a) <> ( PosetMax b) & [( PosetMax a), ( PosetMax b)] in IR) } by Def14;

      

       A2: ( dom FOAR) = NAT by Def14;

      hereby

        assume [x, y] in ( union ( rng FOAR));

        then

        consider Y be set such that

         A3: [x, y] in Y and

         A4: Y in ( rng FOAR) by TARSKI:def 4;

        consider n be object such that

         A5: n in ( dom FOAR) and

         A6: Y = (FOAR . n) by A4, FUNCT_1:def 3;

        reconsider n as Element of NAT by A5;

        per cases ;

          suppose n = 0 ;

          then

          consider a,b be Element of ( Fin CR) such that

           A7: [x, y] = [a, b] and

           A8: a = {} or a <> {} & b <> {} & ( PosetMax a) <> ( PosetMax b) & [( PosetMax a), ( PosetMax b)] in IR by A1, A3, A6;

          x = a by A7, XTUPLE_0: 1;

          hence x = {} or x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in IR or x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( union ( rng FOAR)) by A7, A8, XTUPLE_0: 1;

        end;

          suppose n > 0 ;

          then

           A9: (n - 1) is Element of NAT by NAT_1: 20;

          then (FOAR . ((n - 1) + 1)) = { [a, b] where a,b be Element of ( Fin CR) : a <> {} & b <> {} & ( PosetMax a) = ( PosetMax b) & [(a \ {( PosetMax a)}), (b \ {( PosetMax b)})] in (FOAR . (n - 1)) } by Def14;

          then

          consider a,b be Element of ( Fin CR) such that

           A10: [x, y] = [a, b] and a <> {} and

           A11: b <> {} and

           A12: ( PosetMax a) = ( PosetMax b) and

           A13: [(a \ {( PosetMax a)}), (b \ {( PosetMax b)})] in (FOAR . (n - 1)) by A3, A6;

          

           A14: x = a by A10, XTUPLE_0: 1;

          

           A15: y = b by A10, XTUPLE_0: 1;

          (FOAR . (n - 1)) in ( rng FOAR) by A2, A9, FUNCT_1:def 3;

          hence x = {} or x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in IR or x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( union ( rng FOAR)) by A11, A12, A13, A14, A15, TARSKI:def 4;

        end;

      end;

      assume

       A16: x = {} or x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in IR or x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( union ( rng FOAR));

      per cases by A16;

        suppose x = {} ;

        then

         A17: [x, y] in (FOAR . 0 ) by A1;

        (FOAR . 0 ) in ( rng FOAR) by A2, FUNCT_1:def 3;

        hence thesis by A17, TARSKI:def 4;

      end;

        suppose x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in IR;

        then

         A18: [x, y] in (FOAR . 0 ) by A1;

        (FOAR . 0 ) in ( rng FOAR) by A2, FUNCT_1:def 3;

        hence thesis by A18, TARSKI:def 4;

      end;

        suppose

         A19: x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( union ( rng FOAR));

        set NEXTXY = [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})];

        consider Y be set such that

         A20: NEXTXY in Y and

         A21: Y in ( rng ( FinOrd-Approx R)) by A19, TARSKI:def 4;

        consider n be object such that

         A22: n in ( dom FOAR) and

         A23: Y = (FOAR . n) by A21, FUNCT_1:def 3;

        reconsider n as Nat by A22;

        (FOAR . (n + 1)) = { [a, b] where a,b be Element of ( Fin CR) : a <> {} & b <> {} & ( PosetMax a) = ( PosetMax b) & [(a \ {( PosetMax a)}), (b \ {( PosetMax b)})] in (FOAR . n) } by Def14;

        then

         A24: [x, y] in (FOAR . (n + 1)) by A19, A20, A23;

        (FOAR . (n + 1)) in ( rng FOAR) by A2, FUNCT_1:def 3;

        hence thesis by A24, TARSKI:def 4;

      end;

    end;

    theorem :: BAGORDER:36

    

     Th33: for R be connected non empty Poset, x be Element of ( Fin the carrier of R) st x <> {} holds not [x, {} ] in ( union ( rng ( FinOrd-Approx R)))

    proof

      let R be connected non empty Poset, x be Element of ( Fin the carrier of R) such that

       A1: x <> {} ;

      set CR = the carrier of R, FOAR = ( FinOrd-Approx R);

      reconsider y = {} as Element of ( Fin CR) by FINSUB_1: 7;

      now

        assume

         A2: [x, y] in ( union ( rng ( FinOrd-Approx R)));

        per cases by A2, Th32;

          suppose x = {} ;

          hence contradiction by A1;

        end;

          suppose x <> {} & y <> {} & [( PosetMax x), ( PosetMax y)] in CR;

          hence contradiction;

        end;

          suppose x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ ( PosetMax x)), ( {} \ ( PosetMax y))] in ( union ( rng FOAR));

          hence contradiction;

        end;

      end;

      hence thesis;

    end;

    theorem :: BAGORDER:37

    

     Th34: for R be connected non empty Poset, a be Element of ( Fin the carrier of R) holds (a \ {( PosetMax a)}) is Element of ( Fin the carrier of R)

    proof

      let R be connected non empty Poset, a be Element of ( Fin the carrier of R);

      set CR = the carrier of R;

      

       A1: a c= CR by FINSUB_1:def 5;

      reconsider a9 = a as finite set;

      set z = (a9 \ {( PosetMax a)});

      z c= CR by A1;

      hence thesis by FINSUB_1:def 5;

    end;

    

     Lm1: for R be connected non empty Poset, n be Nat, a be Element of ( Fin the carrier of R) st ( card a) = (n + 1) holds ( card (a \ {( PosetMax a)})) = n

    proof

      let R be connected non empty Poset, n be Nat, a be Element of ( Fin the carrier of R);

      assume

       A1: ( card a) = (n + 1);

      reconsider a9 = a as finite set;

      now

        let w be object;

        assume w in {( PosetMax a)};

        then w = ( PosetMax a) by TARSKI:def 1;

        hence w in a by A1, Def13, CARD_1: 27;

      end;

      then {( PosetMax a)} c= a;

      then

       A2: ( card (a9 \ {( PosetMax a)})) = (( card a9) - ( card {( PosetMax a)})) by CARD_2: 44;

      ( card {( PosetMax a)}) = 1 by CARD_1: 30;

      hence thesis by A1, A2;

    end;

    theorem :: BAGORDER:38

    

     Th35: for R be connected non empty Poset holds ( union ( rng ( FinOrd-Approx R))) is Order of ( Fin the carrier of R)

    proof

      let R be connected non empty Poset;

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

      set X = ( union ( rng ( FinOrd-Approx R)));

      set FOAR = ( FinOrd-Approx R);

      set FOAR0 = { [a, b] where a,b be Element of ( Fin CR) : a = {} or (a <> {} & b <> {} & ( PosetMax a) <> ( PosetMax b) & [( PosetMax a), ( PosetMax b)] in IR) };

      

       A1: (FOAR . 0 ) = FOAR0 by Def14;

      now

        let x be object;

        assume x in X;

        then

         A2: ex Y be set st (x in Y) & (Y in ( rng FOAR)) by TARSKI:def 4;

        ( rng FOAR) c= ( bool [:( Fin CR), ( Fin CR):]) by RELAT_1:def 19;

        hence x in [:( Fin CR), ( Fin CR):] by A2;

      end;

      then

      reconsider X as Relation of ( Fin CR) by TARSKI:def 3;

       A3:

      now

        let x be object such that

         A4: x in ( Fin CR);

         0 in NAT ;

        then 0 in ( dom FOAR) by Def14;

        then

         A5: (FOAR . 0 ) in ( rng FOAR) by FUNCT_1:def 3;

        reconsider x9 = x as Element of ( Fin CR) by A4;

        defpred P[ Nat] means (for x be Element of ( Fin CR) st ( card x) = $1 holds [x, x] in ( union ( rng FOAR)));

        

         A6: P[ 0 ]

        proof

          let x be Element of ( Fin CR);

          assume ( card x) = 0 ;

          then x = {} ;

          then [x, x] in (FOAR . 0 ) by A1;

          hence thesis by A5, TARSKI:def 4;

        end;

        

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

        proof

          let n be Nat such that

           A8: for x be Element of ( Fin CR) st ( card x) = n holds [x, x] in ( union ( rng FOAR));

          let y be Element of ( Fin CR) such that

           A9: ( card y) = (n + 1);

          per cases ;

            suppose y = {} ;

            then [y, y] in (FOAR . 0 ) by A1;

            hence thesis by A5, TARSKI:def 4;

          end;

            suppose

             A10: y <> {} ;

            set z = (y \ {( PosetMax y)});

            reconsider z as Element of ( Fin CR) by Th34;

            ( card z) = n by A9, Lm1;

            then [z, z] in ( union ( rng FOAR)) by A8;

            hence thesis by A10, Th32;

          end;

        end;

        

         A11: for n be Nat holds P[n] from NAT_1:sch 2( A6, A7);

        reconsider xx = x as set by TARSKI: 1;

        ( card x9) = ( card xx);

        hence [x, x] in X by A11;

      end;

       A12:

      now

        let x,y be object such that

         A13: x in ( Fin CR) and

         A14: y in ( Fin CR) and

         A15: [x, y] in X and

         A16: [y, x] in X;

        reconsider x9 = x as Element of ( Fin CR) by A13;

        defpred R[ Nat] means (for x,y be Element of ( Fin CR) st ( card x) = $1 & [x, y] in X & [y, x] in X holds x = y);

        now

          let a,b be Element of ( Fin CR) such that

           A17: ( card a) = 0 and [a, b] in X and

           A18: [b, a] in X;

          reconsider a9 = a as finite set;

          a9 = {} by A17;

          hence a = b by A18, Th33;

        end;

        then

         A19: R[ 0 ];

        now

          let n be Nat such that

           A20: for a,b be Element of ( Fin CR) st ( card a) = n & [a, b] in X & [b, a] in X holds a = b;

          let a,b be Element of ( Fin CR) such that

           A21: ( card a) = (n + 1) and

           A22: [a, b] in X and

           A23: [b, a] in X;

          per cases by A22, Th32;

            suppose a = {} ;

            hence a = b by A21;

          end;

            suppose

             A24: a <> {} & b <> {} & ( PosetMax a) <> ( PosetMax b) & [( PosetMax a), ( PosetMax b)] in IR;

            now

              per cases by A23, Th32;

                suppose b = {} ;

                hence a = b by A24;

              end;

                suppose b <> {} & a <> {} & ( PosetMax b) <> ( PosetMax a) & [( PosetMax b), ( PosetMax a)] in IR;

                hence a = b by A24, ORDERS_1: 4;

              end;

                suppose b <> {} & a <> {} & ( PosetMax b) = ( PosetMax a) & [(b \ {( PosetMax b)}), (a \ {( PosetMax a)})] in X;

                hence a = b by A24;

              end;

            end;

            hence a = b;

          end;

            suppose

             A25: a <> {} & b <> {} & ( PosetMax a) = ( PosetMax b) & [(a \ {( PosetMax a)}), (b \ {( PosetMax b)})] in X;

            now

              per cases by A23, Th32;

                suppose b = {} ;

                hence a = b by A25;

              end;

                suppose b <> {} & a <> {} & ( PosetMax b) <> ( PosetMax a) & [( PosetMax b), ( PosetMax a)] in IR;

                hence a = b by A25;

              end;

                suppose

                 A26: b <> {} & a <> {} & ( PosetMax b) = ( PosetMax a) & [(b \ {( PosetMax b)}), (a \ {( PosetMax a)})] in X;

                reconsider a9 = a as finite set;

                reconsider b9 = b as finite set;

                set za = (a9 \ {( PosetMax a)}), zb = (b9 \ {( PosetMax b)});

                reconsider za, zb as Element of ( Fin CR) by Th34;

                ( card za) = n by A21, Lm1;

                then

                 A27: za = zb by A20, A25, A26;

                now

                  let z be object;

                  assume z in {( PosetMax a)};

                  then z = ( PosetMax a) by TARSKI:def 1;

                  hence z in a by A26, Def13;

                end;

                then {( PosetMax a)} c= a;

                then

                 A28: a = ( {( PosetMax a)} \/ za) by XBOOLE_1: 45;

                now

                  let z be object;

                  assume z in {( PosetMax b)};

                  then z = ( PosetMax b) by TARSKI:def 1;

                  hence z in b by A26, Def13;

                end;

                then {( PosetMax b)} c= b;

                hence a = b by A26, A27, A28, XBOOLE_1: 45;

              end;

            end;

            hence a = b;

          end;

        end;

        then

         A29: for n be Nat st R[n] holds R[(n + 1)];

        

         A30: for n be Nat holds R[n] from NAT_1:sch 2( A19, A29);

        reconsider xx = x as set by TARSKI: 1;

        ( card x9) = ( card xx);

        hence x = y by A14, A15, A16, A30;

      end;

       A31:

      now

        let x,y,z be object such that

         A32: x in ( Fin CR) and

         A33: y in ( Fin CR) and

         A34: z in ( Fin CR) and

         A35: [x, y] in X and

         A36: [y, z] in X;

        defpred S[ Nat] means (for a,b,c be Element of ( Fin CR) st ( card a) = $1 & [a, b] in X & [b, c] in X holds [a, c] in X);

        now

          let a,b,c be Element of ( Fin CR) such that

           A37: ( card a) = 0 and [a, b] in X and [b, c] in X;

          reconsider a9 = a as finite set;

          a9 = {} by A37;

          hence [a, c] in X by Th32;

        end;

        then

         A38: S[ 0 ];

        now

          let n be Nat such that

           A39: for a,b,c be Element of ( Fin CR) st ( card a) = n & [a, b] in X & [b, c] in X holds [a, c] in X;

          let a,b,c be Element of ( Fin CR) such that

           A40: ( card a) = (n + 1) and

           A41: [a, b] in X and

           A42: [b, c] in X;

          per cases by A41, Th32;

            suppose a = {} ;

            hence [a, c] in X by Th32;

          end;

            suppose

             A43: a <> {} & b <> {} & ( PosetMax a) <> ( PosetMax b) & [( PosetMax a), ( PosetMax b)] in IR;

            now

              per cases by A42, Th32;

                suppose b = {} ;

                hence [a, c] in X by A43;

              end;

                suppose

                 A44: b <> {} & c <> {} & ( PosetMax b) <> ( PosetMax c) & [( PosetMax b), ( PosetMax c)] in IR;

                then

                 A45: [( PosetMax a), ( PosetMax c)] in IR by A43, ORDERS_1: 5;

                now

                  per cases ;

                    suppose ( PosetMax a) <> ( PosetMax c);

                    hence [a, c] in X by A43, A44, A45, Th32;

                  end;

                    suppose ( PosetMax a) = ( PosetMax c);

                    hence [a, c] in X by A43, A44, ORDERS_1: 4;

                  end;

                end;

                hence [a, c] in X;

              end;

                suppose b <> {} & c <> {} & ( PosetMax b) = ( PosetMax c) & [(b \ {( PosetMax b)}), (c \ {( PosetMax c)})] in ( union ( rng FOAR));

                hence [a, c] in X by A43, Th32;

              end;

            end;

            hence [a, c] in X;

          end;

            suppose

             A46: a <> {} & b <> {} & ( PosetMax a) = ( PosetMax b) & [(a \ {( PosetMax a)}), (b \ {( PosetMax b)})] in ( union ( rng FOAR));

            now

              per cases by A42, Th32;

                suppose b = {} ;

                hence [a, c] in X by A46;

              end;

                suppose b <> {} & c <> {} & ( PosetMax b) <> ( PosetMax c) & [( PosetMax b), ( PosetMax c)] in IR;

                hence [a, c] in X by A46, Th32;

              end;

                suppose

                 A47: b <> {} & c <> {} & ( PosetMax b) = ( PosetMax c) & [(b \ {( PosetMax b)}), (c \ {( PosetMax c)})] in ( union ( rng FOAR));

                set z = (a \ {( PosetMax a)});

                reconsider z as Element of ( Fin CR) by Th34;

                

                 A48: ( card z) = n by A40, Lm1;

                

                 A49: c c= CR by FINSUB_1:def 5;

                reconsider c9 = c as finite set;

                set zc = (c9 \ {( PosetMax c)});

                zc c= CR by A49;

                then

                reconsider zc as Element of ( Fin CR) by FINSUB_1:def 5;

                

                 A50: b c= CR by FINSUB_1:def 5;

                reconsider b9 = b as finite set;

                set zb = (b9 \ {( PosetMax b)});

                zb c= CR by A50;

                then

                reconsider zb as Element of ( Fin CR) by FINSUB_1:def 5;

                 [z, zb] in ( union ( rng FOAR)) by A46;

                then [z, zc] in ( union ( rng FOAR)) by A39, A47, A48;

                hence [a, c] in X by A46, A47, Th32;

              end;

            end;

            hence [a, c] in X;

          end;

        end;

        then

         A51: for n be Nat st S[n] holds S[(n + 1)];

        

         A52: for n be Nat holds S[n] from NAT_1:sch 2( A38, A51);

        reconsider x9 = x as Element of ( Fin CR) by A32;

        reconsider xx = x as set by TARSKI: 1;

        ( card x9) = ( card xx);

        hence [x, z] in X by A33, A34, A35, A36, A52;

      end;

      

       A53: X is_reflexive_in ( Fin CR) by A3;

      

       A54: X is_antisymmetric_in ( Fin CR) by A12;

      

       A55: X is_transitive_in ( Fin CR) by A31;

      reconsider R = ( union ( rng FOAR)) as Relation of ( Fin CR) by A3;

      

       A56: ( dom R) = ( Fin CR) by A53, ORDERS_1: 13;

      ( field R) = ( Fin CR) by A53, ORDERS_1: 13;

      hence thesis by A53, A54, A55, A56, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

    end;

    definition

      let R be connected non empty Poset;

      :: BAGORDER:def15

      func FinOrd R -> Order of ( Fin the carrier of R) equals ( union ( rng ( FinOrd-Approx R)));

      coherence by Th35;

    end

    definition

      let R be connected non empty Poset;

      :: BAGORDER:def16

      func FinPoset R -> Poset equals RelStr (# ( Fin the carrier of R), ( FinOrd R) #);

      correctness ;

    end

    registration

      let R be connected non empty Poset;

      cluster ( FinPoset R) -> non empty;

      correctness ;

    end

    theorem :: BAGORDER:39

    

     Th36: for R be connected non empty Poset, a,b be Element of ( FinPoset R) holds [a, b] in the InternalRel of ( FinPoset R) iff ex x,y be Element of ( Fin the carrier of R) st a = x & b = y & (x = {} or x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in the InternalRel of R or x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( FinOrd R))

    proof

      let R be connected non empty Poset, a,b be Element of ( FinPoset R);

      set CR = the carrier of R;

      reconsider x = a, y = b as Element of ( Fin CR);

      hereby

        assume

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

        take x, y;

        thus a = x & b = y;

        thus x = {} or x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in the InternalRel of R or x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( FinOrd R) by A1, Th32;

      end;

      assume ex x,y be Element of ( Fin the carrier of R) st a = x & b = y & (x = {} or x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in the InternalRel of R or x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( FinOrd R));

      hence thesis by Th32;

    end;

    registration

      let R be connected non empty Poset;

      cluster ( FinPoset R) -> connected;

      correctness

      proof

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

        set FIR = ( FinOrd R), FCR = ( Fin CR);

        

         A1: ( FinPoset R) = RelStr (# FCR, FIR #);

        now

          let x,y be Element of ( FinPoset R);

          reconsider x9 = x, y9 = y as Element of ( Fin CR);

          defpred P[ Nat] means (for x,y be Element of ( Fin CR) st ( card x) = $1 holds ( [x, y] in FIR or [y, x] in FIR));

          now

            let a,b be Element of ( Fin CR);

            assume ( card a) = 0 ;

            then a = {} ;

            hence [a, b] in FIR or [a, b] in FIR by A1, Th36;

          end;

          then

           A2: P[ 0 ];

          now

            let n be Nat such that

             A3: for x,y be Element of ( Fin CR) st ( card x) = n holds ( [x, y] in FIR or [y, x] in FIR);

            let a,b be Element of ( Fin CR) such that

             A4: ( card a) = (n + 1);

            per cases ;

              suppose a = {} ;

              hence [a, b] in FIR or [b, a] in FIR by A1, Th36;

            end;

              suppose

               A5: a <> {} ;

              now

                per cases ;

                  suppose b = {} ;

                  hence [a, b] in FIR or [b, a] in FIR by A1, Th36;

                end;

                  suppose

                   A6: b <> {} ;

                  now

                    per cases ;

                      suppose

                       A7: ( PosetMax a) <> ( PosetMax b);

                      now

                        per cases by WAYBEL_0:def 29;

                          suppose ( PosetMax a) <= ( PosetMax b);

                          then [( PosetMax a), ( PosetMax b)] in IR by ORDERS_2:def 5;

                          hence [a, b] in FIR or [b, a] in FIR by A1, A5, A6, A7, Th36;

                        end;

                          suppose ( PosetMax b) <= ( PosetMax a);

                          then [( PosetMax b), ( PosetMax a)] in IR by ORDERS_2:def 5;

                          hence [a, b] in FIR or [b, a] in FIR by A1, A5, A6, A7, Th36;

                        end;

                      end;

                      hence [a, b] in FIR or [b, a] in FIR;

                    end;

                      suppose

                       A8: ( PosetMax a) = ( PosetMax b);

                      set ax = (a \ {( PosetMax a)}), bx = (b \ {( PosetMax b)});

                      

                       A9: ( card ax) = n by A4, Lm1;

                      reconsider ax, bx as Element of ( Fin CR) by Th34;

                      now

                        per cases by A3, A9;

                          suppose [ax, bx] in FIR;

                          hence [a, b] in FIR or [b, a] in FIR by A1, A5, A6, A8, Th36;

                        end;

                          suppose [bx, ax] in FIR;

                          hence [a, b] in FIR or [b, a] in FIR by A1, A5, A6, A8, Th36;

                        end;

                      end;

                      hence [a, b] in FIR or [b, a] in FIR;

                    end;

                  end;

                  hence [a, b] in FIR or [b, a] in FIR;

                end;

              end;

              hence [a, b] in FIR or [b, a] in FIR;

            end;

          end;

          then

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

          

           A11: for n be Nat holds P[n] from NAT_1:sch 2( A2, A10);

          ( card x9) = ( card x);

          then [x9, y9] in FIR or [y9, x9] in FIR by A11;

          hence x <= y or y <= x by ORDERS_2:def 5;

        end;

        hence thesis by WAYBEL_0:def 29;

      end;

    end

    definition

      let R be connected non empty RelStr, C be non empty set;

      :: BAGORDER:def17

      func MinElement (C,R) -> Element of R means

      : Def17: it in C & it is_minimal_wrt (C,the InternalRel of R);

      existence

      proof

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

        IR is_well_founded_in CR by A1;

        then

        consider a0 be object such that

         A3: a0 in C and

         A4: (IR -Seg a0) misses C by A2, WELLORD1:def 3;

        reconsider a0 as Element of R by A2, A3;

        take a0;

        thus a0 in C by A3;

        thus thesis by A3, A4, DICKSON: 6;

      end;

      uniqueness

      proof

        let IT1,IT2 be Element of R such that

         A5: IT1 in C and

         A6: IT1 is_minimal_wrt (C,the InternalRel of R) and

         A7: IT2 in C and

         A8: IT2 is_minimal_wrt (C,the InternalRel of R);

        set IR = the InternalRel of R;

        assume

         A9: IT1 <> IT2;

        per cases by WAYBEL_0:def 29;

          suppose IT1 <= IT2;

          then [IT1, IT2] in IR by ORDERS_2:def 5;

          then IT1 in (IR -Seg IT2) by A9, WELLORD1: 1;

          then IT1 in ((IR -Seg IT2) /\ C) by A5, XBOOLE_0:def 4;

          then (IR -Seg IT2) meets C by XBOOLE_0:def 7;

          hence contradiction by A8, DICKSON: 6;

        end;

          suppose IT2 <= IT1;

          then [IT2, IT1] in IR by ORDERS_2:def 5;

          then IT2 in (IR -Seg IT1) by A9, WELLORD1: 1;

          then IT2 in ((IR -Seg IT1) /\ C) by A7, XBOOLE_0:def 4;

          then (IR -Seg IT1) meets C by XBOOLE_0:def 7;

          hence contradiction by A6, DICKSON: 6;

        end;

      end;

    end

    theorem :: BAGORDER:40

    

     Th37: for R be non empty RelStr, s be sequence of R, j be Nat st s is descending holds (s ^\ j) is descending

    proof

      let R be non empty RelStr, s1 be sequence of R, j be Nat such that

       A1: s1 is descending;

      set s2 = (s1 ^\ j);

      set IR = the InternalRel of R;

      now

        let n be Nat;

        set nj = (n + j);

        

         A2: (s2 . n) = (s1 . nj) by NAT_1:def 3;

        

         A3: (s2 . (n + 1)) = (s1 . ((n + 1) + j)) by NAT_1:def 3

        .= (s1 . ((n + j) + 1));

        hence (s2 . (n + 1)) <> (s2 . n) by A1, A2;

        thus [(s2 . (n + 1)), (s2 . n)] in IR by A1, A2, A3;

      end;

      hence thesis;

    end;

    theorem :: BAGORDER:41

    for R be connected non empty Poset st R is well_founded holds ( FinPoset R) is well_founded

    proof

      let R be connected non empty Poset such that

       A1: R is well_founded;

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

      set FIR = ( FinOrd R), FCR = ( Fin CR);

      assume not ( FinPoset R) is well_founded;

      then

      consider A be sequence of ( FinPoset R) such that

       A2: A is descending by WELLFND1: 14;

      set zz = { z where z be sequence of ( FinPoset R) : z is descending };

      A in zz by A2;

      then

      reconsider zz as non empty set;

      set Z = [:CR, zz:];

      defpred S[ Nat, set, set] means ex Sn2 be sequence of ( FinPoset R), Smax be sequence of CR, an be Element of R, ix be Nat, bnt be sequence of ( FinPoset R), bn be sequence of ( FinPoset R) st Sn2 = ($2 `2 ) & (for i be Nat holds ex Sn2i be Element of ( Fin CR) st Sn2i = (Sn2 . i) & Sn2i <> {} & (Smax . i) = ( PosetMax Sn2i)) & an = ( MinElement (( rng Smax),R)) & ix = (Smax mindex an) & bnt = (Sn2 ^\ ix) & (for i be Nat holds (bn . i) = ((bnt . i) \ {an})) & (for i be Nat st ix <= i holds (Smax . i) = an) & $3 = [an, bn];

      

       A3: for n be Nat holds for Sn be Element of Z holds ex Sn1 be Element of Z st S[n, Sn, Sn1]

      proof

        let n be Nat, Sn be Element of Z;

        set Sn2 = (Sn `2 );

        Sn2 in zz;

        then

         A4: ex z be sequence of ( FinPoset R) st (z = Sn2) & (z is descending);

        then

        reconsider Sn2 as sequence of ( FinPoset R);

         A5:

        now

          let i be Nat;

          assume

           A6: (Sn2 . i) = {} ;

          

           A7: (Sn2 . (i + 1)) <> (Sn2 . i) by A4;

           [(Sn2 . (i + 1)), (Sn2 . i)] in FIR by A4;

          hence contradiction by A6, A7, Th33;

        end;

        defpred P[ Nat, set] means (ex Sn2i be Element of ( Fin CR) st Sn2i = (Sn2 . $1) & Sn2i <> {} & $2 = ( PosetMax Sn2i));

        

         A8: for i be Element of NAT holds ex y be Element of CR st P[i, y]

        proof

          let i be Element of NAT ;

          set Sn2i = (Sn2 . i);

          reconsider Sn2i as Element of ( Fin CR);

          set y = ( PosetMax Sn2i);

          take y;

          take Sn2i;

          thus Sn2i = (Sn2 . i);

          thus Sn2i <> {} by A5;

          thus thesis;

        end;

        consider Smax be sequence of CR such that

         A9: for i be Element of NAT holds P[i, (Smax . i)] from FUNCT_2:sch 3( A8);

        set an = ( MinElement (( rng Smax),R));

        set ix = (Smax mindex an);

        set bnt = (Sn2 ^\ ix);

        defpred R[ set, set] means (ex bni be Element of FCR st bni = ((bnt . $1) \ {an}) & $2 = bni);

        now

          let i be Nat;

          set bni = ((bnt . i) \ {an});

          reconsider k = (bnt . i) as finite Subset of CR by FINSUB_1:def 5;

          (k \ {an}) in FCR by FINSUB_1:def 5;

          then

          reconsider bni as Element of FCR;

          set y = bni;

          take y;

          take bni;

          thus bni = ((bnt . i) \ {an});

          thus y = bni;

        end;

        then

         A10: for i be Element of NAT holds ex y be Element of FCR st R[i, y];

        defpred P[ Nat] means (Smax . (ix + $1)) = an;

        

         A11: ( dom Smax) = NAT by FUNCT_2:def 1;

        

         A12: ( rng Smax) c= CR by RELAT_1:def 19;

        then

         A13: an in ( rng Smax) by A1, Def17;

        

         A14: an is_minimal_wrt (( rng Smax),IR) by A1, A12, Def17;

        

         A15: P[ 0 ] by A11, A13, DICKSON:def 11;

         A16:

        now

          let k be Nat such that

           A17: P[k];

          reconsider ixk = (ix + k) as Element of NAT by ORDINAL1:def 12;

          set ixk1 = (ix + (k + 1)), ixk19 = ((ix + k) + 1);

          consider Sn2ixk be Element of ( Fin CR) such that

           A18: Sn2ixk = (Sn2 . ixk) and Sn2ixk <> {} and

           A19: (Smax . ixk) = ( PosetMax Sn2ixk) by A9;

          consider Sn2ixk1 be Element of ( Fin CR) such that

           A20: Sn2ixk1 = (Sn2 . ixk1) and

           A21: Sn2ixk1 <> {} and

           A22: (Smax . ixk1) = ( PosetMax Sn2ixk1) by A9;

          reconsider Sn2ixk9 = Sn2ixk, Sn2ixk19 = Sn2ixk1 as Element of ( FinPoset R);

          ixk1 = ixk19;

          then [Sn2ixk19, Sn2ixk9] in FIR by A4, A18, A20;

          then

          consider x,y be Element of ( Fin CR) such that

           A23: Sn2ixk1 = x and

           A24: Sn2ixk = y and

           A25: x = {} or x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in IR or x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( FinOrd R) by Th36;

          per cases by A25;

            suppose x = {} ;

            hence P[(k + 1)] by A21, A23;

          end;

            suppose

             A26: x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in IR;

            (Smax . ixk1) in ( rng Smax) by A11, FUNCT_1:def 3;

            hence P[(k + 1)] by A14, A17, A19, A22, A23, A24, A26, WAYBEL_4:def 25;

          end;

            suppose x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( FinOrd R);

            hence P[(k + 1)] by A17, A19, A22, A23, A24;

          end;

        end;

        

         A27: for k be Nat holds P[k] from NAT_1:sch 2( A15, A16);

         A28:

        now

          let i be Nat;

          assume ix <= i;

          then

          consider k be Nat such that

           A29: i = (ix + k) by NAT_1: 10;

          reconsider k as Nat;

          i = (ix + k) by A29;

          hence (Smax . i) = an by A27;

        end;

         A30:

        now

          let i be Nat such that

           A31: ix <= i;

          reconsider i0 = i as Element of NAT by ORDINAL1:def 12;

          consider Sn2i be Element of ( Fin CR) such that

           A32: Sn2i = (Sn2 . i) and Sn2i <> {} and

           A33: (Smax . i0) = ( PosetMax Sn2i) by A9;

          take Sn2i;

          thus Sn2i = (Sn2 . i) by A32;

          thus ( PosetMax Sn2i) = an by A28, A31, A33;

        end;

         A34:

        now

          let i be Nat;

          set bnti = (bnt . i);

          reconsider bnti as Element of ( Fin CR);

          take bnti;

          thus bnti = (bnt . i);

          set iix = (i + ix);

          ex Sn2iix be Element of ( Fin CR) st (Sn2iix = (Sn2 . iix)) & (( PosetMax Sn2iix) = an) by A30, NAT_1: 11;

          hence ( PosetMax bnti) = an by NAT_1:def 3;

        end;

        consider bn be sequence of FCR such that

         A35: for i be Element of NAT holds R[i, (bn . i)] from FUNCT_2:sch 3( A10);

        reconsider bn as sequence of ( FinPoset R);

        set Sn1 = [an, bn];

        

         A36: bnt is descending by A4, Th37;

        now

          let i be Nat;

          reconsider i0 = i as Element of NAT by ORDINAL1:def 12;

          

           A37: ex bni be Element of FCR st (bni = ((bnt . i0) \ {an})) & ((bn . i0) = bni) by A35;

          

           A38: ex bni1 be Element of FCR st (bni1 = ((bnt . (i + 1)) \ {an})) & ((bn . (i + 1)) = bni1) by A35;

          reconsider bnti = (bnt . i), bnti1 = (bnt . (i + 1)) as Element of ( FinPoset R);

          reconsider bnti9 = bnti, bnti19 = bnti1 as Element of ( Fin CR);

          

           A39: bnti1 <> bnti by A36;

           [bnti1, bnti] in FIR by A36;

          then

          consider x,y be Element of ( Fin CR) such that

           A40: bnti1 = x and

           A41: bnti = y and

           A42: x = {} or x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in the InternalRel of R or x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( FinOrd R) by Th36;

           A43:

          now

            let i be Nat;

            (bnt . i) = (Sn2 . (i + ix)) by NAT_1:def 3;

            hence (bnt . i) <> {} by A5;

          end;

           A44:

          now

            

             A45: ex bnti99 be Element of ( Fin CR) st (bnti99 = (bnt . i)) & (( PosetMax bnti99) = an) by A34;

            ex bnti199 be Element of ( Fin CR) st (bnti199 = (bnt . (i + 1))) & (( PosetMax bnti199) = an) by A34;

            hence ( PosetMax bnti9) = an & ( PosetMax bnti19) = an by A45;

          end;

          

           A46: bnti9 <> {} by A43;

          

           A47: bnti19 <> {} by A43;

          

           A48: an in bnti by A44, A46, Def13;

          an in bnti1 by A44, A47, Def13;

          hence (bn . (i + 1)) <> (bn . i) by A37, A38, A39, A48, Th1;

          per cases by A42;

            suppose x = {} ;

            hence [(bn . (i + 1)), (bn . i)] in FIR by A40, A43;

          end;

            suppose x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in IR;

            hence [(bn . (i + 1)), (bn . i)] in FIR by A40, A41, A44;

          end;

            suppose x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( FinOrd R);

            hence [(bn . (i + 1)), (bn . i)] in FIR by A37, A38, A40, A41, A44;

          end;

        end;

        then bn is descending;

        then bn in zz;

        then

        reconsider Sn1 as Element of Z by ZFMISC_1:def 2;

        take Sn1, Sn2, Smax, an, ix, bnt, bn;

        thus Sn2 = (Sn `2 );

        thus for i be Nat holds ex Sn2i be Element of ( Fin CR) st Sn2i = (Sn2 . i) & Sn2i <> {} & (Smax . i) = ( PosetMax Sn2i)

        proof

          let i be Nat;

          reconsider i0 = i as Element of NAT by ORDINAL1:def 12;

          ex Sn2i be Element of ( Fin CR) st Sn2i = (Sn2 . i) & Sn2i <> {} & (Smax . i0) = ( PosetMax Sn2i) by A9;

          hence thesis;

        end;

        thus an = ( MinElement (( rng Smax),R));

        thus ix = (Smax mindex an);

        thus bnt = (Sn2 ^\ ix);

        now

          let i be Nat;

          reconsider i0 = i as Element of NAT by ORDINAL1:def 12;

          ex bni be Element of FCR st (bni = ((bnt . i0) \ {an})) & ((bn . i0) = bni) by A35;

          hence (bn . i) = ((bnt . i) \ {an});

        end;

        hence for i be Nat holds (bn . i) = ((bnt . i) \ {an});

        thus for i be Nat st ix <= i holds (Smax . i) = an by A28;

        thus thesis;

      end;

      set aStart = the Element of R;

      set SS = [aStart, A];

      A in zz by A2;

      then

      reconsider SS as Element of Z by ZFMISC_1:def 2;

      consider S01 be Element of Z, S02 be sequence of ( FinPoset R), S0max be sequence of CR, a0 be Element of R, i0 be Nat, b0t,b0 be sequence of ( FinPoset R) such that S02 = (SS `2 ) and

       A49: for i be Nat holds ex S02i be Element of ( Fin CR) st S02i = (S02 . i) & S02i <> {} & (S0max . i) = ( PosetMax S02i) and a0 = ( MinElement (( rng S0max),R)) and i0 = (S0max mindex a0) and

       A50: b0t = (S02 ^\ i0) and

       A51: for i be Nat holds (b0 . i) = ((b0t . i) \ {a0}) and

       A52: for i be Nat st i0 <= i holds (S0max . i) = a0 and

       A53: S01 = [a0, b0] by A3;

      consider S be sequence of Z such that

       A54: (S . 0 ) = S01 and

       A55: for n be Nat holds S[n, (S . n), (S . (n + 1))] from RECDEF_1:sch 2( A3);

      

       A56: for n be Nat holds S[n, (S . n), (S . (n + 1))] by A55;

      deffunc F( object) = ((S . $1) `1 );

       A57:

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider x9 = x as Nat;

        reconsider Sx = (S . x9) as Element of [:CR, zz:];

        (Sx `1 ) in CR;

        hence F(x) in CR;

      end;

      consider a be sequence of CR such that

       A58: for x be object st x in NAT holds (a . x) = F(x) from FUNCT_2:sch 2( A57);

      reconsider a as sequence of R;

      defpred PP[ Nat] means (for i be Nat holds (ex b be sequence of ( FinPoset R) st (b = ((S . $1) `2 )) & (for x be set st x in (b . i) holds x <> ((S . $1) `1 ) & [x, ((S . $1) `1 )] in IR)));

      

       A59: PP[ 0 ]

      proof

        let i be Nat;

        set b = ((S . 0 ) `2 );

        b in zz;

        then ex z be sequence of ( FinPoset R) st (z = b) & (z is descending);

        then

        reconsider b as sequence of ( FinPoset R);

        take b;

        thus b = ((S . 0 ) `2 );

        let x be set such that

         A60: x in (b . i);

        b0 = ( [a0, b0] `2 )

        .= b by A53, A54;

        then

         A61: x in ((b0t . i) \ {a0}) by A51, A60;

        then

         A62: x in (b0t . i);

         not x in {a0} by A61, XBOOLE_0:def 5;

        hence

         A63: x <> ((S . 0 ) `1 ) by A53, A54, TARSKI:def 1;

        (b . i) c= CR by FINSUB_1:def 5;

        then

        reconsider x9 = x as Element of R by A60;

        

         A64: x in (S02 . (i + i0)) by A50, A62, NAT_1:def 3;

        consider S02ib be Element of ( Fin CR) such that

         A65: S02ib = (S02 . (i + i0)) and

         A66: S02ib <> {} and

         A67: (S0max . (i + i0)) = ( PosetMax S02ib) by A49;

        ( PosetMax S02ib) = a0 by A52, A67, NAT_1: 11;

        then a0 is_maximal_wrt (S02ib,IR) by A66, Def13;

        then not [a0, x] in IR by A63, A64, A65, A53, A54, WAYBEL_4:def 23;

        then not a0 <= x9 by ORDERS_2:def 5;

        then x9 <= a0 by WAYBEL_0:def 29;

        hence thesis by A53, A54, ORDERS_2:def 5;

      end;

      

       A68: for n be Nat st PP[n] holds PP[(n + 1)]

      proof

        let n be Nat;

        assume PP[n];

        let i be Nat;

        set n1 = (n + 1);

        reconsider n1 as Nat;

        set b = ((S . n1) `2 );

        consider Sn2 be sequence of ( FinPoset R), Smax be sequence of CR, an be Element of R, ix be Nat, bnt,bn be sequence of ( FinPoset R) such that Sn2 = ((S . n) `2 ) and

         A69: for i be Nat holds ex Sn2i be Element of ( Fin CR) st Sn2i = (Sn2 . i) & Sn2i <> {} & (Smax . i) = ( PosetMax Sn2i) and an = ( MinElement (( rng Smax),R)) and ix = (Smax mindex an) and

         A70: bnt = (Sn2 ^\ ix) and

         A71: for i be Nat holds (bn . i) = ((bnt . i) \ {an}) and

         A72: for i be Nat st ix <= i holds (Smax . i) = an and

         A73: (S . (n + 1)) = [an, bn] by A56;

        b in zz;

        then ex z be sequence of ( FinPoset R) st (z = b) & (z is descending);

        then

        reconsider b as sequence of ( FinPoset R);

        take b;

        thus b = ((S . (n + 1)) `2 );

        let x be set such that

         A74: x in (b . i);

        bn = ( [an, bn] `2 )

        .= b by A73;

        then

         A75: x in ((bnt . i) \ {an}) by A71, A74;

        then

         A76: x in (bnt . i);

         not x in {an} by A75, XBOOLE_0:def 5;

        hence

         A77: x <> ((S . (n + 1)) `1 ) by A73, TARSKI:def 1;

        (b . i) c= CR by FINSUB_1:def 5;

        then

        reconsider x9 = x as Element of R by A74;

        

         A78: x in (Sn2 . (i + ix)) by A70, A76, NAT_1:def 3;

        consider Sn2ib be Element of ( Fin CR) such that

         A79: Sn2ib = (Sn2 . (i + ix)) and

         A80: Sn2ib <> {} and

         A81: (Smax . (i + ix)) = ( PosetMax Sn2ib) by A69;

        ( PosetMax Sn2ib) = an by A72, A81, NAT_1: 11;

        then an is_maximal_wrt (Sn2ib,IR) by A80, Def13;

        then not [an, x] in IR by A77, A78, A79, A73, WAYBEL_4:def 23;

        then not an <= x9 by ORDERS_2:def 5;

        then x9 <= an by WAYBEL_0:def 29;

        hence thesis by A73, ORDERS_2:def 5;

      end;

      

       A82: for n be Nat holds PP[n] from NAT_1:sch 2( A59, A68);

      defpred P3[ Nat] means (ex b be sequence of ( FinPoset R), i be Nat st b = ((S . $1) `2 ) & (a . ($1 + 1)) in (b . i));

      

       A83: P3[ 0 ]

      proof

        set b = ((S . 0 ) `2 );

        b in zz;

        then ex z be sequence of ( FinPoset R) st (z = b) & (z is descending);

        then

        reconsider b as sequence of ( FinPoset R);

        take b;

        

         A84: (a . ( 0 qua Nat + 1)) = ((S . ( 0 qua Nat + 1)) `1 ) by A58;

        consider S12 be sequence of ( FinPoset R), S1max be sequence of CR, a1 be Element of R, i1 be Nat, b1t,b1 be sequence of ( FinPoset R) such that

         A85: S12 = ((S . 0 ) `2 ) and

         A86: for i be Nat holds ex S12i be Element of ( Fin CR) st S12i = (S12 . i) & S12i <> {} & (S1max . i) = ( PosetMax S12i) and

         A87: a1 = ( MinElement (( rng S1max),R)) and i1 = (S1max mindex a1) and b1t = (S12 ^\ i1) and for i be Nat holds (b1 . i) = ((b1t . i) \ {a1}) and for i be Nat st i1 <= i holds (S1max . i) = a1 and

         A88: (S . ( 0 qua Nat + 1)) = [a1, b1] by A55;

        ( rng S1max) c= CR by RELAT_1:def 19;

        then a1 in ( rng S1max) by A1, A87, Def17;

        then

        consider i be object such that

         A89: i in ( dom S1max) and

         A90: (S1max . i) = a1 by FUNCT_1:def 3;

        

         A91: ex S12i be Element of ( Fin CR) st (S12i = (S12 . i)) & (S12i <> {} ) & ((S1max . i) = ( PosetMax S12i)) by A86, A89;

        reconsider i as Nat by A89;

        take i;

        thus b = ((S . 0 ) `2 );

        

         A92: a1 in (b . i) by A85, A90, A91, Def13;

        thus (a . ( 0 qua Nat + 1)) in (b . i) by A84, A88, A92;

      end;

      

       A93: for n be Nat st P3[n] holds P3[(n + 1)]

      proof

        let n be Nat;

        assume P3[n];

        set b = ((S . (n + 1)) `2 );

        b in zz;

        then ex z be sequence of ( FinPoset R) st (z = b) & (z is descending);

        then

        reconsider b as sequence of ( FinPoset R);

        take b;

        set n1 = (n + 1);

        reconsider n1 as Nat;

        consider Sn12 be sequence of ( FinPoset R), Sn1max be sequence of CR, an1 be Element of R, in1 be Nat, bn1t,bn1 be sequence of ( FinPoset R) such that

         A94: Sn12 = ((S . n1) `2 ) and

         A95: for i be Nat holds ex Sn12i be Element of ( Fin CR) st Sn12i = (Sn12 . i) & Sn12i <> {} & (Sn1max . i) = ( PosetMax Sn12i) and

         A96: an1 = ( MinElement (( rng Sn1max),R)) and in1 = (Sn1max mindex an1) and bn1t = (Sn12 ^\ in1) and for i be Nat holds (bn1 . i) = ((bn1t . i) \ {an1}) and for i be Nat st in1 <= i holds (Sn1max . i) = an1 and

         A97: (S . (n1 + 1)) = [an1, bn1] by A55;

        ( rng Sn1max) c= CR by RELAT_1:def 19;

        then an1 in ( rng Sn1max) by A1, A96, Def17;

        then

        consider i be object such that

         A98: i in ( dom Sn1max) and

         A99: (Sn1max . i) = an1 by FUNCT_1:def 3;

        

         A100: ex Sn12i be Element of ( Fin CR) st (Sn12i = (Sn12 . i)) & (Sn12i <> {} ) & ((Sn1max . i) = ( PosetMax Sn12i)) by A95, A98;

        reconsider i as Nat by A98;

        take i;

        thus b = ((S . (n + 1)) `2 );

        

         A101: an1 in (b . i) by A94, A99, A100, Def13;

        ( [an1, bn1] `1 ) = an1;

        hence thesis by A58, A101, A97;

      end;

      

       A102: for n be Nat holds P3[n] from NAT_1:sch 2( A83, A93);

      defpred P4[ Nat] means ((a . ($1 + 1)) <> (a . $1) & [(a . ($1 + 1)), (a . $1)] in IR);

      

       A103: P4[ 0 ]

      proof

        

         A104: (a . 0 ) = ((S . 0 ) `1 ) by A58;

        consider b be sequence of ( FinPoset R), i be Nat such that

         A105: b = ((S . 0 ) `2 ) and

         A106: (a . ( 0 qua Nat + 1)) in (b . i) by A83;

        ex bb be sequence of ( FinPoset R) st (bb = ((S . 0 ) `2 )) & (for x be set st x in (bb . i) holds x <> ((S . 0 ) `1 ) & [x, ((S . 0 ) `1 )] in IR) by A59;

        hence (a . ( 0 qua Nat + 1)) <> (a . 0 ) & [(a . ( 0 qua Nat + 1)), (a . 0 )] in IR by A104, A105, A106;

      end;

      

       A107: for n be Nat st P4[n] holds P4[(n + 1)]

      proof

        let n be Nat;

        assume that (a . (n + 1)) <> (a . n) and [(a . (n + 1)), (a . n)] in IR;

        

         A108: (a . (n + 1)) = ((S . (n + 1)) `1 ) by A58;

        consider b be sequence of ( FinPoset R), i be Nat such that

         A109: b = ((S . (n + 1)) `2 ) and

         A110: (a . ((n + 1) + 1)) in (b . i) by A102;

        ex bb be sequence of ( FinPoset R) st (bb = ((S . (n + 1)) `2 )) & (for x be set st x in (bb . i) holds x <> ((S . (n + 1)) `1 ) & [x, ((S . (n + 1)) `1 )] in IR) by A82;

        hence thesis by A108, A109, A110;

      end;

      for n be Nat holds P4[n] from NAT_1:sch 2( A103, A107);

      then a is descending;

      hence contradiction by A1, WELLFND1: 14;

    end;