TAXONOM1

:: TAXONOM1 semantic presentation

begin

registration

cluster V11() ext-real non negative real for ( ( ) ( ) set ) ;

end;

theorem :: TAXONOM1:2

theorem :: TAXONOM1:3

for X being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) is_reflexive_in X : ( ( ) ( ) set ) holds
dom R : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = X : ( ( ) ( ) set ) ;

theorem :: TAXONOM1:4

for X being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) is_reflexive_in X : ( ( ) ( ) set ) holds
rng R : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = X : ( ( ) ( ) set ) ;

theorem :: TAXONOM1:5

for X being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) is_reflexive_in X : ( ( ) ( ) set ) holds
R : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) [*] : ( ( Relation-like ) ( Relation-like ) set ) is_reflexive_in X : ( ( ) ( ) set ) ;

theorem :: TAXONOM1:6

for X, x, y being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) is_reflexive_in X : ( ( ) ( ) set ) & R : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) reduces x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) holds
[x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in R : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) [*] : ( ( Relation-like ) ( Relation-like ) set ) ;

theorem :: TAXONOM1:7

for X being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) is_symmetric_in X : ( ( ) ( ) set ) holds
R : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) [*] : ( ( Relation-like ) ( Relation-like ) set ) is_symmetric_in X : ( ( ) ( ) set ) ;

theorem :: TAXONOM1:8

for X being ( ( ) ( ) set )
for R being ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) is_reflexive_in X : ( ( ) ( ) set ) holds
R : ( ( ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) Relation of ) [*] : ( ( Relation-like ) ( Relation-like ) set ) is_transitive_in X : ( ( ) ( ) set ) ;

theorem :: TAXONOM1:9

for X being ( ( non empty ) ( non empty ) set )
for R being ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) st R : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is_reflexive_in X : ( ( non empty ) ( non empty ) set ) & R : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) is_symmetric_in X : ( ( non empty ) ( non empty ) set ) holds
R : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) [*] : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is ( ( total symmetric transitive ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) ;

theorem :: TAXONOM1:10

for X being ( ( non empty ) ( non empty ) set )
for R1, R2 being ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) st R1 : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) c= R2 : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) holds
R1 : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) [*] : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= R2 : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) [*] : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TAXONOM1:11

for A being ( ( non empty ) ( non empty ) set ) holds SmallestPartition A : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b₁ : ( ( non empty ) ( non empty ) set ) ) is_finer_than {A : ( ( non empty ) ( non empty ) set ) } : ( ( ) ( non empty finite ) set ) ;

begin

definition

let A be ( ( non empty ) ( non empty ) set ) ;

mode Classification of A -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) means :: TAXONOM1:def 1
for X, Y being ( ( ) ( non empty with_non-empty_elements ) a_partition of A : ( ( ) ( ) MetrStruct ) ) st X : ( ( ) ( non empty with_non-empty_elements ) a_partition of A : ( ( non empty ) ( non empty ) set ) ) in it : ( ( Function-like V29([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Element of bool [:[:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & Y : ( ( ) ( non empty with_non-empty_elements ) a_partition of A : ( ( non empty ) ( non empty ) set ) ) in it : ( ( Function-like V29([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Element of bool [:[:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & not X : ( ( ) ( non empty with_non-empty_elements ) a_partition of A : ( ( non empty ) ( non empty ) set ) ) is_finer_than Y : ( ( ) ( non empty with_non-empty_elements ) a_partition of A : ( ( non empty ) ( non empty ) set ) ) holds
Y : ( ( ) ( non empty with_non-empty_elements ) a_partition of A : ( ( non empty ) ( non empty ) set ) ) is_finer_than X : ( ( ) ( non empty with_non-empty_elements ) a_partition of A : ( ( non empty ) ( non empty ) set ) ) ;

end;

theorem :: TAXONOM1:12

for A being ( ( non empty ) ( non empty ) set ) holds {{A : ( ( non empty ) ( non empty ) set ) } : ( ( ) ( non empty finite ) set ) } : ( ( ) ( non empty finite V48() ) set ) is ( ( ) ( ) Classification of A : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: TAXONOM1:13

for A being ( ( non empty ) ( non empty ) set ) holds {(SmallestPartition A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b₁ : ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) is ( ( ) ( ) Classification of A : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: TAXONOM1:14

for A being ( ( non empty ) ( non empty ) set )
for S being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st S : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {{A : ( ( non empty ) ( non empty ) set ) } : ( ( ) ( non empty finite ) set ) ,(SmallestPartition A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b₁ : ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) holds
S : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Classification of A : ( ( non empty ) ( non empty ) set ) ) ;

definition

let A be ( ( non empty ) ( non empty ) set ) ;

mode Strong_Classification of A -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) means :: TAXONOM1:def 2
( it : ( ( Function-like V29([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Element of bool [:[:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Classification of A : ( ( ) ( ) MetrStruct ) ) & {A : ( ( ) ( ) MetrStruct ) } : ( ( ) ( non empty finite ) set ) in it : ( ( Function-like V29([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Element of bool [:[:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & SmallestPartition A : ( ( ) ( ) MetrStruct ) : ( ( ) ( with_non-empty_elements ) a_partition of A : ( ( ) ( ) MetrStruct ) ) in it : ( ( Function-like V29([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Element of bool [:[:A : ( ( ) ( ) MetrStruct ) ,A : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) );

end;

theorem :: TAXONOM1:15

for A being ( ( non empty ) ( non empty ) set )
for S being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st S : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = {{A : ( ( non empty ) ( non empty ) set ) } : ( ( ) ( non empty finite ) set ) ,(SmallestPartition A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b₁ : ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) set ) holds
S : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Strong_Classification of A : ( ( non empty ) ( non empty ) set ) ) ;

begin

definition

let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like ) ( Relation-like [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) ;
let a be ( ( real ) ( V11() ext-real real ) number ) ;

func low_toler (f,a) -> ( ( ) ( Relation-like X : ( ( ) ( ) MetrStruct ) -defined X : ( ( ) ( ) MetrStruct ) -valued ) Relation of ) means :: TAXONOM1:def 3
for x, y being ( ( ) ( ) Element of X : ( ( ) ( ) MetrStruct ) ) holds
( [x : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in it : ( ( natural ) ( natural V11() ext-real real ) set ) iff f : ( ( Function-like V29([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Element of bool [:[:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . (x : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) <= a : ( ( ) ( ) Element of X : ( ( ) ( ) MetrStruct ) ) );

end;

theorem :: TAXONOM1:16

theorem :: TAXONOM1:17

theorem :: TAXONOM1:18

theorem :: TAXONOM1:19

definition

let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like ) ( Relation-like [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) ;

attr f is nonnegative means :: TAXONOM1:def 4
for x, y being ( ( ) ( ) Element of X : ( ( ) ( ) MetrStruct ) ) holds f : ( ( Function-like V29([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Element of bool [:[:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . (x : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) ,y : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) >= 0 : ( ( ) ( empty natural V11() ext-real non positive non negative finite V48() real V106() V107() V108() V109() V110() V111() V112() bounded_below bounded_above real-bounded interval ) Element of NAT : ( ( ) ( V106() V107() V108() V109() V110() V111() V112() bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ;

end;

theorem :: TAXONOM1:20

theorem :: TAXONOM1:21

theorem :: TAXONOM1:22

begin

theorem :: TAXONOM1:23

for X being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) is nonnegative & f : ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) is Reflexive & f : ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) is discerning holds
(low_toler (f : ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) ,0 : ( ( ) ( empty natural V11() ext-real non positive non negative finite V48() real V106() V107() V108() V109() V110() V111() V112() bounded_below bounded_above real-bounded interval ) Element of NAT : ( ( ) ( V106() V107() V108() V109() V110() V111() V112() bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) [*] : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = low_toler (f : ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) ,0 : ( ( ) ( empty natural V11() ext-real non positive non negative finite V48() real V106() V107() V108() V109() V110() V111() V112() bounded_below bounded_above real-bounded interval ) Element of NAT : ( ( ) ( V106() V107() V108() V109() V110() V111() V112() bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) ;

theorem :: TAXONOM1:24

for X being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,)
for R being ( ( total symmetric transitive ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) st R : ( ( total symmetric transitive ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) = (low_toler (f : ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) ,0 : ( ( ) ( empty natural V11() ext-real non positive non negative finite V48() real V106() V107() V108() V109() V110() V111() V112() bounded_below bounded_above real-bounded interval ) Element of NAT : ( ( ) ( V106() V107() V108() V109() V110() V111() V112() bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) [*] : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) is nonnegative & f : ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) is Reflexive & f : ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) is discerning holds
R : ( ( total symmetric transitive ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) = id X : ( ( non empty ) ( non empty ) set ) : ( ( Relation-like ) ( non empty Relation-like ) set ) ;

theorem :: TAXONOM1:25

for X being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,)
for R being ( ( total symmetric transitive ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) st R : ( ( total symmetric transitive ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) = (low_toler (f : ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) ,0 : ( ( ) ( empty natural V11() ext-real non positive non negative finite V48() real V106() V107() V108() V109() V110() V111() V112() bounded_below bounded_above real-bounded interval ) Element of NAT : ( ( ) ( V106() V107() V108() V109() V110() V111() V112() bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ) [*] : ( ( ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) is nonnegative & f : ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) is Reflexive & f : ( ( Function-like ) ( Relation-like [:b₁ : ( ( non empty ) ( non empty ) set ) ,b₁ : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like ) PartFunc of ,) is discerning holds
Class R : ( ( total symmetric transitive ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b₁ : ( ( non empty ) ( non empty ) set ) ) = SmallestPartition X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b₁ : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: TAXONOM1:26

for X being ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:X : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,X : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) )
for z being ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) )
for A being ( ( real ) ( V11() ext-real real ) number ) st z : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) = rng f : ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V106() V107() V108() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) & A : ( ( real ) ( V11() ext-real real ) number ) >= max z : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ext-real ) ( V11() ext-real real ) set ) holds
for x, y being ( ( ) ( V11() ext-real real ) Element of X : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ) holds f : ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) . (x : ( ( ) ( V11() ext-real real ) Element of b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ) ,y : ( ( ) ( V11() ext-real real ) Element of b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) <= A : ( ( real ) ( V11() ext-real real ) number ) ;

theorem :: TAXONOM1:27

theorem :: TAXONOM1:28

for X being ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:X : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,X : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) )
for z being ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) )
for A being ( ( real ) ( V11() ext-real real ) number ) st z : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) = rng f : ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V106() V107() V108() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) & A : ( ( real ) ( V11() ext-real real ) number ) >= max z : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ext-real ) ( V11() ext-real real ) set ) holds
(low_toler (f : ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ,A : ( ( real ) ( V11() ext-real real ) number ) )) : ( ( ) ( Relation-like b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) -defined b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) -valued ) Relation of ) [*] : ( ( ) ( Relation-like b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) -defined b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) -valued ) Element of bool [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) : ( ( ) ( non empty ) set ) ) = low_toler (f : ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ,A : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( Relation-like b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) -defined b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) -valued ) Relation of ) ;

begin

definition

func fam_class f -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) means :: TAXONOM1:def 5
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) Element of X : ( ( ) ( ) MetrStruct ) ) iff ex a being ( ( non negative real ) ( V11() ext-real non negative real ) number ) ex R being ( ( total symmetric transitive ) ( Relation-like X : ( ( ) ( ) MetrStruct ) -defined X : ( ( ) ( ) MetrStruct ) -valued total symmetric transitive ) Equivalence_Relation of ) st
( R : ( ( total symmetric transitive ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) = (low_toler (f : ( ( Function-like V29([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Element of bool [:[:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( Relation-like X : ( ( ) ( ) MetrStruct ) -defined X : ( ( ) ( ) MetrStruct ) -valued ) Relation of ) [*] : ( ( ) ( Relation-like X : ( ( ) ( ) MetrStruct ) -defined X : ( ( ) ( ) MetrStruct ) -valued ) Element of bool [:X : ( ( ) ( ) MetrStruct ) ,X : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & Class R : ( ( total symmetric transitive ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) : ( ( ) ( with_non-empty_elements ) a_partition of X : ( ( ) ( ) MetrStruct ) ) = x : ( ( ) ( ) set ) ) );

end;

theorem :: TAXONOM1:29

theorem :: TAXONOM1:30

for X being ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:X : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,X : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) st f : ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) is symmetric & f : ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) is nonnegative holds
{X : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite V48() ) set ) in fam_class f : ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: TAXONOM1:31

theorem :: TAXONOM1:32

for X being ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:X : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,X : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) st SmallestPartition X : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ) in fam_class f : ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & f : ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) is symmetric & f : ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) is nonnegative holds
fam_class f : ( ( Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Function of [:b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ,b₁ : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty finite ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Strong_Classification of X : ( ( non empty finite ) ( non empty finite V106() V107() V108() left_end right_end bounded_below bounded_above real-bounded ) Subset of ( ( ) ( non empty ) set ) ) ) ;

begin

definition

let M be ( ( ) ( ) MetrStruct ) ;
let a be ( ( real ) ( V11() ext-real real ) number ) ;
let x, y be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

pred x,y are_in_tolerance_wrt a means :: TAXONOM1:def 6
dist (x : ( ( ) ( ) Element of M : ( ( ) ( ) MetrStruct ) ) ,y : ( ( natural ) ( natural V11() ext-real real ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) <= a : ( ( Function-like V29([:M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Element of bool [:[:M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

definition

let M be ( ( non empty ) ( non empty ) MetrStruct ) ;
let a be ( ( real ) ( V11() ext-real real ) number ) ;

func dist_toler (M,a) -> ( ( ) ( Relation-like the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) -defined the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) -valued ) Relation of ) means :: TAXONOM1:def 7
for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( [x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in it : ( ( ) ( ) Element of M : ( ( ) ( ) MetrStruct ) ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) are_in_tolerance_wrt a : ( ( Function-like V29([:M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Element of bool [:[:M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) );

end;

theorem :: TAXONOM1:33

for M being ( ( non empty ) ( non empty ) MetrStruct )
for a being ( ( real ) ( V11() ext-real real ) number ) holds dist_toler (M : ( ( non empty ) ( non empty ) MetrStruct ) ,a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Relation of ) = low_toler ( the distance of M : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( Function-like V29([: the carrier of b₁ : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([: the carrier of b₁ : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Element of bool [:[: the carrier of b₁ : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Relation of ) ;

theorem :: TAXONOM1:34

for M being ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct )
for a being ( ( real ) ( V11() ext-real real ) number )
for T being ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Relation of ,) st T : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Relation of ,) = dist_toler (M : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) ,a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Relation of ) & a : ( ( real ) ( V11() ext-real real ) number ) >= 0 : ( ( ) ( empty natural V11() ext-real non positive non negative finite V48() real V106() V107() V108() V109() V110() V111() V112() bounded_below bounded_above real-bounded interval ) Element of NAT : ( ( ) ( V106() V107() V108() V109() V110() V111() V112() bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) holds
T : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Relation of ,) is ( ( total reflexive symmetric ) ( Relation-like the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued total reflexive symmetric ) Tolerance of ) ;

definition

let M be ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) ;

func fam_class_metr M -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) means :: TAXONOM1:def 8
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( Function-like V29([:M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [:M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([:M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Element of bool [:[:M : ( ( ) ( ) MetrStruct ) ,M : ( ( ) ( ) MetrStruct ) :] : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) iff ex a being ( ( non negative real ) ( V11() ext-real non negative real ) number ) ex R being ( ( total symmetric transitive ) ( Relation-like the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) -defined the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) st
( R : ( ( total symmetric transitive ) ( Relation-like the carrier of M : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of M : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) = (dist_toler (M : ( ( ) ( ) MetrStruct ) ,a : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( Relation-like the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) -defined the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) -valued ) Relation of ) [*] : ( ( ) ( Relation-like the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) -defined the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) , the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & Class R : ( ( total symmetric transitive ) ( Relation-like the carrier of M : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of M : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) : ( ( ) ( with_non-empty_elements ) a_partition of the carrier of M : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) = x : ( ( ) ( ) set ) ) );

end;

theorem :: TAXONOM1:35

for M being ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) holds fam_class_metr M : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = fam_class the distance of M : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( Function-like V29([: the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like [: the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) -valued Function-like V29([: the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) ) Element of bool [:[: the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty Reflexive symmetric ) ( non empty Reflexive symmetric ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: TAXONOM1:36

theorem :: TAXONOM1:37

for a being ( ( real ) ( V11() ext-real real ) number )
for M being ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) st a : ( ( real ) ( V11() ext-real real ) number ) >= diameter ([#] M : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) ) : ( ( ) ( non empty non proper bounded ) Element of bool the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) holds
dist_toler (M : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) ,a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Relation of ) = nabla the carrier of M : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued total reflexive symmetric transitive ) Element of bool [: the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TAXONOM1:38

for a being ( ( real ) ( V11() ext-real real ) number )
for M being ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) st a : ( ( real ) ( V11() ext-real real ) number ) >= diameter ([#] M : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) ) : ( ( ) ( non empty non proper bounded ) Element of bool the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) holds
dist_toler (M : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) ,a : ( ( real ) ( V11() ext-real real ) number ) ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Relation of ) = (dist_toler (M : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) ,a : ( ( real ) ( V11() ext-real real ) number ) )) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Relation of ) [*] : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TAXONOM1:39

for a being ( ( real ) ( V11() ext-real real ) number )
for M being ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) st a : ( ( real ) ( V11() ext-real real ) number ) >= diameter ([#] M : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) ) : ( ( ) ( non empty non proper bounded ) Element of bool the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) holds
(dist_toler (M : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) ,a : ( ( real ) ( V11() ext-real real ) number ) )) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Relation of ) [*] : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = nabla the carrier of M : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( Relation-like the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued total reflexive symmetric transitive ) Element of bool [: the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: TAXONOM1:40

for M being ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct )
for R being ( ( total symmetric transitive ) ( Relation-like the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of )
for a being ( ( non negative real ) ( V11() ext-real non negative real ) number ) st a : ( ( non negative real ) ( V11() ext-real non negative real ) number ) >= diameter ([#] M : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) ) : ( ( ) ( non empty non proper bounded ) Element of bool the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) & R : ( ( total symmetric transitive ) ( Relation-like the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) = (dist_toler (M : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) ,a : ( ( non negative real ) ( V11() ext-real non negative real ) number ) )) : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Relation of ) [*] : ( ( ) ( Relation-like the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
Class R : ( ( total symmetric transitive ) ( Relation-like the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued total symmetric transitive ) Equivalence_Relation of ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of the carrier of b₁ : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) ) = { the carrier of M : ( ( non empty Reflexive symmetric bounded ) ( non empty Reflexive symmetric bounded ) MetrStruct ) : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite ) set ) ;

registration

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

cluster diameter C : ( ( non empty bounded ) ( non empty bounded ) Element of bool the carrier of M : ( ( non empty Reflexive symmetric triangle ) ( non empty Reflexive symmetric triangle ) MetrStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() ext-real real ) Element of REAL : ( ( ) ( non empty non trivial non finite V106() V107() V108() V112() non bounded_below non bounded_above interval ) set ) ) -> non negative ;

end;

theorem :: TAXONOM1:41

for M being ( ( non empty Reflexive discerning symmetric triangle bounded ) ( non empty Reflexive discerning symmetric triangle bounded ) MetrSpace) holds { the carrier of M : ( ( non empty Reflexive discerning symmetric triangle bounded ) ( non empty Reflexive discerning symmetric triangle bounded ) MetrSpace) : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite ) set ) in fam_class_metr M : ( ( non empty Reflexive discerning symmetric triangle bounded ) ( non empty Reflexive discerning symmetric triangle bounded ) MetrSpace) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: TAXONOM1:42

theorem :: TAXONOM1:43

for M being ( ( non empty Reflexive discerning symmetric triangle bounded ) ( non empty Reflexive discerning symmetric triangle bounded ) MetrSpace) holds fam_class_metr M : ( ( non empty Reflexive discerning symmetric triangle bounded ) ( non empty Reflexive discerning symmetric triangle bounded ) MetrSpace) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is ( ( ) ( ) Strong_Classification of the carrier of M : ( ( non empty Reflexive discerning symmetric triangle bounded ) ( non empty Reflexive discerning symmetric triangle bounded ) MetrSpace) : ( ( ) ( non empty ) set ) ) ;