orders_4.miz



    begin

    definition

      :: ORDERS_4:def1

      mode Chain -> RelStr means

      : Def1: it is connected non empty Poset or it is empty;

      existence

      proof

        set R = the empty RelStr;

        take R;

        thus thesis;

      end;

    end

    registration

      cluster empty -> reflexive transitive antisymmetric for RelStr;

      coherence

      proof

        let A be RelStr;

        assume

         A1: A is empty;

        then for x,y,z be object holds x in the carrier of A & y in the carrier of A & z in the carrier of A & [x, y] in the InternalRel of A & [y, z] in the InternalRel of A implies [x, z] in the InternalRel of A;

        then

         A2: the InternalRel of A is_transitive_in the carrier of A by RELAT_2:def 8;

        for x,y be object holds x in the carrier of A & y in the carrier of A & [x, y] in the InternalRel of A & [y, x] in the InternalRel of A implies x = y by A1;

        then

         A3: the InternalRel of A is_antisymmetric_in the carrier of A by RELAT_2:def 4;

        for x be object holds x in the carrier of A implies [x, x] in the InternalRel of A by A1;

        then the InternalRel of A is_reflexive_in the carrier of A by RELAT_2:def 1;

        hence thesis by A2, A3, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;

      end;

    end

    registration

      cluster -> reflexive transitive antisymmetric for Chain;

      coherence

      proof

        let A be Chain;

        A is connected non empty Poset or A is empty RelStr by Def1;

        hence thesis;

      end;

    end

    registration

      cluster non empty for Chain;

      existence

      proof

        set A = the trivial reflexive transitive antisymmetric non empty RelStr;

        A is Chain by Def1;

        hence thesis;

      end;

    end

    registration

      cluster -> connected for non empty Chain;

      coherence by Def1;

    end

    definition

      let L be 1-sorted;

      :: ORDERS_4:def2

      attr L is countable means the carrier of L is countable;

    end

    registration

      cluster finite non empty for Chain;

      existence

      proof

        set A = the trivial reflexive transitive antisymmetric non empty finite RelStr;

        A is Chain by Def1;

        hence thesis;

      end;

    end

    registration

      cluster countable for Chain;

      existence

      proof

        set L = the finite Chain;

        take L;

        the carrier of L is countable by CARD_4: 1;

        hence thesis;

      end;

    end

    registration

      let A be connected non empty RelStr;

      cluster full -> connected for non empty SubRelStr of A;

      correctness

      proof

        let S be non empty SubRelStr of A;

        assume

         A1: S is full;

        for x,y be Element of S holds x <= y or y <= x

        proof

          let x,y be Element of S;

          

           A2: the carrier of S c= the carrier of A by YELLOW_0:def 13;

          reconsider b = y as Element of A by A2;

          reconsider a = x as Element of A by A2;

          a <= b or b <= a by WAYBEL_0:def 29;

          hence thesis by A1, YELLOW_0: 60;

        end;

        hence thesis by WAYBEL_0:def 29;

      end;

    end

    registration

      let A be finite RelStr;

      cluster -> finite for SubRelStr of A;

      correctness

      proof

        let S be SubRelStr of A;

        the carrier of S c= the carrier of A by YELLOW_0:def 13;

        hence thesis;

      end;

    end

    theorem :: ORDERS_4:1

    

     Th1: for n,m be Nat holds n <= m implies ( InclPoset n) is full SubRelStr of ( InclPoset m)

    proof

      let n,m be Nat;

      

       A1: the InternalRel of ( InclPoset m) = ( RelIncl m) by YELLOW_1: 1;

      assume n <= m;

      then

       A2: ( Segm n) c= ( Segm m) by NAT_1: 39;

      

       A3: ( RelIncl n) c= ( RelIncl m)

      proof

        let x be object;

        assume x in ( RelIncl n);

        then x in (( RelIncl m) |_2 n) by A2, WELLORD2: 7;

        hence thesis by XBOOLE_0:def 4;

      end;

      the carrier of ( InclPoset m) = m by YELLOW_1: 1;

      then

       A4: the carrier of ( InclPoset n) c= the carrier of ( InclPoset m) by A2, YELLOW_1: 1;

      

       A5: the InternalRel of ( InclPoset n) = ( RelIncl n) by YELLOW_1: 1;

      then (( RelIncl m) |_2 n) = the InternalRel of ( InclPoset n) by A2, WELLORD2: 7;

      then the InternalRel of ( InclPoset n) = (the InternalRel of ( InclPoset m) |_2 the carrier of ( InclPoset n)) by A1, YELLOW_1: 1;

      hence thesis by A4, A5, A1, A3, YELLOW_0:def 13, YELLOW_0:def 14;

    end;

    definition

      let L be RelStr;

      let A,B be set;

      :: ORDERS_4:def3

      pred A,B form_upper_lower_partition_of L means (A \/ B) = the carrier of L & for a,b be Element of L st a in A & b in B holds a < b;

    end

    theorem :: ORDERS_4:2

    

     Th2: for L be RelStr holds for A,B be set holds (A,B) form_upper_lower_partition_of L implies A misses B

    proof

      let L be RelStr;

      let A,B be set;

      assume that

       A1: (A,B) form_upper_lower_partition_of L and

       A2: A meets B;

      consider x be object such that

       A3: x in (A /\ B) by A2, XBOOLE_0: 4;

      

       A4: x in B by A3, XBOOLE_0:def 4;

      

       A5: x in A by A3, XBOOLE_0:def 4;

      (A \/ B) = the carrier of L by A1;

      then

      reconsider x as Element of L by A5, XBOOLE_0:def 3;

      x < x by A1, A5, A4;

      hence contradiction;

    end;

    theorem :: ORDERS_4:3

    

     Th3: for L be upper-bounded antisymmetric non empty RelStr holds ((the carrier of L \ {( Top L)}), {( Top L)}) form_upper_lower_partition_of L

    proof

      let L be upper-bounded antisymmetric non empty RelStr;

      

       A1: for a,b be Element of L st a in (the carrier of L \ {( Top L)}) & b in {( Top L)} holds a < b

      proof

        let a,b be Element of L;

        assume that

         A2: a in (the carrier of L \ {( Top L)}) and

         A3: b in {( Top L)};

         not a in {( Top L)} by A2, XBOOLE_0:def 5;

        then

         A4: a <> ( Top L) by TARSKI:def 1;

        

         A5: a <= ( Top L) by YELLOW_0: 45;

        b = ( Top L) by A3, TARSKI:def 1;

        hence thesis by A4, A5, ORDERS_2:def 6;

      end;

      ((the carrier of L \ {( Top L)}) \/ {( Top L)}) = the carrier of L by XBOOLE_1: 45;

      hence thesis by A1;

    end;

    theorem :: ORDERS_4:4

    

     Th4: for L1,L2 be RelStr holds for f be Function of L1, L2 st f is isomorphic holds (the carrier of L1 <> {} iff the carrier of L2 <> {} ) & (the carrier of L2 <> {} or the carrier of L1 = {} ) & (the carrier of L1 = {} iff the carrier of L2 = {} )

    proof

      let L1,L2 be RelStr;

      let f be Function of L1, L2 such that

       A1: f is isomorphic;

      the carrier of L1 = {} iff the carrier of L2 = {}

      proof

        hereby

          assume the carrier of L1 = {} ;

          then L1 is empty;

          then L2 is empty by A1, WAYBEL_0:def 38;

          hence the carrier of L2 = {} ;

        end;

        assume the carrier of L2 = {} ;

        then L2 is empty;

        then L1 is empty by A1, WAYBEL_0:def 38;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ORDERS_4:5

    

     Th5: for L1,L2 be antisymmetric RelStr holds for A1,B1 be Subset of L1 st (A1,B1) form_upper_lower_partition_of L1 holds for A2,B2 be Subset of L2 st (A2,B2) form_upper_lower_partition_of L2 holds for f be Function of ( subrelstr A1), ( subrelstr A2) st f is isomorphic holds for g be Function of ( subrelstr B1), ( subrelstr B2) st g is isomorphic holds ex h be Function of L1, L2 st h = (f +* g) & h is isomorphic

    proof

      let L1,L2 be antisymmetric RelStr;

      let A1,B1 be Subset of L1 such that

       A1: (A1,B1) form_upper_lower_partition_of L1;

      

       A2: (A1 \/ B1) = the carrier of L1 by A1;

      let A2,B2 be Subset of L2 such that

       A3: (A2,B2) form_upper_lower_partition_of L2;

      

       A4: A2 misses B2 by A3, Th2;

      

       A5: (A2 \/ B2) = the carrier of L2 by A3;

      

       A6: A1 misses B1 by A1, Th2;

      let f be Function of ( subrelstr A1), ( subrelstr A2) such that

       A7: f is isomorphic;

      let g be Function of ( subrelstr B1), ( subrelstr B2) such that

       A8: g is isomorphic;

      set h = (f +* g);

      per cases ;

        suppose

         A9: the carrier of L1 = {} ;

        then

         A10: A1 = {} by A2;

        then the carrier of ( subrelstr A1) = {} by YELLOW_0:def 15;

        then ( dom f) = the carrier of ( subrelstr A1);

        then

         A11: ( dom f) = A1 by YELLOW_0:def 15;

        ( subrelstr A1) is empty by A10, YELLOW_0:def 15;

        then ( subrelstr A2) is empty by A7, WAYBEL_0:def 38;

        then

         A12: A2 = {} by YELLOW_0:def 15;

        

         A13: for x be object st x in the carrier of L1 holds (h . x) in the carrier of L2 by A9;

        

         A14: B1 = {} by A2, A9;

        then the carrier of ( subrelstr B2) <> {} or the carrier of ( subrelstr B1) = {} by YELLOW_0:def 15;

        then ( dom g) = the carrier of ( subrelstr B1) by FUNCT_2:def 1;

        then ( dom g) = B1 by YELLOW_0:def 15;

        then ( dom h) = the carrier of L1 by A2, A11, FUNCT_4:def 1;

        then

        reconsider h as Function of L1, L2 by A13, FUNCT_2: 3;

        

         A15: L1 is empty by A9;

        ( subrelstr B1) is empty by A14, YELLOW_0:def 15;

        then L2 is empty by A8, A5, A12, WAYBEL_0:def 38;

        then h is isomorphic by A15, WAYBEL_0:def 38;

        hence thesis;

      end;

        suppose

         A16: the carrier of L1 <> {} ;

        then A1 <> {} or B1 <> {} by A2;

        then ( subrelstr A1) is non empty or ( subrelstr B1) is non empty by YELLOW_0:def 15;

        then

         A17: ( subrelstr A2) is non empty or ( subrelstr B2) is non empty by A7, A8, WAYBEL_0:def 38;

        (A2 <> {} or B2 <> {} ) implies (B2 <> {} or B1 = {} )

        proof

          assume A2 <> {} or B2 <> {} ;

          the carrier of ( subrelstr B2) <> {} or the carrier of ( subrelstr B1) = {} by A8, Th4;

          hence thesis by YELLOW_0:def 15;

        end;

        then

         A18: the carrier of ( subrelstr B2) <> {} or the carrier of ( subrelstr B1) = {} by A17, YELLOW_0:def 15;

        then

         A19: ( dom g) = the carrier of ( subrelstr B1) by FUNCT_2:def 1;

        then

         A20: ( dom g) = B1 by YELLOW_0:def 15;

        (A1 <> {} or B1 <> {} ) implies (A2 <> {} or A1 = {} )

        proof

          assume A1 <> {} or B1 <> {} ;

          the carrier of ( subrelstr A2) <> {} or the carrier of ( subrelstr A1) = {} by A7, Th4;

          hence thesis by YELLOW_0:def 15;

        end;

        then the carrier of ( subrelstr A2) <> {} or the carrier of ( subrelstr A1) = {} by YELLOW_0:def 15;

        then ( dom f) = the carrier of ( subrelstr A1) by FUNCT_2:def 1;

        then

         A21: ( dom f) = A1 by YELLOW_0:def 15;

        

         A22: ( dom h) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1;

        

         A23: ( dom f) misses ( dom g) implies ( rng h) = (( rng f) \/ ( rng g))

        proof

          assume

           A24: ( dom f) misses ( dom g);

          

           A25: (( rng f) \/ ( rng g)) c= ( rng h)

          proof

            let x be object;

            assume

             A26: x in (( rng f) \/ ( rng g));

            per cases by A26, XBOOLE_0:def 3;

              suppose x in ( rng f);

              then

              consider z be object such that

               A27: z in ( dom f) and

               A28: x = (f . z) by FUNCT_1:def 3;

               not z in ( dom g) by A24, A27, XBOOLE_0: 3;

              then

               A29: x = (h . z) by A28, FUNCT_4: 11;

              z in ( dom h) by A22, A27, XBOOLE_0:def 3;

              hence thesis by A29, FUNCT_1:def 3;

            end;

              suppose x in ( rng g);

              then

              consider z be object such that

               A30: z in ( dom g) and

               A31: x = (g . z) by FUNCT_1:def 3;

              z in ( dom h) & (h . z) = (g . z) by A22, A30, FUNCT_4: 13, XBOOLE_0:def 3;

              hence thesis by A31, FUNCT_1:def 3;

            end;

          end;

          ( rng h) c= (( rng f) \/ ( rng g)) by FUNCT_4: 17;

          hence thesis by A25, XBOOLE_0:def 10;

        end;

        

         A32: ( rng h) = the carrier of L2

        proof

          per cases ;

            suppose

             A33: A2 = {} & A1 = {} ;

            then ( subrelstr B1) is non empty by A2, A16, YELLOW_0:def 15;

            then

             A34: ( rng g) = the carrier of ( subrelstr B2) by A8, A17, A33, WAYBEL_0: 66, YELLOW_0:def 15;

            ( rng f) = {} by A21, A33, RELAT_1: 42;

            hence thesis by A5, A21, A23, A33, A34, XBOOLE_1: 65, YELLOW_0:def 15;

          end;

            suppose A2 = {} & A1 <> {} ;

            then the carrier of ( subrelstr A2) = {} & the carrier of ( subrelstr A1) <> {} by YELLOW_0:def 15;

            hence thesis by A7, Th4;

          end;

            suppose A2 <> {} & A1 = {} ;

            then the carrier of ( subrelstr A2) <> {} & the carrier of ( subrelstr A1) = {} by YELLOW_0:def 15;

            hence thesis by A7, Th4;

          end;

            suppose

             A35: A2 <> {} & A1 <> {} ;

            ( rng h) = the carrier of L2

            proof

              per cases ;

                suppose

                 A36: B2 <> {} ;

                then the carrier of ( subrelstr B2) <> {} by YELLOW_0:def 15;

                then the carrier of ( subrelstr B1) <> {} by A8, Th4;

                then

                 A37: ( subrelstr B1) is non empty;

                ( subrelstr A2) is non empty & ( subrelstr A1) is non empty by A35, YELLOW_0:def 15;

                then ( rng f) = the carrier of ( subrelstr A2) by A7, WAYBEL_0: 66;

                then

                 A38: ( rng f) = A2 by YELLOW_0:def 15;

                ( subrelstr B2) is non empty by A36, YELLOW_0:def 15;

                then ( rng g) = the carrier of ( subrelstr B2) by A8, A37, WAYBEL_0: 66;

                hence thesis by A1, A5, A21, A20, A23, A38, Th2, YELLOW_0:def 15;

              end;

                suppose

                 A39: B2 = {} ;

                ( subrelstr A2) is non empty & ( subrelstr A1) is non empty by A35, YELLOW_0:def 15;

                then

                 A40: ( rng f) = the carrier of ( subrelstr A2) by A7, WAYBEL_0: 66;

                g = {} by A18, A39, YELLOW_0:def 15;

                hence thesis by A5, A23, A39, A40, RELAT_1: 38, XBOOLE_1: 65, YELLOW_0:def 15;

              end;

            end;

            hence thesis;

          end;

        end;

        

         A41: ( dom h) = the carrier of L1 by A2, A21, A19, A22, YELLOW_0:def 15;

        then

         A42: for x be object st x in the carrier of L1 holds (h . x) in the carrier of L2 by A32, FUNCT_1:def 3;

        A2 <> {} or B2 <> {} by A17, YELLOW_0:def 15;

        then

        reconsider L2 as non empty RelStr by A5;

        reconsider L1 as non empty RelStr by A16;

        reconsider h as Function of L1, L2 by A41, A42, FUNCT_2: 3;

        

         A43: for x,y be Element of L1 holds x <= y iff (h . x) <= (h . y)

        proof

          let x,y be Element of L1;

          

           A44: ( dom f) misses ( dom g) by A6, A21, A19, YELLOW_0:def 15;

          per cases by A2, XBOOLE_0:def 3;

            suppose

             A45: x in A1 & y in A1;

            then the carrier of ( subrelstr A2) <> {} by A7, Th4;

            then

            reconsider A29 = A2 as non empty Subset of L2 by YELLOW_0:def 15;

            reconsider A19 = A1 as non empty Subset of L1 by A45;

            reconsider ax = x, ay = y as Element of ( subrelstr A19) by A45, YELLOW_0:def 15;

            reconsider f9 = f as Function of ( subrelstr A19), ( subrelstr A29);

            

             A46: (h . x) = (f . x) & (h . y) = (f . y) by A1, A21, A20, A45, Th2, FUNCT_4: 16;

            hereby

              assume x <= y;

              then ax <= ay by YELLOW_0: 60;

              then (f9 . ax) <= (f9 . ay) by A7, WAYBEL_0: 66;

              hence (h . x) <= (h . y) by A46, YELLOW_0: 59;

            end;

            assume (h . x) <= (h . y);

            then (f9 . ax) <= (f9 . ay) by A46, YELLOW_0: 60;

            then ax <= ay by A7, WAYBEL_0: 66;

            hence thesis by YELLOW_0: 59;

          end;

            suppose

             A47: x in A1 & y in B1;

            hereby

              the carrier of ( subrelstr A2) <> {} & the carrier of ( subrelstr B2) <> {} by A7, A8, A47, Th4;

              then

              reconsider A29 = A2, B29 = B2 as non empty Subset of L2 by YELLOW_0:def 15;

              reconsider A19 = A1, B19 = B1 as non empty Subset of L1 by A47;

              assume x <= y;

              reconsider f9 = f as Function of ( subrelstr A19), ( subrelstr A29);

              reconsider g9 = g as Function of ( subrelstr B19), ( subrelstr B29);

              reconsider ax = x as Element of ( subrelstr A19) by A47, YELLOW_0:def 15;

              reconsider ay = y as Element of ( subrelstr B19) by A47, YELLOW_0:def 15;

              (f9 . ax) in the carrier of ( subrelstr A29);

              then

               A48: (f9 . ax) in A29 by YELLOW_0:def 15;

              (g9 . ay) in the carrier of ( subrelstr B29);

              then

               A49: (g9 . ay) in B29 by YELLOW_0:def 15;

              (f . x) = (h . x) & (g . y) = (h . y) by A21, A20, A44, A47, FUNCT_4: 13, FUNCT_4: 16;

              then (h . x) < (h . y) by A3, A48, A49;

              hence (h . x) <= (h . y) by ORDERS_2:def 6;

            end;

            assume (h . x) <= (h . y);

            x < y by A1, A47;

            hence thesis by ORDERS_2:def 6;

          end;

            suppose

             A50: x in B1 & y in A1;

            then the carrier of ( subrelstr B2) is non empty by A8, Th4;

            then ( subrelstr B2) is non empty;

            then

             A51: ( rng g) = the carrier of ( subrelstr B2) by A8, A50, WAYBEL_0: 66;

            (g . x) in ( rng g) by A20, A50, FUNCT_1:def 3;

            then

             A52: (g . x) in B2 by A51, YELLOW_0:def 15;

            the carrier of ( subrelstr A2) is non empty by A7, A50, Th4;

            then ( subrelstr A2) is non empty;

            then

             A53: ( rng f) = the carrier of ( subrelstr A2) by A7, A50, WAYBEL_0: 66;

            (f . y) in ( rng f) by A21, A50, FUNCT_1:def 3;

            then

             A54: (f . y) in A2 by A53, YELLOW_0:def 15;

            y < x by A1, A50;

            hence x <= y implies (h . x) <= (h . y) by ORDERS_2: 6;

            assume

             A55: (h . x) <= (h . y);

            (g . x) = (h . x) & (f . y) = (h . y) by A1, A21, A20, A50, Th2, FUNCT_4: 13, FUNCT_4: 16;

            then (h . x) > (h . y) by A3, A52, A54;

            hence thesis by A55, ORDERS_2: 6;

          end;

            suppose

             A56: x in B1 & y in B1;

            then the carrier of ( subrelstr B2) <> {} by A8, Th4;

            then

            reconsider B29 = B2 as non empty Subset of L2 by YELLOW_0:def 15;

            reconsider B19 = B1 as non empty Subset of L1 by A56;

            reconsider ax = x, ay = y as Element of ( subrelstr B19) by A56, YELLOW_0:def 15;

            reconsider g9 = g as Function of ( subrelstr B19), ( subrelstr B29);

            

             A57: (h . x) = (g . x) & (h . y) = (g . y) by A20, A56, FUNCT_4: 13;

            hereby

              assume x <= y;

              then ax <= ay by YELLOW_0: 60;

              then (g9 . ax) <= (g9 . ay) by A8, WAYBEL_0: 66;

              hence (h . x) <= (h . y) by A57, YELLOW_0: 59;

            end;

            assume (h . x) <= (h . y);

            then (g9 . ax) <= (g9 . ay) by A57, YELLOW_0: 60;

            then ax <= ay by A8, WAYBEL_0: 66;

            hence thesis by YELLOW_0: 59;

          end;

        end;

        h is one-to-one

        proof

          let x1,x2 be Element of L1;

          assume

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

          per cases by A2, XBOOLE_0:def 3;

            suppose

             A59: x1 in A1 & x2 in A1;

            then not x1 in B1 by A6, XBOOLE_0: 3;

            then

             A60: (h . x1) = (f . x1) by A20, FUNCT_4: 11;

            the carrier of ( subrelstr A2) <> {} by A7, A59, Th4;

            then

             A61: ( subrelstr A2) is non empty;

             not x2 in B1 by A6, A59, XBOOLE_0: 3;

            then (f . x1) = (f . x2) by A20, A58, A60, FUNCT_4: 11;

            hence thesis by A7, A21, A59, A61, FUNCT_1:def 4;

          end;

            suppose

             A62: x1 in A1 & x2 in B1;

            then the carrier of ( subrelstr A2) <> {} by A7, Th4;

            then ( subrelstr A2) is non empty;

            then ( rng f) = the carrier of ( subrelstr A2) by A7, A62, WAYBEL_0: 66;

            then

             A63: ( rng f) = A2 by YELLOW_0:def 15;

             not x1 in B1 by A6, A62, XBOOLE_0: 3;

            then (h . x2) = (f . x1) by A20, A58, FUNCT_4: 11;

            then

             A64: (h . x2) in ( rng f) by A21, A62, FUNCT_1:def 3;

            (h . x2) = (g . x2) by A20, A62, FUNCT_4: 13;

            then

             A65: (h . x2) in ( rng g) by A20, A62, FUNCT_1:def 3;

            the carrier of ( subrelstr B2) <> {} by A8, A62, Th4;

            then ( subrelstr B2) is non empty;

            then ( rng g) = the carrier of ( subrelstr B2) by A8, A62, WAYBEL_0: 66;

            then ( rng f) misses ( rng g) by A4, A63, YELLOW_0:def 15;

            hence thesis by A64, A65, XBOOLE_0: 3;

          end;

            suppose

             A66: x1 in B1 & x2 in A1;

            then not x2 in ( dom g) by A6, A20, XBOOLE_0: 3;

            then (h . x2) = (f . x2) by FUNCT_4: 11;

            then

             A67: (h . x2) in ( rng f) by A21, A66, FUNCT_1:def 3;

            the carrier of ( subrelstr B2) <> {} by A8, A66, Th4;

            then ( subrelstr B2) is non empty;

            then

             A68: ( rng g) = the carrier of ( subrelstr B2) by A8, A66, WAYBEL_0: 66;

            (h . x2) = (g . x1) by A20, A58, A66, FUNCT_4: 13;

            then

             A69: (h . x2) in ( rng g) by A20, A66, FUNCT_1:def 3;

            the carrier of ( subrelstr A2) <> {} by A7, A66, Th4;

            then ( subrelstr A2) is non empty;

            

            then ( rng f) = the carrier of ( subrelstr A2) by A7, A66, WAYBEL_0: 66

            .= A2 by YELLOW_0:def 15;

            then ( rng f) misses ( rng g) by A4, A68, YELLOW_0:def 15;

            hence thesis by A69, A67, XBOOLE_0: 3;

          end;

            suppose

             A70: x1 in B1 & x2 in B1;

            then the carrier of ( subrelstr B2) <> {} by A8, Th4;

            then

             A71: ( subrelstr B2) is non empty;

            (h . x1) = (g . x1) by A20, A70, FUNCT_4: 13;

            then (g . x1) = (g . x2) by A20, A58, A70, FUNCT_4: 13;

            hence thesis by A8, A20, A70, A71, FUNCT_1:def 4;

          end;

        end;

        then h is isomorphic by A32, A43, WAYBEL_0: 66;

        hence thesis;

      end;

    end;

    theorem :: ORDERS_4:6

    for A be finite Chain, n be Nat st ( card the carrier of A) = n holds (A,( InclPoset n)) are_isomorphic

    proof

      defpred P[ Nat] means for A be finite Chain st ( card the carrier of A) = $1 holds (A,( InclPoset $1)) are_isomorphic ;

      

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

      proof

        let n be Nat;

        assume

         A2: for A be finite Chain st ( card the carrier of A) = n holds (A,( InclPoset n)) are_isomorphic ;

        n >= 0 by NAT_1: 2;

        then (n + 1) >= ( 0 + 1) by XREAL_1: 6;

        then

         A3: n >= 1 or (n + 1) = 1 by NAT_1: 8;

        let A be finite Chain;

        assume

         A4: ( card the carrier of A) = (n + 1);

        then

        reconsider A as non empty finite Chain;

        set b = ( Top A);

        per cases by A3, NAT_1: 13;

          suppose

           A5: (n + 1) = 1;

          then

          consider x be object such that

           A6: the carrier of A = {x} by A4, CARD_2: 42;

          (A,( InclPoset 1)) are_isomorphic

          proof

            set g = (the carrier of A --> 0 );

            

             A7: ( rng g) = { 0 } by FUNCOP_1: 8;

            

             A8: { 0 } = the carrier of ( InclPoset 1) by CARD_1: 49, YELLOW_1: 1;

            then

            reconsider g as Function of A, ( InclPoset 1);

            

             A9: for e,f be Element of A holds e <= f iff (g . e) <= (g . f)

            proof

              let e,f be Element of A;

              hereby

                assume e <= f;

                (g . e) = 0 by FUNCOP_1: 7;

                hence (g . e) <= (g . f) by FUNCOP_1: 7;

              end;

              assume (g . e) <= (g . f);

              e = x by A6, TARSKI:def 1;

              hence thesis by A6, TARSKI:def 1;

            end;

            g is one-to-one

            proof

              let x1,x2 be Element of A;

              assume (g . x1) = (g . x2);

              x1 = x by A6, TARSKI:def 1;

              hence thesis by A6, TARSKI:def 1;

            end;

            then g is isomorphic by A7, A8, A9, WAYBEL_0: 66;

            hence thesis;

          end;

          hence thesis by A5;

        end;

          suppose

           A10: (n + 1) > 1;

          

           A11: ( card (the carrier of A \ {b})) = (( card the carrier of A) - ( card {b})) by CARD_2: 44

          .= ((n + 1) - 1) by A4, CARD_1: 30

          .= n;

          ((n + 1) - 1) > (1 - 1) by A10, XREAL_1: 9;

          then

          reconsider Ab = (the carrier of A \ {b}) as non empty Subset of A by A11;

          reconsider B = ( subrelstr Ab) as finite Chain by Def1;

          ( card the carrier of B) = n by A11, YELLOW_0:def 15;

          then (B,( InclPoset n)) are_isomorphic by A2;

          then

          consider f be Function of B, ( InclPoset n) such that

           A12: f is isomorphic;

          the carrier of B = (the carrier of A \ {b}) by YELLOW_0:def 15;

          then

           A13: (the carrier of B, {b}) form_upper_lower_partition_of A by Th3;

          

           A14: ( Segm (n + 1)) = (( Segm n) \/ {n}) by AFINSQ_1: 2;

          then {n} c= ( Segm (n + 1)) by XBOOLE_1: 7;

          then

          reconsider n9 = {n} as non empty Subset of ( InclPoset (n + 1)) by YELLOW_1: 1;

          set X = ( InclPoset {b});

          

           A15: the carrier of ( subrelstr n9) = n9 by YELLOW_0:def 15;

           {b} c= {b};

          then

          reconsider b9 = {b} as non empty Subset of X by YELLOW_1: 1;

          set X9 = ( subrelstr b9);

          set g = (the carrier of X9 --> n);

          ( dom g) = the carrier of X9 by FUNCOP_1: 13;

          then

          reconsider g as ManySortedSet of the carrier of X9 by PARTFUN1:def 2;

          

           A16: for a,b be Element of ( InclPoset (n + 1)) st a in the carrier of ( InclPoset n) & b in {n} holds a < b

          proof

            let a,b be Element of ( InclPoset (n + 1));

            assume that

             A17: a in the carrier of ( InclPoset n) and

             A18: b in {n};

            

             A19: a in n by A17, YELLOW_1: 1;

            then a in { i where i be Nat : i < n } by AXIOMS: 4;

            then

            consider h be Nat such that

             A20: h = a and

             A21: h < n;

            

             A22: b = n by A18, TARSKI:def 1;

            a c= b

            proof

              assume not a c= b;

              then

              consider x be object such that

               A23: x in a and

               A24: not x in b;

              x in { w where w be Nat : w < h } by A20, A23, AXIOMS: 4;

              then

              consider w9 be Nat such that

               A25: w9 = x and

               A26: w9 < h;

              w9 < n by A21, A26, XXREAL_0: 2;

              then w9 in { t where t be Nat : t < n };

              hence contradiction by A22, A24, A25, AXIOMS: 4;

            end;

            then

             A27: a <= b by YELLOW_1: 3;

            a <> b by A19, A22;

            hence thesis by A27, ORDERS_2:def 6;

          end;

          the carrier of ( InclPoset n) = n by YELLOW_1: 1;

          then (the carrier of ( InclPoset n) \/ {n}) = the carrier of ( InclPoset (n + 1)) by A14, YELLOW_1: 1;

          then

           A28: (the carrier of ( InclPoset n), {n}) form_upper_lower_partition_of ( InclPoset (n + 1)) by A16;

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

          then ( Segm n) c= ( Segm (n + 1)) by NAT_1: 39;

          then n c= the carrier of ( InclPoset (n + 1)) by YELLOW_1: 1;

          then

          reconsider A2 = the carrier of ( InclPoset n) as Subset of ( InclPoset (n + 1)) by YELLOW_1: 1;

          

           A29: the carrier of ( subrelstr {b}) = {b} by YELLOW_0:def 15;

          

           A30: the carrier of X9 = {b} by YELLOW_0:def 15;

          then

          reconsider g as Function of ( subrelstr {b}), ( subrelstr n9) by A15, A29;

          (g . b) in n9 by A15, A29, FUNCT_2: 47;

          then (g . b) = n by TARSKI:def 1;

          then

           A31: ( rng g) = the carrier of ( subrelstr n9) by A15, A29, FUNCT_2: 48;

          

           A32: for e,f be Element of ( subrelstr {b}) holds e <= f iff (g . e) <= (g . f)

          proof

            let e,f be Element of ( subrelstr {b});

            reconsider f1 = f as Element of X9 by A30, YELLOW_0:def 15;

            reconsider e1 = e as Element of X9 by A30, YELLOW_0:def 15;

            hereby

              assume e <= f;

              (g . e1) = n & (g . f1) = n by FUNCOP_1: 7;

              hence (g . e) <= (g . f);

            end;

            assume (g . e) <= (g . f);

            e in the carrier of ( subrelstr {b});

            then e in {b} by YELLOW_0:def 15;

            then

             A33: e = b by TARSKI:def 1;

            f in the carrier of ( subrelstr {b});

            then f in {b} by YELLOW_0:def 15;

            hence thesis by A33, TARSKI:def 1;

          end;

          g is one-to-one by A29, PARTFUN1: 17;

          then

           A34: g is isomorphic by A31, A32, WAYBEL_0: 66;

          ( InclPoset n) is full SubRelStr of ( InclPoset (n + 1)) by Th1, NAT_1: 11;

          then

           A35: ( InclPoset n) = ( subrelstr A2) by YELLOW_0:def 15;

          the carrier of B = Ab by YELLOW_0:def 15;

          then ex h be Function of A, ( InclPoset (n + 1)) st h = (f +* g) & h is isomorphic by A12, A13, A28, A34, A35, Th5;

          hence thesis;

        end;

      end;

      

       A36: P[ 0 ]

      proof

        let A be finite Chain;

        set f = the Function of A, ( InclPoset 0 );

        assume ( card the carrier of A) = 0 ;

        then

         A37: A is empty;

        take f;

        ( InclPoset 0 ) is empty by YELLOW_1: 1;

        hence thesis by A37, WAYBEL_0:def 38;

      end;

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

      hence thesis;

    end;