taxonom1.miz



    begin

    reserve A,X for non empty set;

    reserve f for PartFunc of [:X, X:], REAL ;

    reserve a for Real;

    registration

      cluster non negative for Real;

      existence

      proof

        take 0 ;

        thus thesis;

      end;

    end

    theorem :: TAXONOM1:1

    

     Th1: for p be FinSequence, k be Nat st (k + 1) in ( dom p) & not k in ( dom p) holds k = 0

    proof

      let p be FinSequence, k be Nat such that

       A1: (k + 1) in ( dom p) and

       A2: not k in ( dom p);

      assume k <> 0 ;

      then

       A3: k >= 1 by NAT_1: 14;

      k <= (k + 1) & (k + 1) <= ( len p) by A1, FINSEQ_3: 25, NAT_1: 12;

      then k <= ( len p) by XXREAL_0: 2;

      hence thesis by A2, A3, FINSEQ_3: 25;

    end;

    theorem :: TAXONOM1:2

    

     Th2: for p be FinSequence, i,j be Nat st i in ( dom p) & j in ( dom p) & for k be Nat st k in ( dom p) & (k + 1) in ( dom p) holds (p . k) = (p . (k + 1)) holds (p . i) = (p . j)

    proof

      let p be FinSequence, i,j be Nat such that

       A1: i in ( dom p) & j in ( dom p) and

       A2: for k be Nat st k in ( dom p) & (k + 1) in ( dom p) holds (p . k) = (p . (k + 1));

      defpred P[ Nat] means for j be Nat st $1 in ( dom p) & j in ( dom p) holds (p . $1) = (p . j);

      

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

      proof

        let k be Nat such that

         A4: P[k];

        let j be Nat such that

         A5: (k + 1) in ( dom p) and

         A6: j in ( dom p);

        per cases ;

          suppose

           A7: k in ( dom p);

          

          hence (p . (k + 1)) = (p . k) by A2, A5

          .= (p . j) by A4, A6, A7;

        end;

          suppose

           A8: not k in ( dom p);

          defpred R[ Nat] means $1 in ( dom p) implies (p . $1) = (p . 1);

          

           A9: for w be Nat st R[w] holds R[(w + 1)]

          proof

            let w be Nat such that

             A10: R[w];

            assume

             A11: (w + 1) in ( dom p);

            per cases ;

              suppose w in ( dom p);

              hence thesis by A2, A10, A11;

            end;

              suppose not w in ( dom p);

              then w = 0 by A11, Th1;

              hence thesis;

            end;

          end;

          

           A12: R[ 0 ] by FINSEQ_3: 24;

          

           A13: for k be Nat holds R[k] from NAT_1:sch 2( A12, A9);

          k = 0 by A5, A8, Th1;

          hence thesis by A6, A13;

        end;

      end;

      

       A14: P[ 0 ] by FINSEQ_3: 24;

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

      hence thesis by A1;

    end;

    theorem :: TAXONOM1:3

    

     Th3: for X be set, R be Relation of X st R is_reflexive_in X holds ( dom R) = X

    proof

      let X be set, R be Relation of X such that

       A1: R is_reflexive_in X;

      for x be object st x in X holds ex y be object st [x, y] in R

      proof

        let x be object such that

         A2: x in X;

        take x;

        thus thesis by A1, A2, RELAT_2:def 1;

      end;

      hence thesis by RELSET_1: 9;

    end;

    theorem :: TAXONOM1:4

    for X be set, R be Relation of X st R is_reflexive_in X holds ( rng R) = X

    proof

      let X be set, R be Relation of X such that

       A1: R is_reflexive_in X;

      for x be object st x in X holds ex y be object st [y, x] in R

      proof

        let x be object such that

         A2: x in X;

        take x;

        thus thesis by A1, A2, RELAT_2:def 1;

      end;

      hence thesis by RELSET_1: 10;

    end;

    theorem :: TAXONOM1:5

    

     Th5: for X be set, R be Relation of X st R is_reflexive_in X holds (R [*] ) is_reflexive_in X

    proof

      let X be set, R be Relation of X such that

       A1: R is_reflexive_in X;

      now

        let x be object;

        assume x in X;

        then

         A2: [x, x] in R by A1, RELAT_2:def 1;

        R c= (R [*] ) by LANG1: 18;

        hence [x, x] in (R [*] ) by A2;

      end;

      hence thesis by RELAT_2:def 1;

    end;

    theorem :: TAXONOM1:6

    

     Th6: for X be set, x,y be object holds for R be Relation of X st R is_reflexive_in X holds R reduces (x,y) & x in X implies [x, y] in (R [*] )

    proof

      let X be set, x,y be object;

      let R be Relation of X such that

       A1: R is_reflexive_in X;

      assume that

       A2: R reduces (x,y) and

       A3: x in X;

      per cases by A2, REWRITE1: 20;

        suppose [x, y] in (R [*] );

        hence thesis;

      end;

        suppose

         A4: x = y;

        (R [*] ) is_reflexive_in X by A1, Th5;

        hence thesis by A3, A4, RELAT_2:def 1;

      end;

    end;

    theorem :: TAXONOM1:7

    

     Th7: for X be set, R be Relation of X st R is_symmetric_in X holds (R [*] ) is_symmetric_in X

    proof

      let X be set, R be Relation of X such that

       A1: R is_symmetric_in X;

      now

        let x,y be object;

        assume that x in X and y in X and

         A2: [x, y] in (R [*] );

        

         A3: x in ( field R) & y in ( field R) by A2, FINSEQ_1:def 16;

        consider p be FinSequence such that

         A4: ( len p) >= 1 and

         A5: (p . 1) = x and

         A6: (p . ( len p)) = y and

         A7: for i be Nat st i >= 1 & i < ( len p) holds [(p . i), (p . (i + 1))] in R by A2, FINSEQ_1:def 16;

        consider r be FinSequence such that

         A8: r = ( Rev p);

         A9:

        now

          let j be Nat such that

           A10: j >= 1 and

           A11: j < ( len r);

          

           A12: (( len p) - 0 ) > (( len p) - j) by A10, XREAL_1: 10;

          j <= ( len p) by A8, A11, FINSEQ_5:def 3;

          then j in ( Seg ( len p)) by A10, FINSEQ_1: 1;

          then j in ( dom p) by FINSEQ_1:def 3;

          then

           A13: (r . j) = (p . ((( len p) - j) + 1)) by A8, FINSEQ_5: 58;

          

           A14: j < ( len p) by A8, A11, FINSEQ_5:def 3;

          then

           A15: ( len p) >= (j + 1) by NAT_1: 13;

          (j + 1) >= 1 by NAT_1: 11;

          then (j + 1) in ( Seg ( len p)) by A15, FINSEQ_1: 1;

          then

           A16: (j + 1) in ( dom p) by FINSEQ_1:def 3;

          (( len p) - j) is Nat by A14, NAT_1: 21;

          then (( len p) - j) in NAT by ORDINAL1:def 12;

          then

          consider j1 be Element of NAT such that

           A17: j1 = (( len p) - j);

          j1 >= 1 by A15, A17, XREAL_1: 19;

          then

           A18: [(p . (( len p) - j)), (p . ((( len p) - j) + 1))] in R by A7, A17, A12;

          then (p . (( len p) - j)) in X & (p . ((( len p) - j) + 1)) in X by ZFMISC_1: 87;

          then [(p . ((( len p) - j) + 1)), (p . ((( len p) - (j + 1)) + 1))] in R by A1, A18, RELAT_2:def 3;

          hence [(r . j), (r . (j + 1))] in R by A8, A16, A13, FINSEQ_5: 58;

        end;

        

         A19: (r . ( len r)) = (r . ( len p)) by A8, FINSEQ_5:def 3

        .= x by A5, A8, FINSEQ_5: 62;

        ( len r) >= 1 & (r . 1) = y by A4, A6, A8, FINSEQ_5: 62, FINSEQ_5:def 3;

        hence [y, x] in (R [*] ) by A3, A19, A9, FINSEQ_1:def 16;

      end;

      hence thesis by RELAT_2:def 3;

    end;

    theorem :: TAXONOM1:8

    

     Th8: for X be set, R be Relation of X st R is_reflexive_in X holds (R [*] ) is_transitive_in X

    proof

      let X be set, R be Relation of X such that

       A1: R is_reflexive_in X;

      now

        let x,y,z be object;

        assume that

         A2: x in X and y in X and z in X and

         A3: [x, y] in (R [*] ) & [y, z] in (R [*] );

        R reduces (x,y) & R reduces (y,z) by A3, REWRITE1: 20;

        hence [x, z] in (R [*] ) by A1, A2, Th6, REWRITE1: 16;

      end;

      hence thesis by RELAT_2:def 8;

    end;

    theorem :: TAXONOM1:9

    

     Th9: for X be non empty set, R be Relation of X st R is_reflexive_in X & R is_symmetric_in X holds (R [*] ) is Equivalence_Relation of X

    proof

      let X be non empty set, R be Relation of X such that

       A1: R is_reflexive_in X and

       A2: R is_symmetric_in X;

      (R [*] ) is_reflexive_in X by A1, Th5;

      then

       A3: ( dom (R [*] )) = X & ( field (R [*] )) = X by ORDERS_1: 13;

      (R [*] ) is_symmetric_in X & (R [*] ) is_transitive_in X by A1, A2, Th7, Th8;

      hence thesis by A3, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

    end;

    theorem :: TAXONOM1:10

    

     Th10: for R1,R2 be Relation of X holds R1 c= R2 implies (R1 [*] ) c= (R2 [*] )

    proof

      let R1,R2 be Relation of X;

      assume

       A1: R1 c= R2;

      

       A2: ( field R1) c= ( field R2) by A1, RELAT_1: 16;

      let p be object such that

       A3: p in (R1 [*] );

      consider x,y be object such that

       A4: p = [x, y] by A3, RELAT_1:def 1;

      consider r be FinSequence such that

       A5: ( len r) >= 1 & (r . 1) = x & (r . ( len r)) = y and

       A6: for i be Nat st i >= 1 & i < ( len r) holds [(r . i), (r . (i + 1))] in R1 by A3, A4, FINSEQ_1:def 16;

      

       A7: for i be Nat st i >= 1 & i < ( len r) holds [(r . i), (r . (i + 1))] in R2 by A1, A6;

      x in ( field R1) & y in ( field R1) by A3, A4, FINSEQ_1:def 16;

      hence p in (R2 [*] ) by A4, A5, A2, A7, FINSEQ_1:def 16;

    end;

     Lm1:

    now

      let A;

      let X,Y be a_partition of A;

      assume that

       A1: X in { {A}} and

       A2: Y in { {A}};

      X = {A} by A1, TARSKI:def 1;

      hence X is_finer_than Y or Y is_finer_than X by A2, TARSKI:def 1;

    end;

    theorem :: TAXONOM1:11

    

     Th11: ( SmallestPartition A) is_finer_than {A}

    proof

      let X be set;

      assume

       A1: X in ( SmallestPartition A);

      take A;

      thus thesis by A1, TARSKI:def 1;

    end;

    begin

    definition

      let A be non empty set;

      :: TAXONOM1:def1

      mode Classification of A -> Subset of ( PARTITIONS A) means

      : Def1: for X,Y be a_partition of A st X in it & Y in it holds X is_finer_than Y or Y is_finer_than X;

      existence

      proof

         {A} is a_partition of A by EQREL_1: 39;

        then {A} in ( PARTITIONS A) by PARTIT1:def 3;

        then

        reconsider S = { {A}} as Subset of ( PARTITIONS A) by ZFMISC_1: 31;

        take S;

        thus thesis by Lm1;

      end;

    end

    theorem :: TAXONOM1:12

     { {A}} is Classification of A

    proof

       {A} is a_partition of A by EQREL_1: 39;

      then {A} in ( PARTITIONS A) by PARTIT1:def 3;

      then

      reconsider S = { {A}} as Subset of ( PARTITIONS A) by ZFMISC_1: 31;

      S is Classification of A

      proof

        let X be a_partition of A;

        thus thesis by Lm1;

      end;

      hence thesis;

    end;

    theorem :: TAXONOM1:13

     {( SmallestPartition A)} is Classification of A

    proof

      ( SmallestPartition A) in ( PARTITIONS A) by PARTIT1:def 3;

      then

      reconsider S = {( SmallestPartition A)} as Subset of ( PARTITIONS A) by ZFMISC_1: 31;

      S is Classification of A

      proof

        let X,Y be a_partition of A;

        assume that

         A1: X in S and

         A2: Y in S;

        X = ( SmallestPartition A) by A1, TARSKI:def 1;

        hence thesis by A2, TARSKI:def 1;

      end;

      hence thesis;

    end;

    theorem :: TAXONOM1:14

    

     Th14: for S be Subset of ( PARTITIONS A) st S = { {A}, ( SmallestPartition A)} holds S is Classification of A

    proof

      let S be Subset of ( PARTITIONS A);

      assume

       A1: S = { {A}, ( SmallestPartition A)};

      let X,Y be a_partition of A such that

       A2: X in S and

       A3: Y in S;

      per cases by A1, A2, TARSKI:def 2;

        suppose

         A4: X = {A};

        per cases by A1, A3, TARSKI:def 2;

          suppose Y = {A};

          hence thesis by A4;

        end;

          suppose Y = ( SmallestPartition A);

          hence thesis by A4, Th11;

        end;

      end;

        suppose

         A5: X = ( SmallestPartition A);

        per cases by A1, A3, TARSKI:def 2;

          suppose Y = ( SmallestPartition A);

          hence thesis by A5;

        end;

          suppose Y = {A};

          hence thesis by A5, Th11;

        end;

      end;

    end;

    definition

      let A be non empty set;

      :: TAXONOM1:def2

      mode Strong_Classification of A -> Subset of ( PARTITIONS A) means

      : Def2: it is Classification of A & {A} in it & ( SmallestPartition A) in it ;

      existence

      proof

         {A} is a_partition of A by EQREL_1: 39;

        then

         A1: {A} in ( PARTITIONS A) by PARTIT1:def 3;

        ( SmallestPartition A) in ( PARTITIONS A) by PARTIT1:def 3;

        then

        reconsider S = { {A}, ( SmallestPartition A)} as Subset of ( PARTITIONS A) by A1, ZFMISC_1: 32;

        take S;

        thus thesis by Th14, TARSKI:def 2;

      end;

    end

    theorem :: TAXONOM1:15

    for S be Subset of ( PARTITIONS A) st S = { {A}, ( SmallestPartition A)} holds S is Strong_Classification of A

    proof

      let S be Subset of ( PARTITIONS A) such that

       A1: S = { {A}, ( SmallestPartition A)};

      

       A2: ( SmallestPartition A) in S by A1, TARSKI:def 2;

      S is Classification of A & {A} in S by A1, Th14, TARSKI:def 2;

      hence thesis by A2, Def2;

    end;

    begin

    definition

      let X be non empty set, f be PartFunc of [:X, X:], REAL , a be Real;

      :: TAXONOM1:def3

      func low_toler (f,a) -> Relation of X means

      : Def3: for x,y be Element of X holds [x, y] in it iff (f . (x,y)) <= a;

      existence

      proof

        defpred X[ Element of X, Element of X] means (f . ($1,$2)) <= a;

        consider R be Relation of X, X such that

         A1: for x,y be Element of X holds [x, y] in R iff X[x, y] from RELSET_1:sch 2;

        take R;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let R1,R2 be Relation of X such that

         A2: for x,y be Element of X holds [x, y] in R1 iff (f . (x,y)) <= a and

         A3: for x,y be Element of X holds [x, y] in R2 iff (f . (x,y)) <= a;

        

         A4: for c,d be object holds [c, d] in R2 implies [c, d] in R1

        proof

          let c,d be object;

          assume

           A5: [c, d] in R2;

          then

          reconsider c1 = c, d1 = d as Element of X by ZFMISC_1: 87;

          (f . (c1,d1)) <= a by A3, A5;

          hence thesis by A2;

        end;

        for c,d be object holds [c, d] in R1 implies [c, d] in R2

        proof

          let c,d be object;

          assume

           A6: [c, d] in R1;

          then

          reconsider c1 = c, d1 = d as Element of X by ZFMISC_1: 87;

          (f . (c1,d1)) <= a by A2, A6;

          hence thesis by A3;

        end;

        hence thesis by A4, RELAT_1:def 2;

      end;

    end

    theorem :: TAXONOM1:16

    

     Th16: f is Reflexive & a >= 0 implies ( low_toler (f,a)) is_reflexive_in X

    proof

      assume

       A1: f is Reflexive & a >= 0 ;

      now

        let x be object;

        assume x in X;

        then

        reconsider x1 = x as Element of X;

        (f . (x1,x1)) <= a by A1, METRIC_1:def 2;

        hence [x, x] in ( low_toler (f,a)) by Def3;

      end;

      hence thesis by RELAT_2:def 1;

    end;

    theorem :: TAXONOM1:17

    

     Th17: f is symmetric implies ( low_toler (f,a)) is_symmetric_in X

    proof

      assume

       A1: f is symmetric;

      now

        let x,y be object such that

         A2: x in X & y in X and

         A3: [x, y] in ( low_toler (f,a));

        reconsider x1 = x, y1 = y as Element of X by A2;

        (f . (x1,y1)) <= a by A3, Def3;

        then (f . (y1,x1)) <= a by A1, METRIC_1:def 4;

        hence [y, x] in ( low_toler (f,a)) by Def3;

      end;

      hence thesis by RELAT_2:def 3;

    end;

    theorem :: TAXONOM1:18

    

     Th18: a >= 0 & f is Reflexive symmetric implies ( low_toler (f,a)) is Tolerance of X

    proof

      set T = ( low_toler (f,a));

      assume that

       A1: a >= 0 and

       A2: f is Reflexive symmetric;

      

       A3: ( low_toler (f,a)) is_reflexive_in X by A1, A2, Th16;

      

       A4: ( dom T) = X by A1, A2, Th3, Th16;

      

      then

       A5: ( field T) = (X \/ ( rng ( low_toler (f,a)))) by RELAT_1:def 6

      .= X by XBOOLE_1: 12;

      then T is_symmetric_in ( field T) by A2, Th17;

      hence thesis by A3, A4, A5, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 11;

    end;

    theorem :: TAXONOM1:19

    

     Th19: for X be non empty set, f be PartFunc of [:X, X:], REAL , a1,a2 be Real st a1 <= a2 holds ( low_toler (f,a1)) c= ( low_toler (f,a2))

    proof

      let X be non empty set, f be PartFunc of [:X, X:], REAL , a1,a2 be Real such that

       A1: a1 <= a2;

      let p be object such that

       A2: p in ( low_toler (f,a1));

      consider x,y be object such that

       A3: x in X & y in X and

       A4: p = [x, y] by A2, ZFMISC_1:def 2;

      reconsider x1 = x, y1 = y as Element of X by A3;

      (f . (x1,y1)) <= a1 by A2, A4, Def3;

      then (f . (x1,y1)) <= a2 by A1, XXREAL_0: 2;

      hence p in ( low_toler (f,a2)) by A4, Def3;

    end;

    definition

      let X be set;

      let f be PartFunc of [:X, X:], REAL ;

      :: TAXONOM1:def4

      attr f is nonnegative means for x,y be Element of X holds (f . (x,y)) >= 0 ;

    end

    theorem :: TAXONOM1:20

    

     Th20: for X be non empty set, f be PartFunc of [:X, X:], REAL , x,y be object st f is nonnegative Reflexive discerning holds [x, y] in ( low_toler (f, 0 )) implies x = y

    proof

      let X be non empty set, f be PartFunc of [:X, X:], REAL , x,y be object such that

       A1: f is nonnegative Reflexive discerning;

      assume

       A2: [x, y] in ( low_toler (f, 0 ));

      then

      reconsider x1 = x, y1 = y as Element of X by ZFMISC_1: 87;

      (f . (x1,y1)) <= 0 by A2, Def3;

      then (f . (x1,y1)) = 0 by A1;

      hence thesis by A1, METRIC_1:def 3;

    end;

    theorem :: TAXONOM1:21

    

     Th21: for X be non empty set, f be PartFunc of [:X, X:], REAL , x be Element of X st f is Reflexive discerning holds [x, x] in ( low_toler (f, 0 ))

    proof

      let X be non empty set, f be PartFunc of [:X, X:], REAL , x be Element of X;

      assume f is Reflexive discerning;

      then (f . (x,x)) = 0 by METRIC_1:def 2;

      hence thesis by Def3;

    end;

    theorem :: TAXONOM1:22

    

     Th22: for X be non empty set, f be PartFunc of [:X, X:], REAL , a be Real st ( low_toler (f,a)) is_reflexive_in X & f is symmetric holds (( low_toler (f,a)) [*] ) is Equivalence_Relation of X

    proof

      let X be non empty set, f be PartFunc of [:X, X:], REAL , a be Real such that

       A1: ( low_toler (f,a)) is_reflexive_in X and

       A2: f is symmetric;

      now

        let x,y be object such that

         A3: x in X & y in X and

         A4: [x, y] in ( low_toler (f,a));

        reconsider x1 = x, y1 = y as Element of X by A3;

        (f . (x1,y1)) <= a by A4, Def3;

        then (f . (y1,x1)) <= a by A2, METRIC_1:def 4;

        hence [y, x] in ( low_toler (f,a)) by Def3;

      end;

      then ( low_toler (f,a)) is_symmetric_in X by RELAT_2:def 3;

      hence thesis by A1, Th9;

    end;

    

     Lm2: for x be object, X be non empty set, a1,a2 be non negative Real st a1 <= a2 holds for f be PartFunc of [:X, X:], REAL , R1,R2 be Equivalence_Relation of X st R1 = (( low_toler (f,a1)) [*] ) & R2 = (( low_toler (f,a2)) [*] ) holds ( Class (R1,x)) c= ( Class (R2,x))

    proof

      let x be object, X be non empty set, a1,a2 be non negative Real such that

       A1: a1 <= a2;

      let f be PartFunc of [:X, X:], REAL , R1,R2 be Equivalence_Relation of X such that

       A2: R1 = (( low_toler (f,a1)) [*] ) & R2 = (( low_toler (f,a2)) [*] );

      let z1 be object;

      assume z1 in ( Class (R1,x));

      then

       A3: [z1, x] in R1 by EQREL_1: 19;

      R1 c= R2 by A1, A2, Th10, Th19;

      hence z1 in ( Class (R2,x)) by A3, EQREL_1: 19;

    end;

    begin

    theorem :: TAXONOM1:23

    

     Th23: for X be non empty set, f be PartFunc of [:X, X:], REAL st f is nonnegative Reflexive discerning holds (( low_toler (f, 0 )) [*] ) = ( low_toler (f, 0 ))

    proof

      let X be non empty set, f be PartFunc of [:X, X:], REAL such that

       A1: f is nonnegative Reflexive discerning;

      now

        let p be object such that

         A2: p in (( low_toler (f, 0 )) [*] );

        consider x,y be object such that

         A3: p = [x, y] by A2, RELAT_1:def 1;

        ( low_toler (f, 0 )) reduces (x,y) by A2, A3, REWRITE1: 20;

        then

        consider r be RedSequence of ( low_toler (f, 0 )) such that

         A4: (r . 1) = x & (r . ( len r)) = y by REWRITE1:def 3;

         A5:

        now

          let i be Nat;

          assume i in ( dom r) & (i + 1) in ( dom r);

          then [(r . i), (r . (i + 1))] in ( low_toler (f, 0 )) by REWRITE1:def 2;

          hence (r . i) = (r . (i + 1)) by A1, Th20;

        end;

        

         A6: x is Element of X by A2, A3, ZFMISC_1: 87;

         0 < ( len r) by REWRITE1:def 2;

        then ( 0 + 1) <= ( len r) by NAT_1: 13;

        then 1 in ( dom r) & ( len r) in ( dom r) by FINSEQ_3: 25;

        then (r . 1) = (r . ( len r)) by A5, Th2;

        hence p in ( low_toler (f, 0 )) by A1, A3, A4, A6, Th21;

      end;

      then ( low_toler (f, 0 )) c= (( low_toler (f, 0 )) [*] ) & (( low_toler (f, 0 )) [*] ) c= ( low_toler (f, 0 )) by LANG1: 18;

      hence thesis by XBOOLE_0:def 10;

    end;

    theorem :: TAXONOM1:24

    

     Th24: for X be non empty set, f be PartFunc of [:X, X:], REAL , R be Equivalence_Relation of X st R = (( low_toler (f, 0 )) [*] ) & f is nonnegative Reflexive discerning holds R = ( id X)

    proof

      let X be non empty set, f be PartFunc of [:X, X:], REAL , R be Equivalence_Relation of X such that

       A1: R = (( low_toler (f, 0 )) [*] ) and

       A2: f is nonnegative Reflexive discerning;

      

       A3: for x,y be object st x in X & x = y holds [x, y] in (( low_toler (f, 0 )) [*] )

      proof

        let x,y be object;

        assume x in X & x = y;

        then [x, y] in ( low_toler (f, 0 )) by A2, Th21;

        hence thesis by A2, Th23;

      end;

      for x,y be object st [x, y] in (( low_toler (f, 0 )) [*] ) holds x in X & x = y

      proof

        let x,y be object;

        assume [x, y] in (( low_toler (f, 0 )) [*] );

        then [x, y] in ( low_toler (f, 0 )) by A2, Th23;

        hence thesis by A2, Th20, ZFMISC_1: 87;

      end;

      hence thesis by A1, A3, RELAT_1:def 10;

    end;

    theorem :: TAXONOM1:25

    for X be non empty set, f be PartFunc of [:X, X:], REAL , R be Equivalence_Relation of X st R = (( low_toler (f, 0 )) [*] ) & f is nonnegative Reflexive discerning holds ( Class R) = ( SmallestPartition X) by Th24;

    theorem :: TAXONOM1:26

    

     Th26: for X be finite non empty Subset of REAL , f be Function of [:X, X:], REAL , z be finite non empty Subset of REAL , A be Real st z = ( rng f) & A >= ( max z) holds for x,y be Element of X holds (f . (x,y)) <= A

    proof

      let X be finite non empty Subset of REAL , f be Function of [:X, X:], REAL , z be finite non empty Subset of REAL , A be Real such that

       A1: z = ( rng f) and

       A2: A >= ( max z);

      now

        let x,y be Element of X;

        reconsider c = (f . [x, y]) as Real;

        ( dom f) = [:X, X:] by FUNCT_2:def 1;

        then [x, y] in ( dom f) by ZFMISC_1:def 2;

        then c in z by A1, FUNCT_1:def 3;

        then (f . (x,y)) <= ( max z) by XXREAL_2:def 8;

        hence (f . (x,y)) <= A by A2, XXREAL_0: 2;

      end;

      hence thesis;

    end;

    theorem :: TAXONOM1:27

    

     Th27: for X be finite non empty Subset of REAL , f be Function of [:X, X:], REAL , z be finite non empty Subset of REAL , A be Real st z = ( rng f) & A >= ( max z) holds for R be Equivalence_Relation of X st R = (( low_toler (f,A)) [*] ) holds ( Class R) = {X}

    proof

      let X be finite non empty Subset of REAL , f be Function of [:X, X:], REAL , z be finite non empty Subset of REAL , A be Real such that

       A1: z = ( rng f) & A >= ( max z);

      now

        let R be Equivalence_Relation of X such that

         A2: R = (( low_toler (f,A)) [*] );

        

         A3: for x be set st x in X holds X = ( Class (R,x))

        proof

          let x be set;

          assume x in X;

          then

          reconsider x9 = x as Element of X;

          now

            let x1 be object;

            assume x1 in X;

            then

            reconsider x19 = x1 as Element of X;

            (f . (x19,x9)) <= A by A1, Th26;

            then

             A4: [x1, x] in ( low_toler (f,A)) by Def3;

            ( low_toler (f,A)) c= (( low_toler (f,A)) [*] ) by LANG1: 18;

            hence x1 in ( Class (R,x)) by A2, A4, EQREL_1: 19;

          end;

          then X c= ( Class (R,x));

          hence thesis by XBOOLE_0:def 10;

        end;

        now

          let a be object;

          assume a in {X};

          then

           A5: a = X by TARSKI:def 1;

          consider x be object such that

           A6: x in X by XBOOLE_0:def 1;

          X = ( Class (R,x)) by A3, A6;

          hence a in ( Class R) by A5, A6, EQREL_1:def 3;

        end;

        then

         A7: {X} c= ( Class R);

        now

          let a be object;

          assume a in ( Class R);

          then ex x be object st x in X & a = ( Class (R,x)) by EQREL_1:def 3;

          then a = X by A3;

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

        end;

        then ( Class R) c= {X};

        hence ( Class R) = {X} by A7, XBOOLE_0:def 10;

      end;

      hence thesis;

    end;

    theorem :: TAXONOM1:28

    for X be finite non empty Subset of REAL , f be Function of [:X, X:], REAL , z be finite non empty Subset of REAL , A be Real st z = ( rng f) & A >= ( max z) holds (( low_toler (f,A)) [*] ) = ( low_toler (f,A))

    proof

      let X be finite non empty Subset of REAL , f be Function of [:X, X:], REAL , z be finite non empty Subset of REAL , A be Real such that

       A1: z = ( rng f) & A >= ( max z);

      now

        let p be object;

        assume p in (( low_toler (f,A)) [*] );

        then

        consider x,y be object such that

         A2: x in X & y in X and

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

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

        (f . (x9,y9)) <= A by A1, Th26;

        hence p in ( low_toler (f,A)) by A3, Def3;

      end;

      then ( low_toler (f,A)) c= (( low_toler (f,A)) [*] ) & (( low_toler (f,A)) [*] ) c= ( low_toler (f,A)) by LANG1: 18;

      hence thesis by XBOOLE_0:def 10;

    end;

    begin

    definition

      let X be non empty set, f be PartFunc of [:X, X:], REAL ;

      :: TAXONOM1:def5

      func fam_class (f) -> Subset of ( PARTITIONS X) means

      : Def5: for x be object holds x in it iff ex a be non negative Real, R be Equivalence_Relation of X st R = (( low_toler (f,a)) [*] ) & ( Class R) = x;

      existence

      proof

        defpred X[ object] means ex a be non negative Real, R be Equivalence_Relation of X st R = (( low_toler (f,a)) [*] ) & ( Class R) = $1;

        consider A be set such that

         A1: for x be object holds x in A iff x in ( PARTITIONS X) & X[x] from XBOOLE_0:sch 1;

        A c= ( PARTITIONS X) by A1;

        then

        reconsider A1 = A as Subset of ( PARTITIONS X);

        take A1;

        let x be object;

        thus x in A1 implies ex a be non negative Real, R be Equivalence_Relation of X st R = (( low_toler (f,a)) [*] ) & ( Class R) = x by A1;

        given a be non negative Real, R be Equivalence_Relation of X such that

         A2: R = (( low_toler (f,a)) [*] ) & ( Class R) = x;

        ( Class R) in ( PARTITIONS X) by PARTIT1:def 3;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        defpred X[ object] means ex a be non negative Real, R be Equivalence_Relation of X st R = (( low_toler (f,a)) [*] ) & ( Class R) = $1;

        

         A3: for X1,X2 be Subset of ( PARTITIONS X) st (for x be object holds x in X1 iff X[x]) & (for x be object holds x in X2 iff X[x]) holds X1 = X2 from LMOD_7:sch 1;

        let X1,X2 be Subset of ( PARTITIONS X);

        assume (for x be object holds x in X1 iff ex a be non negative Real, R be Equivalence_Relation of X st R = (( low_toler (f,a)) [*] ) & ( Class R) = x) & (for x be object holds x in X2 iff ex a be non negative Real, R be Equivalence_Relation of X st R = (( low_toler (f,a)) [*] ) & ( Class R) = x);

        hence thesis by A3;

      end;

    end

    theorem :: TAXONOM1:29

    for X be non empty set, f be PartFunc of [:X, X:], REAL , a be non negative Real st ( low_toler (f,a)) is_reflexive_in X & f is symmetric holds ( fam_class f) is non empty set

    proof

      let X be non empty set, f be PartFunc of [:X, X:], REAL , a be non negative Real;

      assume ( low_toler (f,a)) is_reflexive_in X & f is symmetric;

      then

      reconsider R = (( low_toler (f,a)) [*] ) as Equivalence_Relation of X by Th22;

      reconsider x = ( Class R) as set;

      x in ( fam_class f) by Def5;

      hence thesis;

    end;

    theorem :: TAXONOM1:30

    

     Th30: for X be finite non empty Subset of REAL , f be Function of [:X, X:], REAL st f is symmetric nonnegative holds {X} in ( fam_class f)

    proof

      let X be finite non empty Subset of REAL , f be Function of [:X, X:], REAL such that

       A1: f is symmetric nonnegative;

      ( dom f) = [:X, X:] by FUNCT_2:def 1;

      then

      reconsider rn = ( rng f) as finite non empty Subset of REAL by RELAT_1: 42;

      reconsider A1 = ( max rn) as Real;

      now

        set x = the Element of X;

        assume

         A2: A1 is negative;

        (f . (x,x)) <= A1 by Th26;

        hence contradiction by A1, A2;

      end;

      then

      reconsider A19 = A1 as non negative Real;

      now

        let x be object;

        assume x in X;

        then

        reconsider x1 = x as Element of X;

        (f . (x1,x1)) <= A1 by Th26;

        hence [x, x] in ( low_toler (f,A1)) by Def3;

      end;

      then ( low_toler (f,A19)) is_reflexive_in X by RELAT_2:def 1;

      then

      reconsider R = (( low_toler (f,A19)) [*] ) as Equivalence_Relation of X by A1, Th22;

      ( Class R) in ( fam_class f) by Def5;

      hence thesis by Th27;

    end;

    theorem :: TAXONOM1:31

    

     Th31: for X be non empty set, f be PartFunc of [:X, X:], REAL holds ( fam_class f) is Classification of X

    proof

      let X be non empty set, f be PartFunc of [:X, X:], REAL ;

      for A,B be a_partition of X st A in ( fam_class f) & B in ( fam_class f) holds A is_finer_than B or B is_finer_than A

      proof

        let A,B be a_partition of X;

        assume that

         A1: A in ( fam_class f) and

         A2: B in ( fam_class f);

        consider a1 be non negative Real, R1 be Equivalence_Relation of X such that

         A3: R1 = (( low_toler (f,a1)) [*] ) and

         A4: ( Class R1) = A by A1, Def5;

        consider a2 be non negative Real, R2 be Equivalence_Relation of X such that

         A5: R2 = (( low_toler (f,a2)) [*] ) and

         A6: ( Class R2) = B by A2, Def5;

        now

          per cases ;

            suppose

             A7: a1 <= a2;

            now

              let x be set;

              assume x in A;

              then

              consider c be object such that

               A8: c in X and

               A9: x = ( Class (R1,c)) by A4, EQREL_1:def 3;

              consider y be set such that

               A10: y = ( Class (R2,c));

              take y;

              thus y in B by A6, A8, A10, EQREL_1:def 3;

              thus x c= y by A3, A5, A7, A9, A10, Lm2;

            end;

            hence thesis;

          end;

            suppose

             A11: a1 > a2;

            now

              let y be set;

              assume y in B;

              then

              consider c be object such that

               A12: c in X and

               A13: y = ( Class (R2,c)) by A6, EQREL_1:def 3;

              consider x be set such that

               A14: x = ( Class (R1,c));

              take x;

              thus x in A by A4, A12, A14, EQREL_1:def 3;

              thus y c= x by A3, A5, A11, A13, A14, Lm2;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis by Def1;

    end;

    theorem :: TAXONOM1:32

    for X be finite non empty Subset of REAL , f be Function of [:X, X:], REAL st ( SmallestPartition X) in ( fam_class f) & f is symmetric nonnegative holds ( fam_class f) is Strong_Classification of X

    proof

      let X be finite non empty Subset of REAL , f be Function of [:X, X:], REAL such that

       A1: ( SmallestPartition X) in ( fam_class f) and

       A2: f is symmetric nonnegative;

      

       A3: ( fam_class f) is Classification of X by Th31;

       {X} in ( fam_class f) by A2, Th30;

      hence thesis by A1, A3, Def2;

    end;

    begin

    definition

      let M be MetrStruct, a be Real, x,y be Element of M;

      :: TAXONOM1:def6

      pred x,y are_in_tolerance_wrt a means ( dist (x,y)) <= a;

    end

    definition

      let M be non empty MetrStruct, a be Real;

      :: TAXONOM1:def7

      func dist_toler (M,a) -> Relation of M means

      : Def7: for x,y be Element of M holds [x, y] in it iff (x,y) are_in_tolerance_wrt a;

      existence

      proof

        defpred X[ Element of M, Element of M] means ($1,$2) are_in_tolerance_wrt a;

        consider R be Relation of the carrier of M, the carrier of M such that

         A1: for x,y be Element of M holds [x, y] in R iff X[x, y] from RELSET_1:sch 2;

        reconsider R as Relation of M;

        take R;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let A,B be Relation of M such that

         A2: for x,y be Element of M holds [x, y] in A iff (x,y) are_in_tolerance_wrt a and

         A3: for x,y be Element of M holds [x, y] in B iff (x,y) are_in_tolerance_wrt a;

        

         A4: for c,d be object holds [c, d] in B implies [c, d] in A

        proof

          let c,d be object;

          assume

           A5: [c, d] in B;

          then

          reconsider c1 = c, d1 = d as Element of M by ZFMISC_1: 87;

          (c1,d1) are_in_tolerance_wrt a by A3, A5;

          hence thesis by A2;

        end;

        for c,d be object holds [c, d] in A implies [c, d] in B

        proof

          let c,d be object;

          assume

           A6: [c, d] in A;

          then

          reconsider c1 = c, d1 = d as Element of M by ZFMISC_1: 87;

          (c1,d1) are_in_tolerance_wrt a by A2, A6;

          hence thesis by A3;

        end;

        hence thesis by A4, RELAT_1:def 2;

      end;

    end

    theorem :: TAXONOM1:33

    

     Th33: for M be non empty MetrStruct, a be Real holds ( dist_toler (M,a)) = ( low_toler (the distance of M,a))

    proof

      let M be non empty MetrStruct, a be Real;

      now

        let z be object such that

         A1: z in ( low_toler (the distance of M,a));

        consider x,y be object such that

         A2: x in the carrier of M & y in the carrier of M and

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

        reconsider x1 = x, y1 = y as Element of M by A2;

        ( dist (x1,y1)) = (the distance of M . (x1,y1)) by METRIC_1:def 1;

        then ( dist (x1,y1)) <= a by A1, A3, Def3;

        then (x1,y1) are_in_tolerance_wrt a;

        hence z in ( dist_toler (M,a)) by A3, Def7;

      end;

      then

       A4: ( low_toler (the distance of M,a)) c= ( dist_toler (M,a));

      now

        let z be object such that

         A5: z in ( dist_toler (M,a));

        consider x,y be object such that

         A6: x in the carrier of M & y in the carrier of M and

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

        reconsider x1 = x, y1 = y as Element of M by A6;

        (the distance of M . (x1,y1)) = ( dist (x1,y1)) & (x1,y1) are_in_tolerance_wrt a by A5, A7, Def7, METRIC_1:def 1;

        then (the distance of M . (x1,y1)) <= a;

        hence z in ( low_toler (the distance of M,a)) by A7, Def3;

      end;

      then ( dist_toler (M,a)) c= ( low_toler (the distance of M,a));

      hence thesis by A4, XBOOLE_0:def 10;

    end;

    theorem :: TAXONOM1:34

    for M be non empty Reflexive symmetric MetrStruct, a be Real, T be Relation of the carrier of M, the carrier of M st T = ( dist_toler (M,a)) & a >= 0 holds T is Tolerance of the carrier of M

    proof

      let M be non empty Reflexive symmetric MetrStruct, a be Real, T be Relation of the carrier of M, the carrier of M such that

       A1: T = ( dist_toler (M,a)) and

       A2: a >= 0 ;

      

       A3: the distance of M is symmetric & the distance of M is Reflexive by METRIC_1:def 6, METRIC_1:def 8;

      T = ( low_toler (the distance of M,a)) by A1, Th33;

      hence thesis by A2, A3, Th18;

    end;

    definition

      let M be Reflexive symmetric non empty MetrStruct;

      :: TAXONOM1:def8

      func fam_class_metr (M) -> Subset of ( PARTITIONS the carrier of M) means

      : Def8: for x be object holds x in it iff ex a be non negative Real, R be Equivalence_Relation of M st R = (( dist_toler (M,a)) [*] ) & ( Class R) = x;

      existence

      proof

        defpred X[ object] means ex a be non negative Real, R be Equivalence_Relation of M st R = (( dist_toler (M,a)) [*] ) & ( Class R) = $1;

        consider X be set such that

         A1: for x be object holds x in X iff x in ( PARTITIONS the carrier of M) & X[x] from XBOOLE_0:sch 1;

        X c= ( PARTITIONS the carrier of M) by A1;

        then

        reconsider X1 = X as Subset of ( PARTITIONS the carrier of M);

        take X1;

        let x be object;

        thus x in X1 implies ex a be non negative Real, R be Equivalence_Relation of M st R = (( dist_toler (M,a)) [*] ) & ( Class R) = x by A1;

        given a be non negative Real, R be Equivalence_Relation of M such that

         A2: R = (( dist_toler (M,a)) [*] ) & ( Class R) = x;

        ( Class R) in ( PARTITIONS the carrier of M) by PARTIT1:def 3;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        defpred X[ object] means ex a be non negative Real, R be Equivalence_Relation of M st R = (( dist_toler (M,a)) [*] ) & ( Class R) = $1;

        

         A3: for X1,X2 be Subset of ( PARTITIONS the carrier of M) st (for x be object holds x in X1 iff X[x]) & (for x be object holds x in X2 iff X[x]) holds X1 = X2 from LMOD_7:sch 1;

        let X1,X2 be Subset of ( PARTITIONS the carrier of M);

        assume (for x be object holds x in X1 iff ex a be non negative Real, R be Equivalence_Relation of M st R = (( dist_toler (M,a)) [*] ) & ( Class R) = x) & (for x be object holds x in X2 iff ex a be non negative Real, R be Equivalence_Relation of M st R = (( dist_toler (M,a)) [*] ) & ( Class R) = x);

        hence thesis by A3;

      end;

    end

    theorem :: TAXONOM1:35

    

     Th35: for M be Reflexive symmetric non empty MetrStruct holds ( fam_class_metr M) = ( fam_class the distance of M)

    proof

      let M be Reflexive symmetric non empty MetrStruct;

      now

        let z be object;

        assume z in ( fam_class the distance of M);

        then

        consider a be non negative Real, R be Equivalence_Relation of the carrier of M such that

         A1: R = (( low_toler (the distance of M,a)) [*] ) and

         A2: ( Class R) = z by Def5;

        reconsider R1 = R as Equivalence_Relation of M;

        R1 = (( dist_toler (M,a)) [*] ) by A1, Th33;

        hence z in ( fam_class_metr M) by A2, Def8;

      end;

      then

       A3: ( fam_class the distance of M) c= ( fam_class_metr M);

      now

        let z be object;

        assume z in ( fam_class_metr M);

        then

        consider a be non negative Real, R be Equivalence_Relation of M such that

         A4: R = (( dist_toler (M,a)) [*] ) and

         A5: ( Class R) = z by Def8;

        R = (( low_toler (the distance of M,a)) [*] ) by A4, Th33;

        hence z in ( fam_class the distance of M) by A5, Def5;

      end;

      then ( fam_class_metr M) c= ( fam_class the distance of M);

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: TAXONOM1:36

    

     Th36: for M be non empty MetrSpace holds for R be Equivalence_Relation of M st R = (( dist_toler (M, 0 )) [*] ) holds ( Class R) = ( SmallestPartition the carrier of M)

    proof

      let M be non empty MetrSpace;

      now

        let x,y be Element of M;

        ( dist (x,y)) >= 0 by METRIC_1: 5;

        hence (the distance of M . (x,y)) >= 0 by METRIC_1:def 1;

      end;

      then

       A1: the distance of M is nonnegative;

      let R be Equivalence_Relation of M;

      assume R = (( dist_toler (M, 0 )) [*] );

      then the distance of M is Reflexive discerning & (( low_toler (the distance of M, 0 )) [*] ) = R by Th33, METRIC_1:def 6, METRIC_1:def 7;

      hence thesis by A1, Th24;

    end;

    theorem :: TAXONOM1:37

    

     Th37: for M be Reflexive symmetric bounded non empty MetrStruct st a >= ( diameter ( [#] M)) holds ( dist_toler (M,a)) = ( nabla the carrier of M)

    proof

      let M be Reflexive symmetric bounded non empty MetrStruct such that

       A1: a >= ( diameter ( [#] M));

      now

        let z be object;

        assume z in ( nabla the carrier of M);

        then

        consider x,y be object such that

         A2: x in the carrier of M & y in the carrier of M and

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

        reconsider x1 = x, y1 = y as Element of M by A2;

        ( dist (x1,y1)) <= ( diameter ( [#] M)) by TBSP_1:def 8;

        then ( dist (x1,y1)) <= a by A1, XXREAL_0: 2;

        then (x1,y1) are_in_tolerance_wrt a;

        hence z in ( dist_toler (M,a)) by A3, Def7;

      end;

      then ( nabla the carrier of M) c= ( dist_toler (M,a));

      hence thesis by XBOOLE_0:def 10;

    end;

    theorem :: TAXONOM1:38

    

     Th38: for M be Reflexive symmetric bounded non empty MetrStruct st a >= ( diameter ( [#] M)) holds ( dist_toler (M,a)) = (( dist_toler (M,a)) [*] )

    proof

      let M be Reflexive symmetric bounded non empty MetrStruct such that

       A1: a >= ( diameter ( [#] M));

      (( dist_toler (M,a)) [*] ) c= ( nabla the carrier of M);

      then ( dist_toler (M,a)) c= (( dist_toler (M,a)) [*] ) & (( dist_toler (M,a)) [*] ) c= ( dist_toler (M,a)) by A1, Th37, LANG1: 18;

      hence thesis by XBOOLE_0:def 10;

    end;

    theorem :: TAXONOM1:39

    

     Th39: for M be Reflexive symmetric bounded non empty MetrStruct st a >= ( diameter ( [#] M)) holds (( dist_toler (M,a)) [*] ) = ( nabla the carrier of M)

    proof

      let M be Reflexive symmetric bounded non empty MetrStruct such that

       A1: a >= ( diameter ( [#] M));

      ( dist_toler (M,a)) = (( dist_toler (M,a)) [*] ) by A1, Th38;

      hence thesis by A1, Th37;

    end;

    theorem :: TAXONOM1:40

    

     Th40: for M be Reflexive symmetric bounded non empty MetrStruct, R be Equivalence_Relation of M, a be non negative Real st a >= ( diameter ( [#] M)) & R = (( dist_toler (M,a)) [*] ) holds ( Class R) = {the carrier of M}

    proof

      let M be Reflexive symmetric bounded non empty MetrStruct, R be Equivalence_Relation of M, a be non negative Real such that

       A1: a >= ( diameter ( [#] M)) & R = (( dist_toler (M,a)) [*] );

      ( Class ( nabla the carrier of M)) = {the carrier of M} by MSUALG_9: 4;

      hence thesis by A1, Th39;

    end;

    registration

      let M be Reflexive symmetric triangle non empty MetrStruct, C be non empty bounded Subset of M;

      cluster ( diameter C) -> non negative;

      coherence by TBSP_1: 21;

    end

    theorem :: TAXONOM1:41

    

     Th41: for M be bounded non empty MetrSpace holds {the carrier of M} in ( fam_class_metr M)

    proof

      let M be bounded non empty MetrSpace;

      set a = ( diameter ( [#] M));

      the distance of M is symmetric by METRIC_1:def 8;

      then ( low_toler (the distance of M,a)) is_symmetric_in the carrier of M by Th17;

      then

       A1: ( dist_toler (M,a)) is_symmetric_in the carrier of M by Th33;

      the distance of M is Reflexive by METRIC_1:def 6;

      then ( low_toler (the distance of M,a)) is_reflexive_in the carrier of M by Th16;

      then ( dist_toler (M,a)) is_reflexive_in the carrier of M by Th33;

      then

      reconsider R = (( dist_toler (M,a)) [*] ) as Equivalence_Relation of M by A1, Th9;

      ( Class R) = {the carrier of M} by Th40;

      hence thesis by Def8;

    end;

    theorem :: TAXONOM1:42

    

     Th42: for M be Reflexive symmetric non empty MetrStruct holds ( fam_class_metr M) is Classification of the carrier of M

    proof

      let M be Reflexive symmetric non empty MetrStruct;

      ( fam_class_metr M) = ( fam_class the distance of M) by Th35;

      hence thesis by Th31;

    end;

    theorem :: TAXONOM1:43

    for M be bounded non empty MetrSpace holds ( fam_class_metr M) is Strong_Classification of the carrier of M

    proof

      reconsider a = 0 as non negative Real;

      let M be bounded non empty MetrSpace;

      the distance of M is symmetric by METRIC_1:def 8;

      then ( low_toler (the distance of M,a)) is_symmetric_in the carrier of M by Th17;

      then

       A1: ( dist_toler (M,a)) is_symmetric_in the carrier of M by Th33;

      the distance of M is Reflexive by METRIC_1:def 6;

      then ( low_toler (the distance of M,a)) is_reflexive_in the carrier of M by Th16;

      then ( dist_toler (M,a)) is_reflexive_in the carrier of M by Th33;

      then

      reconsider R = (( dist_toler (M,a)) [*] ) as Equivalence_Relation of M by A1, Th9;

      ( Class R) in ( fam_class_metr M) by Def8;

      then

       A2: ( SmallestPartition the carrier of M) in ( fam_class_metr M) by Th36;

      ( fam_class_metr M) is Classification of the carrier of M & {the carrier of M} in ( fam_class_metr M) by Th41, Th42;

      hence thesis by A2, Def2;

    end;