:: TAXONOM1 semantic presentation

begin


registration
clusterV11() ext-real non negative real for set ;
existence
 not for b1 being real number holds b1 is negative
proof
take  0 ; ::_thesis: not 0 is negative
thus  not 0 is negative ; ::_thesis: verum
end;
end;

theorem Th1: :: TAXONOM1:1
for p being FinSequence
for k being Nat st k + 1 in dom p & not k in dom p holds
k = 0
proof
let p be FinSequence; ::_thesis: for k being Nat st k + 1 in dom p & not k in dom p holds
k = 0
let k be Nat; ::_thesis: ( k + 1 in dom p & not k in dom p implies k = 0 )
assume that
A1: k + 1 in dom p and
A2: not k in dom p ; ::_thesis: k = 0
assume  k <> 0 ; ::_thesis: contradiction
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  contradiction by A2, A3, FINSEQ_3:25; ::_thesis: verum
end;

theorem Th2: :: TAXONOM1:2
for p being FinSequence
for i, j being Nat st i in dom p & j in dom p & ( for k being 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; ::_thesis: for i, j being Nat st i in dom p & j in dom p & ( for k being Nat st k in dom p & k + 1 in dom p holds
p . k = p . (k + 1) ) holds
p . i = p . j
let i, j be Nat; ::_thesis: ( i in dom p & j in dom p & ( for k being Nat st k in dom p & k + 1 in dom p holds
p . k = p . (k + 1) ) implies p . i = p . j )
assume that
A1: ( i in dom p & j in dom p ) and
A2: for k being Nat st k in dom p & k + 1 in dom p holds
p . k = p . (k + 1) ; ::_thesis: p . i = p . j
defpred S1[ Nat] means  for j being Nat st $1 in dom p & j in dom p holds
p . $1 = p . j;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
let j be Nat; ::_thesis: ( k + 1 in dom p & j in dom p implies p . (k + 1) = p . j )
assume that
A5: k + 1 in dom p and
A6: j in dom p ; ::_thesis: p . (k + 1) = p . j
percases ( k in dom p or not k in dom p ) ;
supposeA7: k in dom p ; ::_thesis: p . (k + 1) = p . j
hence p . (k + 1) = p . k by A2, A5
.= p . j by A4, A6, A7 ;
::_thesis: verum
end;
supposeA8: not k in dom p ; ::_thesis: p . (k + 1) = p . j
defpred S2[ Nat] means ( $1 in dom p implies p . $1 = p . 1 );
A9: for w being Nat st S2[w] holds
S2[w + 1]
proof
let w be Nat; ::_thesis: ( S2[w] implies S2[w + 1] )
assume A10: S2[w] ; ::_thesis: S2[w + 1]
assume A11: w + 1 in dom p ; ::_thesis: p . (w + 1) = p . 1
percases ( w in dom p or not w in dom p ) ;
suppose w in dom p ; ::_thesis: p . (w + 1) = p . 1
hence  p . (w + 1) = p . 1 by A2, A10, A11; ::_thesis: verum
end;
suppose not w in dom p ; ::_thesis: p . (w + 1) = p . 1
then  w = 0 by A11, Th1;
hence  p . (w + 1) = p . 1 ; ::_thesis: verum
end;
end;
end;
A12: S2[ 0 ] by FINSEQ_3:24;
A13: for k being Nat holds S2[k] from NAT_1:sch_2(A12, A9);
 k = 0 by A5, A8, Th1;
hence  p . (k + 1) = p . j by A6, A13; ::_thesis: verum
end;
end;
end;
A14: S1[ 0 ] by FINSEQ_3:24;
 for k being Nat holds S1[k] from NAT_1:sch_2(A14, A3);
hence  p . i = p . j by A1; ::_thesis: verum
end;

theorem Th3: :: TAXONOM1:3
for X being set
for R being Relation of X st R is_reflexive_in X holds
dom R = X
proof
let X be set ; ::_thesis: for R being Relation of X st R is_reflexive_in X holds
dom R = X
let R be Relation of X; ::_thesis: ( R is_reflexive_in X implies dom R = X )
assume A1: R is_reflexive_in X ; ::_thesis: dom R = X
 for x being set st x in X holds
ex y being set st [x,y] in R
proof
let x be set ; ::_thesis: ( x in X implies ex y being set st [x,y] in R )
assume A2: x in X ; ::_thesis: ex y being set st [x,y] in R
take  x ; ::_thesis: [x,x] in R
thus  [x,x] in R by A1, A2, RELAT_2:def_1; ::_thesis: verum
end;
hence  dom R = X by RELSET_1:9; ::_thesis: verum
end;

theorem :: TAXONOM1:4
for X being set
for R being Relation of X st R is_reflexive_in X holds
rng R = X
proof
let X be set ; ::_thesis: for R being Relation of X st R is_reflexive_in X holds
rng R = X
let R be Relation of X; ::_thesis: ( R is_reflexive_in X implies rng R = X )
assume A1: R is_reflexive_in X ; ::_thesis: rng R = X
 for x being set st x in X holds
ex y being set st [y,x] in R
proof
let x be set ; ::_thesis: ( x in X implies ex y being set st [y,x] in R )
assume A2: x in X ; ::_thesis: ex y being set st [y,x] in R
consider x1 being set  such that
A3: x1 = x ;
take  x1 ; ::_thesis: [x1,x] in R
thus  [x1,x] in R by A1, A2, A3, RELAT_2:def_1; ::_thesis: verum
end;
hence  rng R = X by RELSET_1:10; ::_thesis: verum
end;

theorem Th5: :: TAXONOM1:5
for X being set
for R being Relation of X st R is_reflexive_in X holds
R [*] is_reflexive_in X
proof
let X be set ; ::_thesis: for R being Relation of X st R is_reflexive_in X holds
R [*] is_reflexive_in X
let R be Relation of X; ::_thesis: ( R is_reflexive_in X implies R [*] is_reflexive_in X )
assume A1: R is_reflexive_in X ; ::_thesis: R [*] is_reflexive_in X
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
[x,x]_in_R_[*]
let x be set ; ::_thesis: ( x in X implies [x,x] in R [*] )
assume  x in X ; ::_thesis: [x,x] in R [*]
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; ::_thesis: verum
end;
hence  R [*] is_reflexive_in X by RELAT_2:def_1; ::_thesis: verum
end;

theorem Th6: :: TAXONOM1:6
for X, x, y being set
for R being Relation of X st R is_reflexive_in X & R reduces x,y & x in X holds
[x,y] in R [*]
proof
let X, x, y be set ; ::_thesis: for R being Relation of X st R is_reflexive_in X & R reduces x,y & x in X holds
[x,y] in R [*]
let R be Relation of X; ::_thesis: ( R is_reflexive_in X & R reduces x,y & x in X implies [x,y] in R [*] )
assume A1: R is_reflexive_in X ; ::_thesis: ( not R reduces x,y or not x in X or [x,y] in R [*] )
assume that
A2: R reduces x,y and
A3: x in X ; ::_thesis: [x,y] in R [*]
percases ( [x,y] in R [*] or x = y ) by A2, REWRITE1:20;
suppose [x,y] in R [*] ; ::_thesis: [x,y] in R [*]
hence  [x,y] in R [*] ; ::_thesis: verum
end;
supposeA4: x = y ; ::_thesis: [x,y] in R [*]
 R [*] is_reflexive_in X by A1, Th5;
hence  [x,y] in R [*] by A3, A4, RELAT_2:def_1; ::_thesis: verum
end;
end;
end;

theorem Th7: :: TAXONOM1:7
for X being set
for R being Relation of X st R is_symmetric_in X holds
R [*] is_symmetric_in X
proof
let X be set ; ::_thesis: for R being Relation of X st R is_symmetric_in X holds
R [*] is_symmetric_in X
let R be Relation of X; ::_thesis: ( R is_symmetric_in X implies R [*] is_symmetric_in X )
assume A1: R is_symmetric_in X ; ::_thesis: R [*] is_symmetric_in X
now__::_thesis:_for_x,_y_being_set_st_x_in_X_&_y_in_X_&_[x,y]_in_R_[*]_holds_
[y,x]_in_R_[*]
let x, y be set ; ::_thesis: ( x in X & y in X & [x,y] in R [*] implies [y,x] in R [*] )
assume that
 x in X and
 y in X and
A2: [x,y] in R [*] ; ::_thesis: [y,x] in R [*]
A3: ( x in field R & y in field R ) by A2, FINSEQ_1:def_16;
consider p being FinSequence such that
A4: len p >= 1 and
A5: p . 1 = x and
A6: p . (len p) = y and
A7: for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R by A2, FINSEQ_1:def_16;
consider r being FinSequence such that
A8: r = Rev p ;
A9: now__::_thesis:_for_j_being_Nat_st_j_>=_1_&_j_<_len_r_holds_
[(r_._j),(r_._(j_+_1))]_in_R
let j be Nat; ::_thesis: ( j >= 1 & j < len r implies [(r . j),(r . (j + 1))] in R )
assume that
A10: j >= 1 and
A11: j < len r ; ::_thesis: [(r . j),(r . (j + 1))] in 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 being 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; ::_thesis: verum
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; ::_thesis: verum
end;
hence  R [*] is_symmetric_in X by RELAT_2:def_3; ::_thesis: verum
end;

theorem Th8: :: TAXONOM1:8
for X being set
for R being Relation of X st R is_reflexive_in X holds
R [*] is_transitive_in X
proof
let X be set ; ::_thesis: for R being Relation of X st R is_reflexive_in X holds
R [*] is_transitive_in X
let R be Relation of X; ::_thesis: ( R is_reflexive_in X implies R [*] is_transitive_in X )
assume A1: R is_reflexive_in X ; ::_thesis: R [*] is_transitive_in X
now__::_thesis:_for_x,_y,_z_being_set_st_x_in_X_&_y_in_X_&_z_in_X_&_[x,y]_in_R_[*]_&_[y,z]_in_R_[*]_holds_
[x,z]_in_R_[*]
let x, y, z be set ; ::_thesis: ( x in X & y in X & z in X & [x,y] in R [*] & [y,z] in R [*] implies [x,z] in R [*] )
assume that
A2: x in X and
 y in X and
 z in X and
A3: ( [x,y] in R [*] & [y,z] in R [*] ) ; ::_thesis: [x,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; ::_thesis: verum
end;
hence  R [*] is_transitive_in X by RELAT_2:def_8; ::_thesis: verum
end;

theorem Th9: :: TAXONOM1:9
for X being non empty set
for R being 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 ; ::_thesis: for R being Relation of X st R is_reflexive_in X & R is_symmetric_in X holds
R [*] is Equivalence_Relation of X
let R be Relation of X; ::_thesis: ( R is_reflexive_in X & R is_symmetric_in X implies R [*] is Equivalence_Relation of X )
assume that
A1: R is_reflexive_in X and
A2: R is_symmetric_in X ; ::_thesis: R [*] is Equivalence_Relation of 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  R [*] is Equivalence_Relation of X by A3, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum
end;

theorem Th10: :: TAXONOM1:10
for X being non empty set
for R1, R2 being Relation of X st R1 c= R2 holds
R1 [*] c= R2 [*]
proof
let X be non empty set ; ::_thesis: for R1, R2 being Relation of X st R1 c= R2 holds
R1 [*] c= R2 [*]
let R1, R2 be Relation of X; ::_thesis: ( R1 c= R2 implies R1 [*] c= R2 [*] )
assume A1: R1 c= R2 ; ::_thesis: R1 [*] c= R2 [*]
now__::_thesis:_for_p_being_set_st_p_in_R1_[*]_holds_
p_in_R2_[*]
A2: field R1 c= field R2 by A1, RELAT_1:16;
let p be set ; ::_thesis: ( p in R1 [*] implies p in R2 [*] )
assume A3: p in R1 [*] ; ::_thesis: p in R2 [*]
consider x, y being set  such that
A4: p = [x,y] by A3, RELAT_1:def_1;
consider r being FinSequence such that
A5: ( len r >= 1 & r . 1 = x & r . (len r) = y ) and
A6: for i being Nat st i >= 1 & i < len r holds
[(r . i),(r . (i + 1))] in R1 by A3, A4, FINSEQ_1:def_16;
A7: now__::_thesis:_for_i_being_Nat_st_i_>=_1_&_i_<_len_r_holds_
[(r_._i),(r_._(i_+_1))]_in_R2
let i be Nat; ::_thesis: ( i >= 1 & i < len r implies [(r . i),(r . (i + 1))] in R2 )
assume  ( i >= 1 & i < len r ) ; ::_thesis: [(r . i),(r . (i + 1))] in R2
then  [(r . i),(r . (i + 1))] in R1 by A6;
hence  [(r . i),(r . (i + 1))] in R2 by A1; ::_thesis: verum
end;
 ( 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; ::_thesis: verum
end;
hence  R1 [*] c= R2 [*] by TARSKI:def_3; ::_thesis: verum
end;

Lm1: now__::_thesis:_for_A_being_non_empty_set_
for_X,_Y_being_a_partition_of_A_st_X_in_{{A}}_&_Y_in_{{A}}_&_not_X_is_finer_than_Y_holds_
Y_is_finer_than_X
let A be non empty set ; ::_thesis: for X, Y being a_partition of A st X in {{A}} & Y in {{A}} & not X is_finer_than Y holds
Y is_finer_than X
let X, Y be a_partition of A; ::_thesis: ( X in {{A}} & Y in {{A}} & not X is_finer_than Y implies Y is_finer_than X )
assume that
A1: X in {{A}} and
A2: Y in {{A}} ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X )
 X = {A} by A1, TARSKI:def_1;
hence  ( X is_finer_than Y or Y is_finer_than X ) by A2, TARSKI:def_1; ::_thesis: verum
end;

theorem Th11: :: TAXONOM1:11
for A being non empty set holds SmallestPartition A is_finer_than {A}
proof
let A be non empty set ; ::_thesis: SmallestPartition A is_finer_than {A}
let X be set ; :: according to SETFAM_1:def_2 ::_thesis: ( not X in SmallestPartition A or ex b1 being set st
( b1 in {A} & X c= b1 ) )
assume A1: X in SmallestPartition A ; ::_thesis: ex b1 being set st
( b1 in {A} & X c= b1 )
take  A ; ::_thesis: ( A in {A} & X c= A )
thus  ( A in {A} & X c= A ) by A1, TARSKI:def_1; ::_thesis: verum
end;

begin

definition
let A be non empty set ;
mode Classification of A ->  Subset of (PARTITIONS A) means :Def1: :: TAXONOM1:def 1
 for X, Y being a_partition of A st X in it & Y in it & not X is_finer_than Y holds
Y is_finer_than X;
existence
 ex b1 being Subset of (PARTITIONS A) st
for X, Y being a_partition of A st X in b1 & Y in b1 & not X is_finer_than Y holds
Y is_finer_than X
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 ; ::_thesis: for X, Y being a_partition of A st X in S & Y in S & not X is_finer_than Y holds
Y is_finer_than X
thus  for X, Y being a_partition of A st X in S & Y in S & not X is_finer_than Y holds
Y is_finer_than X by Lm1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Classification TAXONOM1:def_1_:_
 for A being non empty set
for b2 being Subset of (PARTITIONS A) holds
( b2 is Classification of A iff for X, Y being a_partition of A st X in b2 & Y in b2 & not X is_finer_than Y holds
Y is_finer_than X );

theorem :: TAXONOM1:12
for A being non empty set holds {{A}} is Classification of A
proof
let A be non empty set ; ::_thesis: {{A}} is Classification of A
 {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; :: according to TAXONOM1:def_1 ::_thesis: for Y being a_partition of A st X in S & Y in S & not X is_finer_than Y holds
Y is_finer_than X
thus  for Y being a_partition of A st X in S & Y in S & not X is_finer_than Y holds
Y is_finer_than X by Lm1; ::_thesis: verum
end;
hence  {{A}} is Classification of A ; ::_thesis: verum
end;

theorem :: TAXONOM1:13
for A being non empty set holds {(SmallestPartition A)} is Classification of A
proof
let A be non empty set ; ::_thesis: {(SmallestPartition A)} is Classification of A
 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; :: according to TAXONOM1:def_1 ::_thesis: ( X in S & Y in S & not X is_finer_than Y implies Y is_finer_than X )
assume that
A1: X in S and
A2: Y in S ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X )
 X = SmallestPartition A by A1, TARSKI:def_1;
hence  ( X is_finer_than Y or Y is_finer_than X ) by A2, TARSKI:def_1; ::_thesis: verum
end;
hence  {(SmallestPartition A)} is Classification of A ; ::_thesis: verum
end;

theorem Th14: :: TAXONOM1:14
for A being non empty set
for S being Subset of (PARTITIONS A) st S = {{A},(SmallestPartition A)} holds
S is Classification of A
proof
let A be non empty set ; ::_thesis: for S being Subset of (PARTITIONS A) st S = {{A},(SmallestPartition A)} holds
S is Classification of A
let S be Subset of (PARTITIONS A); ::_thesis: ( S = {{A},(SmallestPartition A)} implies S is Classification of A )
assume A1: S = {{A},(SmallestPartition A)} ; ::_thesis: S is Classification of A
let X, Y be a_partition of A; :: according to TAXONOM1:def_1 ::_thesis: ( X in S & Y in S & not X is_finer_than Y implies Y is_finer_than X )
assume that
A2: X in S and
A3: Y in S ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X )
percases ( X = {A} or X = SmallestPartition A ) by A1, A2, TARSKI:def_2;
supposeA4: X = {A} ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X )
percases ( Y = {A} or Y = SmallestPartition A ) by A1, A3, TARSKI:def_2;
suppose Y = {A} ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X )
hence  ( X is_finer_than Y or Y is_finer_than X ) by A4; ::_thesis: verum
end;
suppose Y = SmallestPartition A ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X )
hence  ( X is_finer_than Y or Y is_finer_than X ) by A4, Th11; ::_thesis: verum
end;
end;
end;
supposeA5: X = SmallestPartition A ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X )
percases ( Y = SmallestPartition A or Y = {A} ) by A1, A3, TARSKI:def_2;
suppose Y = SmallestPartition A ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X )
hence  ( X is_finer_than Y or Y is_finer_than X ) by A5; ::_thesis: verum
end;
suppose Y = {A} ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X )
hence  ( X is_finer_than Y or Y is_finer_than X ) by A5, Th11; ::_thesis: verum
end;
end;
end;
end;
end;

definition
let A be non empty set ;
mode Strong_Classification of A ->  Subset of (PARTITIONS A) means :Def2: :: TAXONOM1:def 2
( it is Classification of A & {A} in it & SmallestPartition A in it );
existence
 ex b1 being Subset of (PARTITIONS A) st
( b1 is Classification of A & {A} in b1 & SmallestPartition A in b1 )
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 ; ::_thesis: ( S is Classification of A & {A} in S & SmallestPartition A in S )
thus  ( S is Classification of A & {A} in S & SmallestPartition A in S ) by Th14, TARSKI:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Strong_Classification TAXONOM1:def_2_:_
 for A being non empty set
for b2 being Subset of (PARTITIONS A) holds
( b2 is Strong_Classification of A iff ( b2 is Classification of A & {A} in b2 & SmallestPartition A in b2 ) );

theorem :: TAXONOM1:15
for A being non empty set
for S being Subset of (PARTITIONS A) st S = {{A},(SmallestPartition A)} holds
S is Strong_Classification of A
proof
let A be non empty set ; ::_thesis: for S being Subset of (PARTITIONS A) st S = {{A},(SmallestPartition A)} holds
S is Strong_Classification of A
let S be Subset of (PARTITIONS A); ::_thesis: ( S = {{A},(SmallestPartition A)} implies S is Strong_Classification of A )
assume A1: S = {{A},(SmallestPartition A)} ; ::_thesis: S is Strong_Classification of 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  S is Strong_Classification of A by A2, Def2; ::_thesis: verum
end;

begin

definition
let X be non empty set ;
let f be PartFunc of [:X,X:],REAL;
let a be real number ;
func low_toler (f,a) ->  Relation of X means :Def3: :: TAXONOM1:def 3
 for x, y being Element of X holds
( [x,y] in it iff f . (x,y) <= a );
existence
 ex b1 being Relation of X st
for x, y being Element of X holds
( [x,y] in b1 iff f . (x,y) <= a )
proof
defpred S1[ Element of X, Element of X] means f . ($1,$2) <= a;
consider R being Relation of X,X such that
A1: for x, y being Element of X holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2();
take  R ; ::_thesis: for x, y being Element of X holds
( [x,y] in R iff f . (x,y) <= a )
thus  for x, y being Element of X holds
( [x,y] in R iff f . (x,y) <= a ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of X st ( for x, y being Element of X holds
( [x,y] in b1 iff f . (x,y) <= a ) ) & ( for x, y being Element of X holds
( [x,y] in b2 iff f . (x,y) <= a ) ) holds
b1 = b2
proof
let R1, R2 be Relation of X; ::_thesis: ( ( for x, y being Element of X holds
( [x,y] in R1 iff f . (x,y) <= a ) ) & ( for x, y being Element of X holds
( [x,y] in R2 iff f . (x,y) <= a ) ) implies R1 = R2 )
assume that
A2: for x, y being Element of X holds
( [x,y] in R1 iff f . (x,y) <= a ) and
A3: for x, y being Element of X holds
( [x,y] in R2 iff f . (x,y) <= a ) ; ::_thesis: R1 = R2
A4: for c, d being set st [c,d] in R2 holds
[c,d] in R1
proof
let c, d be set ; ::_thesis: ( [c,d] in R2 implies [c,d] in R1 )
assume A5: [c,d] in R2 ; ::_thesis: [c,d] in R1
then reconsider c1 = c, d1 = d as Element of X by ZFMISC_1:87;
 f . (c1,d1) <= a by A3, A5;
hence  [c,d] in R1 by A2; ::_thesis: verum
end;
 for c, d being set st [c,d] in R1 holds
[c,d] in R2
proof
let c, d be set ; ::_thesis: ( [c,d] in R1 implies [c,d] in R2 )
assume A6: [c,d] in R1 ; ::_thesis: [c,d] in R2
then reconsider c1 = c, d1 = d as Element of X by ZFMISC_1:87;
 f . (c1,d1) <= a by A2, A6;
hence  [c,d] in R2 by A3; ::_thesis: verum
end;
hence  R1 = R2 by A4, RELAT_1:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines low_toler TAXONOM1:def_3_:_
 for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being real number
for b4 being Relation of X holds
( b4 = low_toler (f,a) iff for x, y being Element of X holds
( [x,y] in b4 iff f . (x,y) <= a ) );

theorem Th16: :: TAXONOM1:16
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being real number st f is Reflexive & a >= 0 holds
low_toler (f,a) is_reflexive_in X
proof
let X be non empty set ; ::_thesis: for f being PartFunc of [:X,X:],REAL
for a being real number st f is Reflexive & a >= 0 holds
low_toler (f,a) is_reflexive_in X
let f be PartFunc of [:X,X:],REAL; ::_thesis: for a being real number st f is Reflexive & a >= 0 holds
low_toler (f,a) is_reflexive_in X
let a be real number ; ::_thesis: ( f is Reflexive & a >= 0 implies low_toler (f,a) is_reflexive_in X )
assume A1: ( f is Reflexive & a >= 0 ) ; ::_thesis: low_toler (f,a) is_reflexive_in X
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
[x,x]_in_low_toler_(f,a)
let x be set ; ::_thesis: ( x in X implies [x,x] in low_toler (f,a) )
assume  x in X ; ::_thesis: [x,x] in low_toler (f,a)
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; ::_thesis: verum
end;
hence  low_toler (f,a) is_reflexive_in X by RELAT_2:def_1; ::_thesis: verum
end;

theorem Th17: :: TAXONOM1:17
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being real number st f is symmetric holds
low_toler (f,a) is_symmetric_in X
proof
let X be non empty set ; ::_thesis: for f being PartFunc of [:X,X:],REAL
for a being real number st f is symmetric holds
low_toler (f,a) is_symmetric_in X
let f be PartFunc of [:X,X:],REAL; ::_thesis: for a being real number st f is symmetric holds
low_toler (f,a) is_symmetric_in X
let a be real number ; ::_thesis: ( f is symmetric implies low_toler (f,a) is_symmetric_in X )
assume A1: f is symmetric ; ::_thesis: low_toler (f,a) is_symmetric_in X
now__::_thesis:_for_x,_y_being_set_st_x_in_X_&_y_in_X_&_[x,y]_in_low_toler_(f,a)_holds_
[y,x]_in_low_toler_(f,a)
let x, y be set ; ::_thesis: ( x in X & y in X & [x,y] in low_toler (f,a) implies [y,x] in low_toler (f,a) )
assume that
A2: ( x in X & y in X ) and
A3: [x,y] in low_toler (f,a) ; ::_thesis: [y,x] 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; ::_thesis: verum
end;
hence  low_toler (f,a) is_symmetric_in X by RELAT_2:def_3; ::_thesis: verum
end;

theorem Th18: :: TAXONOM1:18
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being real number st a >= 0 & f is Reflexive & f is symmetric holds
low_toler (f,a) is Tolerance of X
proof
let X be non empty set ; ::_thesis: for f being PartFunc of [:X,X:],REAL
for a being real number st a >= 0 & f is Reflexive & f is symmetric holds
low_toler (f,a) is Tolerance of X
let f be PartFunc of [:X,X:],REAL; ::_thesis: for a being real number st a >= 0 & f is Reflexive & f is symmetric holds
low_toler (f,a) is Tolerance of X
let a be real number ; ::_thesis: ( a >= 0 & f is Reflexive & f is symmetric implies low_toler (f,a) is Tolerance of X )
set T = low_toler (f,a);
assume that
A1: a >= 0 and
A2: ( f is Reflexive & f is symmetric ) ; ::_thesis: low_toler (f,a) is Tolerance of X
A3: low_toler (f,a) is_reflexive_in X by A1, A2, Th16;
A4: dom (low_toler (f,a)) = X by A1, A2, Th3, Th16;
then A5: field (low_toler (f,a)) = X \/ (rng (low_toler (f,a))) by RELAT_1:def_6
.= X by XBOOLE_1:12 ;
then  low_toler (f,a) is_symmetric_in field (low_toler (f,a)) by A2, Th17;
hence  low_toler (f,a) is Tolerance of X by A3, A4, A5, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_11; ::_thesis: verum
end;

theorem Th19: :: TAXONOM1:19
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a1, a2 being real number st a1 <= a2 holds
low_toler (f,a1) c= low_toler (f,a2)
proof
let X be non empty set ; ::_thesis: for f being PartFunc of [:X,X:],REAL
for a1, a2 being real number st a1 <= a2 holds
low_toler (f,a1) c= low_toler (f,a2)
let f be PartFunc of [:X,X:],REAL; ::_thesis: for a1, a2 being real number st a1 <= a2 holds
low_toler (f,a1) c= low_toler (f,a2)
let a1, a2 be real number ; ::_thesis: ( a1 <= a2 implies low_toler (f,a1) c= low_toler (f,a2) )
assume A1: a1 <= a2 ; ::_thesis: low_toler (f,a1) c= low_toler (f,a2)
now__::_thesis:_for_p_being_set_st_p_in_low_toler_(f,a1)_holds_
p_in_low_toler_(f,a2)
let p be set ; ::_thesis: ( p in low_toler (f,a1) implies p in low_toler (f,a2) )
assume A2: p in low_toler (f,a1) ; ::_thesis: p in low_toler (f,a2)
consider x, y being set  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; ::_thesis: verum
end;
hence  low_toler (f,a1) c= low_toler (f,a2) by TARSKI:def_3; ::_thesis: verum
end;

definition
let X be set ;
let f be PartFunc of [:X,X:],REAL;
attrf is nonnegative  means :Def4: :: TAXONOM1:def 4
 for x, y being Element of X holds f . (x,y) >= 0 ;
end;

:: deftheorem Def4 defines nonnegative TAXONOM1:def_4_:_
 for X being set
for f being PartFunc of [:X,X:],REAL holds
( f is nonnegative iff for x, y being Element of X holds f . (x,y) >= 0 );

theorem Th20: :: TAXONOM1:20
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for x, y being set st f is nonnegative & f is Reflexive & f is discerning & [x,y] in low_toler (f,0) holds
x = y
proof
let X be non empty set ; ::_thesis: for f being PartFunc of [:X,X:],REAL
for x, y being set st f is nonnegative & f is Reflexive & f is discerning & [x,y] in low_toler (f,0) holds
x = y
let f be PartFunc of [:X,X:],REAL; ::_thesis: for x, y being set st f is nonnegative & f is Reflexive & f is discerning & [x,y] in low_toler (f,0) holds
x = y
let x, y be set ; ::_thesis: ( f is nonnegative & f is Reflexive & f is discerning & [x,y] in low_toler (f,0) implies x = y )
assume A1: ( f is nonnegative & f is Reflexive & f is discerning ) ; ::_thesis: ( not [x,y] in low_toler (f,0) or x = y )
assume A2: [x,y] in low_toler (f,0) ; ::_thesis: x = y
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, Def4;
hence  x = y by A1, METRIC_1:def_3; ::_thesis: verum
end;

theorem Th21: :: TAXONOM1:21
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for x being Element of X st f is Reflexive & f is discerning holds
[x,x] in low_toler (f,0)
proof
let X be non empty set ; ::_thesis: for f being PartFunc of [:X,X:],REAL
for x being Element of X st f is Reflexive & f is discerning holds
[x,x] in low_toler (f,0)
let f be PartFunc of [:X,X:],REAL; ::_thesis: for x being Element of X st f is Reflexive & f is discerning holds
[x,x] in low_toler (f,0)
let x be Element of X; ::_thesis: ( f is Reflexive & f is discerning implies [x,x] in low_toler (f,0) )
assume  ( f is Reflexive & f is discerning ) ; ::_thesis: [x,x] in low_toler (f,0)
then  f . (x,x) = 0 by METRIC_1:def_2;
hence  [x,x] in low_toler (f,0) by Def3; ::_thesis: verum
end;

theorem Th22: :: TAXONOM1:22
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being real number 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 ; ::_thesis: for f being PartFunc of [:X,X:],REAL
for a being real number st low_toler (f,a) is_reflexive_in X & f is symmetric holds
(low_toler (f,a)) [*] is Equivalence_Relation of X
let f be PartFunc of [:X,X:],REAL; ::_thesis: for a being real number st low_toler (f,a) is_reflexive_in X & f is symmetric holds
(low_toler (f,a)) [*] is Equivalence_Relation of X
let a be real number ; ::_thesis: ( low_toler (f,a) is_reflexive_in X & f is symmetric implies (low_toler (f,a)) [*] is Equivalence_Relation of X )
assume that
A1: low_toler (f,a) is_reflexive_in X and
A2: f is symmetric ; ::_thesis: (low_toler (f,a)) [*] is Equivalence_Relation of X
now__::_thesis:_for_x,_y_being_set_st_x_in_X_&_y_in_X_&_[x,y]_in_low_toler_(f,a)_holds_
[y,x]_in_low_toler_(f,a)
let x, y be set ; ::_thesis: ( x in X & y in X & [x,y] in low_toler (f,a) implies [y,x] in low_toler (f,a) )
assume that
A3: ( x in X & y in X ) and
A4: [x,y] in low_toler (f,a) ; ::_thesis: [y,x] 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; ::_thesis: verum
end;
then  low_toler (f,a) is_symmetric_in X by RELAT_2:def_3;
hence  (low_toler (f,a)) [*] is Equivalence_Relation of X by A1, Th9; ::_thesis: verum
end;

Lm2:  for x being set
for X being non empty set
for a1, a2 being non negative real number st a1 <= a2 holds
for f being PartFunc of [:X,X:],REAL
for R1, R2 being 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 set ; ::_thesis: for X being non empty set
for a1, a2 being non negative real number st a1 <= a2 holds
for f being PartFunc of [:X,X:],REAL
for R1, R2 being Equivalence_Relation of X st R1 = (low_toler (f,a1)) [*] & R2 = (low_toler (f,a2)) [*] holds
Class (R1,x) c= Class (R2,x)
let X be non empty set ; ::_thesis: for a1, a2 being non negative real number st a1 <= a2 holds
for f being PartFunc of [:X,X:],REAL
for R1, R2 being Equivalence_Relation of X st R1 = (low_toler (f,a1)) [*] & R2 = (low_toler (f,a2)) [*] holds
Class (R1,x) c= Class (R2,x)
let a1, a2 be non negative real number ; ::_thesis: ( a1 <= a2 implies for f being PartFunc of [:X,X:],REAL
for R1, R2 being Equivalence_Relation of X st R1 = (low_toler (f,a1)) [*] & R2 = (low_toler (f,a2)) [*] holds
Class (R1,x) c= Class (R2,x) )
assume A1: a1 <= a2 ; ::_thesis: for f being PartFunc of [:X,X:],REAL
for R1, R2 being Equivalence_Relation of X st R1 = (low_toler (f,a1)) [*] & R2 = (low_toler (f,a2)) [*] holds
Class (R1,x) c= Class (R2,x)
let f be PartFunc of [:X,X:],REAL; ::_thesis: for R1, R2 being Equivalence_Relation of X st R1 = (low_toler (f,a1)) [*] & R2 = (low_toler (f,a2)) [*] holds
Class (R1,x) c= Class (R2,x)
let R1, R2 be Equivalence_Relation of X; ::_thesis: ( R1 = (low_toler (f,a1)) [*] & R2 = (low_toler (f,a2)) [*] implies Class (R1,x) c= Class (R2,x) )
assume A2: ( R1 = (low_toler (f,a1)) [*] & R2 = (low_toler (f,a2)) [*] ) ; ::_thesis: Class (R1,x) c= Class (R2,x)
now__::_thesis:_for_z1_being_set_st_z1_in_Class_(R1,x)_holds_
z1_in_Class_(R2,x)
let z1 be set ; ::_thesis: ( z1 in Class (R1,x) implies z1 in Class (R2,x) )
assume  z1 in Class (R1,x) ; ::_thesis: z1 in Class (R2,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; ::_thesis: verum
end;
hence  Class (R1,x) c= Class (R2,x) by TARSKI:def_3; ::_thesis: verum
end;

begin

theorem Th23: :: TAXONOM1:23
for X being non empty set
for f being PartFunc of [:X,X:],REAL st f is nonnegative & f is Reflexive & f is discerning holds
(low_toler (f,0)) [*] = low_toler (f,0)
proof
let X be non empty set ; ::_thesis: for f being PartFunc of [:X,X:],REAL st f is nonnegative & f is Reflexive & f is discerning holds
(low_toler (f,0)) [*] = low_toler (f,0)
let f be PartFunc of [:X,X:],REAL; ::_thesis: ( f is nonnegative & f is Reflexive & f is discerning implies (low_toler (f,0)) [*] = low_toler (f,0) )
assume A1: ( f is nonnegative & f is Reflexive & f is discerning ) ; ::_thesis: (low_toler (f,0)) [*] = low_toler (f,0)
now__::_thesis:_for_p_being_set_st_p_in_(low_toler_(f,0))_[*]_holds_
p_in_low_toler_(f,0)
let p be set ; ::_thesis: ( p in (low_toler (f,0)) [*] implies p in low_toler (f,0) )
assume A2: p in (low_toler (f,0)) [*] ; ::_thesis: p in low_toler (f,0)
consider x, y being set  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 being RedSequence of low_toler (f,0) such that
A4: ( r . 1 = x & r . (len r) = y ) by REWRITE1:def_3;
A5: now__::_thesis:_for_i_being_Nat_st_i_in_dom_r_&_i_+_1_in_dom_r_holds_
r_._i_=_r_._(i_+_1)
let i be Nat; ::_thesis: ( i in dom r & i + 1 in dom r implies r . i = r . (i + 1) )
assume  ( i in dom r & i + 1 in dom r ) ; ::_thesis: r . i = r . (i + 1)
then  [(r . i),(r . (i + 1))] in low_toler (f,0) by REWRITE1:def_2;
hence  r . i = r . (i + 1) by A1, Th20; ::_thesis: verum
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; ::_thesis: verum
end;
then  ( low_toler (f,0) c= (low_toler (f,0)) [*] & (low_toler (f,0)) [*] c= low_toler (f,0) ) by LANG1:18, TARSKI:def_3;
hence  (low_toler (f,0)) [*] = low_toler (f,0) by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th24: :: TAXONOM1:24
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for R being Equivalence_Relation of X st R = (low_toler (f,0)) [*] & f is nonnegative & f is Reflexive & f is discerning holds
R = id X
proof
let X be non empty set ; ::_thesis: for f being PartFunc of [:X,X:],REAL
for R being Equivalence_Relation of X st R = (low_toler (f,0)) [*] & f is nonnegative & f is Reflexive & f is discerning holds
R = id X
let f be PartFunc of [:X,X:],REAL; ::_thesis: for R being Equivalence_Relation of X st R = (low_toler (f,0)) [*] & f is nonnegative & f is Reflexive & f is discerning holds
R = id X
let R be Equivalence_Relation of X; ::_thesis: ( R = (low_toler (f,0)) [*] & f is nonnegative & f is Reflexive & f is discerning implies R = id X )
assume that
A1: R = (low_toler (f,0)) [*] and
A2: ( f is nonnegative & f is Reflexive & f is discerning ) ; ::_thesis: R = id X
A3: for x, y being set st x in X & x = y holds
[x,y] in (low_toler (f,0)) [*]
proof
let x, y be set ; ::_thesis: ( x in X & x = y implies [x,y] in (low_toler (f,0)) [*] )
assume  ( x in X & x = y ) ; ::_thesis: [x,y] in (low_toler (f,0)) [*]
then  [x,y] in low_toler (f,0) by A2, Th21;
hence  [x,y] in (low_toler (f,0)) [*] by A2, Th23; ::_thesis: verum
end;
 for x, y being set st [x,y] in (low_toler (f,0)) [*] holds
( x in X & x = y )
proof
let x, y be set ; ::_thesis: ( [x,y] in (low_toler (f,0)) [*] implies ( x in X & x = y ) )
assume  [x,y] in (low_toler (f,0)) [*] ; ::_thesis: ( x in X & x = y )
then  [x,y] in low_toler (f,0) by A2, Th23;
hence  ( x in X & x = y ) by A2, Th20, ZFMISC_1:87; ::_thesis: verum
end;
hence  R = id X by A1, A3, RELAT_1:def_10; ::_thesis: verum
end;

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

theorem Th26: :: TAXONOM1:26
for X being non empty finite Subset of REAL
for f being Function of [:X,X:],REAL
for z being non empty finite Subset of REAL
for A being real number st z = rng f & A >= max z holds
for x, y being Element of X holds f . (x,y) <= A
proof
let X be non empty finite Subset of REAL; ::_thesis: for f being Function of [:X,X:],REAL
for z being non empty finite Subset of REAL
for A being real number st z = rng f & A >= max z holds
for x, y being Element of X holds f . (x,y) <= A
let f be Function of [:X,X:],REAL; ::_thesis: for z being non empty finite Subset of REAL
for A being real number st z = rng f & A >= max z holds
for x, y being Element of X holds f . (x,y) <= A
let z be non empty finite Subset of REAL; ::_thesis: for A being real number st z = rng f & A >= max z holds
for x, y being Element of X holds f . (x,y) <= A
let A be real number ; ::_thesis: ( z = rng f & A >= max z implies for x, y being Element of X holds f . (x,y) <= A )
assume that
A1: z = rng f and
A2: A >= max z ; ::_thesis: for x, y being Element of X holds f . (x,y) <= A
now__::_thesis:_for_x,_y_being_Element_of_X_holds_f_._(x,y)_<=_A
let x, y be Element of X; ::_thesis: f . (x,y) <= A
 f . [x,y] = f . (x,y) ;
then reconsider c = f . [x,y] as real number ;
 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; ::_thesis: verum
end;
hence  for x, y being Element of X holds f . (x,y) <= A ; ::_thesis: verum
end;

theorem Th27: :: TAXONOM1:27
for X being non empty finite Subset of REAL
for f being Function of [:X,X:],REAL
for z being non empty finite Subset of REAL
for A being real number st z = rng f & A >= max z holds
for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}
proof
let X be non empty finite Subset of REAL; ::_thesis: for f being Function of [:X,X:],REAL
for z being non empty finite Subset of REAL
for A being real number st z = rng f & A >= max z holds
for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}
let f be Function of [:X,X:],REAL; ::_thesis: for z being non empty finite Subset of REAL
for A being real number st z = rng f & A >= max z holds
for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}
let z be non empty finite Subset of REAL; ::_thesis: for A being real number st z = rng f & A >= max z holds
for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}
let A be real number ; ::_thesis: ( z = rng f & A >= max z implies for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X} )
assume A1: ( z = rng f & A >= max z ) ; ::_thesis: for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}
now__::_thesis:_for_R_being_Equivalence_Relation_of_X_st_R_=_(low_toler_(f,A))_[*]_holds_
Class_R_=_{X}
let R be Equivalence_Relation of X; ::_thesis: ( R = (low_toler (f,A)) [*] implies Class R = {X} )
assume A2: R = (low_toler (f,A)) [*] ; ::_thesis: Class R = {X}
A3: for x being set st x in X holds
X = Class (R,x)
proof
let x be set ; ::_thesis: ( x in X implies X = Class (R,x) )
assume  x in X ; ::_thesis: X = Class (R,x)
then reconsider x9 = x as Element of X ;
now__::_thesis:_for_x1_being_set_st_x1_in_X_holds_
x1_in_Class_(R,x)
let x1 be set ; ::_thesis: ( x1 in X implies x1 in Class (R,x) )
assume  x1 in X ; ::_thesis: x1 in Class (R,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; ::_thesis: verum
end;
then  X c= Class (R,x) by TARSKI:def_3;
hence  X = Class (R,x) by XBOOLE_0:def_10; ::_thesis: verum
end;
now__::_thesis:_for_a_being_set_st_a_in_{X}_holds_
a_in_Class_R
let a be set ; ::_thesis: ( a in {X} implies a in Class R )
assume  a in {X} ; ::_thesis: a in Class R
then A5: a = X by TARSKI:def_1;
consider x being set  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; ::_thesis: verum
end;
then A7: {X} c= Class R by TARSKI:def_3;
now__::_thesis:_for_a_being_set_st_a_in_Class_R_holds_
a_in_{X}
let a be set ; ::_thesis: ( a in Class R implies a in {X} )
assume  a in Class R ; ::_thesis: a in {X}
then  ex x being set 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; ::_thesis: verum
end;
then  Class R c= {X} by TARSKI:def_3;
hence  Class R = {X} by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X} ; ::_thesis: verum
end;

theorem :: TAXONOM1:28
for X being non empty finite Subset of REAL
for f being Function of [:X,X:],REAL
for z being non empty finite Subset of REAL
for A being real number st z = rng f & A >= max z holds
(low_toler (f,A)) [*] = low_toler (f,A)
proof
let X be non empty finite Subset of REAL; ::_thesis: for f being Function of [:X,X:],REAL
for z being non empty finite Subset of REAL
for A being real number st z = rng f & A >= max z holds
(low_toler (f,A)) [*] = low_toler (f,A)
let f be Function of [:X,X:],REAL; ::_thesis: for z being non empty finite Subset of REAL
for A being real number st z = rng f & A >= max z holds
(low_toler (f,A)) [*] = low_toler (f,A)
let z be non empty finite Subset of REAL; ::_thesis: for A being real number st z = rng f & A >= max z holds
(low_toler (f,A)) [*] = low_toler (f,A)
let A be real number ; ::_thesis: ( z = rng f & A >= max z implies (low_toler (f,A)) [*] = low_toler (f,A) )
assume A1: ( z = rng f & A >= max z ) ; ::_thesis: (low_toler (f,A)) [*] = low_toler (f,A)
now__::_thesis:_for_p_being_set_st_p_in_(low_toler_(f,A))_[*]_holds_
p_in_low_toler_(f,A)
let p be set ; ::_thesis: ( p in (low_toler (f,A)) [*] implies p in low_toler (f,A) )
assume  p in (low_toler (f,A)) [*] ; ::_thesis: p in low_toler (f,A)
then consider x, y being set  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; ::_thesis: verum
end;
then  ( low_toler (f,A) c= (low_toler (f,A)) [*] & (low_toler (f,A)) [*] c= low_toler (f,A) ) by LANG1:18, TARSKI:def_3;
hence  (low_toler (f,A)) [*] = low_toler (f,A) by XBOOLE_0:def_10; ::_thesis: verum
end;

begin

definition
let X be non empty set ;
let f be PartFunc of [:X,X:],REAL;
func fam_class f ->  Subset of (PARTITIONS X) means :Def5: :: TAXONOM1:def 5
 for x being set holds
( x in it iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) );
existence
 ex b1 being Subset of (PARTITIONS X) st
for x being set holds
( x in b1 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) )
proof
defpred S1[ set ] means  ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = $1 );
consider A being set  such that
A1: for x being set holds
( x in A iff ( x in PARTITIONS X & S1[x] ) ) from XBOOLE_0:sch_1();
 A c= PARTITIONS X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in PARTITIONS X )
assume  a in A ; ::_thesis: a in PARTITIONS X
hence  a in PARTITIONS X by A1; ::_thesis: verum
end;
then reconsider A1 = A as Subset of (PARTITIONS X) ;
take  A1 ; ::_thesis: for x being set holds
( x in A1 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) )
let x be set ; ::_thesis: ( x in A1 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) )
thus  ( x in A1 implies ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) ) by A1; ::_thesis: ( ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) implies x in A1 )
given a being non negative real number , R being Equivalence_Relation of X such that A2: ( R = (low_toler (f,a)) [*] & Class R = x ) ; ::_thesis: x in A1
 Class R in PARTITIONS X by PARTIT1:def_3;
hence  x in A1 by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of (PARTITIONS X) st ( for x being set holds
( x in b1 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) ) ) & ( for x being set holds
( x in b2 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = $1 );
A3: for X1, X2 being Subset of (PARTITIONS X) st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from LMOD_7:sch_1();
let X1, X2 be Subset of (PARTITIONS X); ::_thesis: ( ( for x being set holds
( x in X1 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) ) ) & ( for x being set holds
( x in X2 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) ) ) implies X1 = X2 )
assume  ( ( for x being set holds
( x in X1 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) ) ) & ( for x being set holds
( x in X2 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) ) ) ) ; ::_thesis: X1 = X2
hence  X1 = X2 by A3; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines fam_class TAXONOM1:def_5_:_
 for X being non empty set
for f being PartFunc of [:X,X:],REAL
for b3 being Subset of (PARTITIONS X) holds
( b3 = fam_class f iff for x being set holds
( x in b3 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) ) );

theorem :: TAXONOM1:29
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being non negative real number 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 ; ::_thesis: for f being PartFunc of [:X,X:],REAL
for a being non negative real number st low_toler (f,a) is_reflexive_in X & f is symmetric holds
fam_class f is non empty set
let f be PartFunc of [:X,X:],REAL; ::_thesis: for a being non negative real number st low_toler (f,a) is_reflexive_in X & f is symmetric holds
fam_class f is non empty set
let a be non negative real number ; ::_thesis: ( low_toler (f,a) is_reflexive_in X & f is symmetric implies fam_class f is non empty set )
assume  ( low_toler (f,a) is_reflexive_in X & f is symmetric ) ; ::_thesis: fam_class f is non empty set
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  fam_class f is non empty set ; ::_thesis: verum
end;

theorem Th30: :: TAXONOM1:30
for X being non empty finite Subset of REAL
for f being Function of [:X,X:],REAL st f is symmetric & f is nonnegative holds
{X} in fam_class f
proof
let X be non empty finite Subset of REAL; ::_thesis: for f being Function of [:X,X:],REAL st f is symmetric & f is nonnegative holds
{X} in fam_class f
let f be Function of [:X,X:],REAL; ::_thesis: ( f is symmetric & f is nonnegative implies {X} in fam_class f )
assume A1: ( f is symmetric & f is nonnegative ) ; ::_thesis: {X} in fam_class f
 dom f = [:X,X:] by FUNCT_2:def_1;
then reconsider rn = rng f as non empty finite Subset of REAL by RELAT_1:42;
reconsider A1 = max rn as real number ;
now__::_thesis:_not_A1_is_negative
set x = the Element of X;
assume A2: A1 is negative ; ::_thesis: contradiction
 f . ( the Element of X, the Element of X) <= A1 by Th26;
hence  contradiction by A1, A2, Def4; ::_thesis: verum
end;
then reconsider A19 = A1 as non negative real number ;
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
[x,x]_in_low_toler_(f,A1)
let x be set ; ::_thesis: ( x in X implies [x,x] in low_toler (f,A1) )
assume  x in X ; ::_thesis: [x,x] in low_toler (f,A1)
then reconsider x1 = x as Element of X ;
 f . (x1,x1) <= A1 by Th26;
hence  [x,x] in low_toler (f,A1) by Def3; ::_thesis: verum
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  {X} in fam_class f by Th27; ::_thesis: verum
end;

theorem Th31: :: TAXONOM1:31
for X being non empty set
for f being PartFunc of [:X,X:],REAL holds fam_class f is Classification of X
proof
let X be non empty set ; ::_thesis: for f being PartFunc of [:X,X:],REAL holds fam_class f is Classification of X
let f be PartFunc of [:X,X:],REAL; ::_thesis: fam_class f is Classification of X
 for A, B being a_partition of X st A in fam_class f & B in fam_class f & not A is_finer_than B holds
B is_finer_than A
proof
let A, B be a_partition of X; ::_thesis: ( A in fam_class f & B in fam_class f & not A is_finer_than B implies B is_finer_than A )
assume that
A1: A in fam_class f and
A2: B in fam_class f ; ::_thesis: ( A is_finer_than B or B is_finer_than A )
consider a1 being non negative real number , R1 being Equivalence_Relation of X such that
A3: R1 = (low_toler (f,a1)) [*] and
A4: Class R1 = A by A1, Def5;
consider a2 being non negative real number , R2 being Equivalence_Relation of X such that
A5: R2 = (low_toler (f,a2)) [*] and
A6: Class R2 = B by A2, Def5;
now__::_thesis:_(_A_is_finer_than_B_or_B_is_finer_than_A_)
percases ( a1 <= a2 or a1 > a2 ) ;
supposeA7: a1 <= a2 ; ::_thesis: ( A is_finer_than B or B is_finer_than A )
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
ex_y_being_set_st_
(_y_in_B_&_x_c=_y_)
let x be set ; ::_thesis: ( x in A implies ex y being set st
( y in B & x c= y ) )
assume  x in A ; ::_thesis: ex y being set st
( y in B & x c= y )
then consider c being set  such that
A8: c in X and
A9: x = Class (R1,c) by A4, EQREL_1:def_3;
consider y being set  such that
A10: y = Class (R2,c) ;
take y = y; ::_thesis: ( y in B & x c= y )
thus  y in B by A6, A8, A10, EQREL_1:def_3; ::_thesis: x c= y
thus  x c= y by A3, A5, A7, A9, A10, Lm2; ::_thesis: verum
end;
hence  ( A is_finer_than B or B is_finer_than A ) by SETFAM_1:def_2; ::_thesis: verum
end;
supposeA11: a1 > a2 ; ::_thesis: ( A is_finer_than B or B is_finer_than A )
now__::_thesis:_for_y_being_set_st_y_in_B_holds_
ex_x_being_set_st_
(_x_in_A_&_y_c=_x_)
let y be set ; ::_thesis: ( y in B implies ex x being set st
( x in A & y c= x ) )
assume  y in B ; ::_thesis: ex x being set st
( x in A & y c= x )
then consider c being set  such that
A12: c in X and
A13: y = Class (R2,c) by A6, EQREL_1:def_3;
consider x being set  such that
A14: x = Class (R1,c) ;
take x = x; ::_thesis: ( x in A & y c= x )
thus  x in A by A4, A12, A14, EQREL_1:def_3; ::_thesis: y c= x
thus  y c= x by A3, A5, A11, A13, A14, Lm2; ::_thesis: verum
end;
hence  ( A is_finer_than B or B is_finer_than A ) by SETFAM_1:def_2; ::_thesis: verum
end;
end;
end;
hence  ( A is_finer_than B or B is_finer_than A ) ; ::_thesis: verum
end;
hence  fam_class f is Classification of X by Def1; ::_thesis: verum
end;

theorem :: TAXONOM1:32
for X being non empty finite Subset of REAL
for f being Function of [:X,X:],REAL st SmallestPartition X in fam_class f & f is symmetric & f is nonnegative holds
fam_class f is Strong_Classification of X
proof
let X be non empty finite Subset of REAL; ::_thesis: for f being Function of [:X,X:],REAL st SmallestPartition X in fam_class f & f is symmetric & f is nonnegative holds
fam_class f is Strong_Classification of X
let f be Function of [:X,X:],REAL; ::_thesis: ( SmallestPartition X in fam_class f & f is symmetric & f is nonnegative implies fam_class f is Strong_Classification of X )
assume that
A1: SmallestPartition X in fam_class f and
A2: ( f is symmetric & f is nonnegative ) ; ::_thesis: fam_class f is Strong_Classification of X
A3: fam_class f is Classification of X by Th31;
 {X} in fam_class f by A2, Th30;
hence  fam_class f is Strong_Classification of X by A1, A3, Def2; ::_thesis: verum
end;

begin

definition
let M be MetrStruct ;
let a be real number ;
let x, y be Element of M;
predx,y are_in_tolerance_wrt a means :Def6: :: TAXONOM1:def 6
 dist (x,y) <= a;
end;

:: deftheorem Def6 defines are_in_tolerance_wrt TAXONOM1:def_6_:_
 for M being MetrStruct
for a being real number
for x, y being Element of M holds
( x,y are_in_tolerance_wrt a iff dist (x,y) <= a );

definition
let M be non empty MetrStruct ;
let a be real number ;
func dist_toler (M,a) ->  Relation of M means :Def7: :: TAXONOM1:def 7
 for x, y being Element of M holds
( [x,y] in it iff x,y are_in_tolerance_wrt a );
existence
 ex b1 being Relation of M st
for x, y being Element of M holds
( [x,y] in b1 iff x,y are_in_tolerance_wrt a )
proof
defpred S1[ Element of M, Element of M] means $1,$2 are_in_tolerance_wrt a;
consider R being Relation of the carrier of M, the carrier of M such that
A1: for x, y being Element of M holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2();
reconsider R = R as Relation of M ;
take  R ; ::_thesis: for x, y being Element of M holds
( [x,y] in R iff x,y are_in_tolerance_wrt a )
thus  for x, y being Element of M holds
( [x,y] in R iff x,y are_in_tolerance_wrt a ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of M st ( for x, y being Element of M holds
( [x,y] in b1 iff x,y are_in_tolerance_wrt a ) ) & ( for x, y being Element of M holds
( [x,y] in b2 iff x,y are_in_tolerance_wrt a ) ) holds
b1 = b2
proof
let A, B be Relation of M; ::_thesis: ( ( for x, y being Element of M holds
( [x,y] in A iff x,y are_in_tolerance_wrt a ) ) & ( for x, y being Element of M holds
( [x,y] in B iff x,y are_in_tolerance_wrt a ) ) implies A = B )
assume that
A2: for x, y being Element of M holds
( [x,y] in A iff x,y are_in_tolerance_wrt a ) and
A3: for x, y being Element of M holds
( [x,y] in B iff x,y are_in_tolerance_wrt a ) ; ::_thesis: A = B
A4: for c, d being set st [c,d] in B holds
[c,d] in A
proof
let c, d be set ; ::_thesis: ( [c,d] in B implies [c,d] in A )
assume A5: [c,d] in B ; ::_thesis: [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 A3, A5;
hence  [c,d] in A by A2; ::_thesis: verum
end;
 for c, d being set st [c,d] in A holds
[c,d] in B
proof
let c, d be set ; ::_thesis: ( [c,d] in A implies [c,d] in B )
assume A6: [c,d] in A ; ::_thesis: [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 A2, A6;
hence  [c,d] in B by A3; ::_thesis: verum
end;
hence  A = B by A4, RELAT_1:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines dist_toler TAXONOM1:def_7_:_
 for M being non empty MetrStruct
for a being real number
for b3 being Relation of M holds
( b3 = dist_toler (M,a) iff for x, y being Element of M holds
( [x,y] in b3 iff x,y are_in_tolerance_wrt a ) );

theorem Th33: :: TAXONOM1:33
for M being non empty MetrStruct
for a being real number holds dist_toler (M,a) = low_toler ( the distance of M,a)
proof
let M be non empty MetrStruct ; ::_thesis: for a being real number holds dist_toler (M,a) = low_toler ( the distance of M,a)
let a be real number ; ::_thesis: dist_toler (M,a) = low_toler ( the distance of M,a)
now__::_thesis:_for_z_being_set_st_z_in_low_toler_(_the_distance_of_M,a)_holds_
z_in_dist_toler_(M,a)
let z be set ; ::_thesis: ( z in low_toler ( the distance of M,a) implies z in dist_toler (M,a) )
assume A1: z in low_toler ( the distance of M,a) ; ::_thesis: z in dist_toler (M,a)
consider x, y being set  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 by Def6;
hence  z in dist_toler (M,a) by A3, Def7; ::_thesis: verum
end;
then A4: low_toler ( the distance of M,a) c= dist_toler (M,a) by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_dist_toler_(M,a)_holds_
z_in_low_toler_(_the_distance_of_M,a)
let z be set ; ::_thesis: ( z in dist_toler (M,a) implies z in low_toler ( the distance of M,a) )
assume A5: z in dist_toler (M,a) ; ::_thesis: z in low_toler ( the distance of M,a)
consider x, y being set  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 by Def6;
hence  z in low_toler ( the distance of M,a) by A7, Def3; ::_thesis: verum
end;
then  dist_toler (M,a) c= low_toler ( the distance of M,a) by TARSKI:def_3;
hence  dist_toler (M,a) = low_toler ( the distance of M,a) by A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: TAXONOM1:34
for M being non empty Reflexive symmetric MetrStruct
for a being real number
for T being 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 ; ::_thesis: for a being real number
for T being 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
let a be real number ; ::_thesis: for T being 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
let T be Relation of the carrier of M, the carrier of M; ::_thesis: ( T = dist_toler (M,a) & a >= 0 implies T is Tolerance of the carrier of M )
assume that
A1: T = dist_toler (M,a) and
A2: a >= 0 ; ::_thesis: T is Tolerance of the carrier of M
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  T is Tolerance of the carrier of M by A2, A3, Th18; ::_thesis: verum
end;

definition
let M be non empty Reflexive symmetric MetrStruct ;
func fam_class_metr M ->  Subset of (PARTITIONS the carrier of M) means :Def8: :: TAXONOM1:def 8
 for x being set holds
( x in it iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = x ) );
existence
 ex b1 being Subset of (PARTITIONS the carrier of M) st
for x being set holds
( x in b1 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = x ) )
proof
defpred S1[ set ] means  ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = $1 );
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in PARTITIONS the carrier of M & S1[x] ) ) from XBOOLE_0:sch_1();
 X c= PARTITIONS the carrier of M
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in PARTITIONS the carrier of M )
assume  a in X ; ::_thesis: a in PARTITIONS the carrier of M
hence  a in PARTITIONS the carrier of M by A1; ::_thesis: verum
end;
then reconsider X1 = X as Subset of (PARTITIONS the carrier of M) ;
take  X1 ; ::_thesis: for x being set holds
( x in X1 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = x ) )
let x be set ; ::_thesis: ( x in X1 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = x ) )
thus  ( x in X1 implies ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = x ) ) by A1; ::_thesis: ( ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = x ) implies x in X1 )
given a being non negative real number , R being Equivalence_Relation of M such that A2: ( R = (dist_toler (M,a)) [*] & Class R = x ) ; ::_thesis: x in X1
 Class R in PARTITIONS the carrier of M by PARTIT1:def_3;
hence  x in X1 by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of (PARTITIONS the carrier of M) st ( for x being set holds
( x in b1 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) & ( for x being set holds
( x in b2 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = $1 );
A3: for X1, X2 being Subset of (PARTITIONS the carrier of M) st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from LMOD_7:sch_1();
let X1, X2 be Subset of (PARTITIONS the carrier of M); ::_thesis: ( ( for x being set holds
( x in X1 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) & ( for x being set holds
( x in X2 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) implies X1 = X2 )
assume  ( ( for x being set holds
( x in X1 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) & ( for x being set holds
( x in X2 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) ) ; ::_thesis: X1 = X2
hence  X1 = X2 by A3; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines fam_class_metr TAXONOM1:def_8_:_
 for M being non empty Reflexive symmetric MetrStruct
for b2 being Subset of (PARTITIONS the carrier of M) holds
( b2 = fam_class_metr M iff for x being set holds
( x in b2 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] & Class R = x ) ) );

theorem Th35: :: TAXONOM1:35
for M being non empty Reflexive symmetric MetrStruct holds fam_class_metr M = fam_class the distance of M
proof
let M be non empty Reflexive symmetric MetrStruct ; ::_thesis: fam_class_metr M = fam_class the distance of M
now__::_thesis:_for_z_being_set_st_z_in_fam_class_the_distance_of_M_holds_
z_in_fam_class_metr_M
let z be set ; ::_thesis: ( z in fam_class the distance of M implies z in fam_class_metr M )
assume  z in fam_class the distance of M ; ::_thesis: z in fam_class_metr M
then consider a being non negative real number , R being 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; ::_thesis: verum
end;
then A3: fam_class the distance of M c= fam_class_metr M by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_fam_class_metr_M_holds_
z_in_fam_class_the_distance_of_M
let z be set ; ::_thesis: ( z in fam_class_metr M implies z in fam_class the distance of M )
assume  z in fam_class_metr M ; ::_thesis: z in fam_class the distance of M
then consider a being non negative real number , R being 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; ::_thesis: verum
end;
then  fam_class_metr M c= fam_class the distance of M by TARSKI:def_3;
hence  fam_class_metr M = fam_class the distance of M by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th36: :: TAXONOM1:36
for M being non empty MetrSpace
for R being 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; ::_thesis: for R being Equivalence_Relation of M st R = (dist_toler (M,0)) [*] holds
Class R = SmallestPartition the carrier of M
now__::_thesis:_for_x,_y_being_Element_of_M_holds_the_distance_of_M_._(x,y)_>=_0
let x, y be Element of M; ::_thesis: the distance of M . (x,y) >= 0
 dist (x,y) >= 0 by METRIC_1:5;
hence  the distance of M . (x,y) >= 0 by METRIC_1:def_1; ::_thesis: verum
end;
then A1: the distance of M is nonnegative by Def4;
let R be Equivalence_Relation of M; ::_thesis: ( R = (dist_toler (M,0)) [*] implies Class R = SmallestPartition the carrier of M )
assume  R = (dist_toler (M,0)) [*] ; ::_thesis: Class R = SmallestPartition the carrier of M
then  ( the distance of M is Reflexive & the distance of M is discerning & (low_toler ( the distance of M,0)) [*] = R ) by Th33, METRIC_1:def_6, METRIC_1:def_7;
hence  Class R = SmallestPartition the carrier of M by A1, Th24; ::_thesis: verum
end;

theorem Th37: :: TAXONOM1:37
for a being real number
for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds
dist_toler (M,a) = nabla the carrier of M
proof
let a be real number ; ::_thesis: for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds
dist_toler (M,a) = nabla the carrier of M
let M be non empty Reflexive symmetric bounded MetrStruct ; ::_thesis: ( a >= diameter ([#] M) implies dist_toler (M,a) = nabla the carrier of M )
assume A1: a >= diameter ([#] M) ; ::_thesis: dist_toler (M,a) = nabla the carrier of M
now__::_thesis:_for_z_being_set_st_z_in_nabla_the_carrier_of_M_holds_
z_in_dist_toler_(M,a)
let z be set ; ::_thesis: ( z in nabla the carrier of M implies z in dist_toler (M,a) )
assume  z in nabla the carrier of M ; ::_thesis: z in dist_toler (M,a)
then consider x, y being set  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 by Def6;
hence  z in dist_toler (M,a) by A3, Def7; ::_thesis: verum
end;
then  nabla the carrier of M c= dist_toler (M,a) by TARSKI:def_3;
hence  dist_toler (M,a) = nabla the carrier of M by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th38: :: TAXONOM1:38
for a being real number
for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds
dist_toler (M,a) = (dist_toler (M,a)) [*]
proof
let a be real number ; ::_thesis: for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds
dist_toler (M,a) = (dist_toler (M,a)) [*]
let M be non empty Reflexive symmetric bounded MetrStruct ; ::_thesis: ( a >= diameter ([#] M) implies dist_toler (M,a) = (dist_toler (M,a)) [*] )
assume A1: a >= diameter ([#] M) ; ::_thesis: dist_toler (M,a) = (dist_toler (M,a)) [*]
 (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  dist_toler (M,a) = (dist_toler (M,a)) [*] by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th39: :: TAXONOM1:39
for a being real number
for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds
(dist_toler (M,a)) [*] = nabla the carrier of M
proof
let a be real number ; ::_thesis: for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds
(dist_toler (M,a)) [*] = nabla the carrier of M
let M be non empty Reflexive symmetric bounded MetrStruct ; ::_thesis: ( a >= diameter ([#] M) implies (dist_toler (M,a)) [*] = nabla the carrier of M )
assume A1: a >= diameter ([#] M) ; ::_thesis: (dist_toler (M,a)) [*] = nabla the carrier of M
 dist_toler (M,a) = (dist_toler (M,a)) [*] by A1, Th38;
hence  (dist_toler (M,a)) [*] = nabla the carrier of M by A1, Th37; ::_thesis: verum
end;

theorem Th40: :: TAXONOM1:40
for M being non empty Reflexive symmetric bounded MetrStruct
for R being Equivalence_Relation of M
for a being non negative real number st a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] holds
Class R = { the carrier of M}
proof
let M be non empty Reflexive symmetric bounded MetrStruct ; ::_thesis: for R being Equivalence_Relation of M
for a being non negative real number st a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] holds
Class R = { the carrier of M}
let R be Equivalence_Relation of M; ::_thesis: for a being non negative real number st a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] holds
Class R = { the carrier of M}
let a be non negative real number ; ::_thesis: ( a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] implies Class R = { the carrier of M} )
assume A1: ( a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] ) ; ::_thesis: Class R = { the carrier of M}
 Class (nabla the carrier of M) = { the carrier of M} by MSUALG_9:4;
hence  Class R = { the carrier of M} by A1, Th39; ::_thesis: verum
end;

registration
let M be non empty Reflexive symmetric triangle MetrStruct ;
let C be non empty bounded Subset of M;
cluster diameter C ->  non negative ;
coherence
 not diameter C is negative by TBSP_1:21;
end;

theorem Th41: :: TAXONOM1:41
for M being non empty bounded MetrSpace holds { the carrier of M} in fam_class_metr M
proof
let M be non empty bounded MetrSpace; ::_thesis: { the carrier of M} in fam_class_metr M
set a = diameter ([#] M);
 the distance of M is symmetric by METRIC_1:def_8;
then  low_toler ( the distance of M,(diameter ([#] M))) is_symmetric_in the carrier of M by Th17;
then A1: dist_toler (M,(diameter ([#] M))) 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,(diameter ([#] M))) is_reflexive_in the carrier of M by Th16;
then  dist_toler (M,(diameter ([#] M))) is_reflexive_in the carrier of M by Th33;
then reconsider R = (dist_toler (M,(diameter ([#] M)))) [*] as Equivalence_Relation of M by A1, Th9;
 Class R = { the carrier of M} by Th40;
hence  { the carrier of M} in fam_class_metr M by Def8; ::_thesis: verum
end;

theorem Th42: :: TAXONOM1:42
for M being non empty Reflexive symmetric MetrStruct holds fam_class_metr M is Classification of the carrier of M
proof
let M be non empty Reflexive symmetric MetrStruct ; ::_thesis: fam_class_metr M is Classification of the carrier of M
 fam_class_metr M = fam_class the distance of M by Th35;
hence  fam_class_metr M is Classification of the carrier of M by Th31; ::_thesis: verum
end;

theorem :: TAXONOM1:43
for M being non empty bounded MetrSpace holds fam_class_metr M is Strong_Classification of the carrier of M
proof
reconsider a = 0 as non negative real number ;
let M be non empty bounded MetrSpace; ::_thesis: fam_class_metr M is Strong_Classification of the carrier of 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 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  fam_class_metr M is Strong_Classification of the carrier of M by A2, Def2; ::_thesis: verum
end;