let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL holds fam_class f is Classification of X
let f be PartFunc of [:X,X:],REAL; :: thesis: fam_class f is Classification of X
for A, B being a_partition of X st A in fam_class f & B in fam_class f & not A is_finer_than B holds
B is_finer_than A
proof
let A, B be a_partition of X; :: thesis: ( A in fam_class f & B in fam_class f & not A is_finer_than B implies B is_finer_than A )
assume that
A1: A in fam_class f and
A2: B in fam_class f ; :: thesis: ( A is_finer_than B or B is_finer_than A )
consider a1 being non negative Real, R1 being Equivalence_Relation of X such that
A3: R1 = (low_toler (f,a1)) [*] and
A4: Class R1 = A by ;
consider a2 being non negative Real, R2 being Equivalence_Relation of X such that
A5: R2 = (low_toler (f,a2)) [*] and
A6: Class R2 = B by ;
now :: thesis: ( A is_finer_than B or B is_finer_than A )
per cases ( a1 <= a2 or a1 > a2 ) ;
suppose A7: a1 <= a2 ; :: thesis: ( A is_finer_than B or B is_finer_than A )
now :: thesis: for x being set st x in A holds
ex y being set st
( y in B & x c= y )
let x be set ; :: thesis: ( x in A implies ex y being set st
( y in B & x c= y ) )

assume x in A ; :: thesis: ex y being set st
( y in B & x c= y )

then consider c being object such that
A8: c in X and
A9: x = Class (R1,c) by ;
consider y being set such that
A10: y = Class (R2,c) ;
take y = y; :: thesis: ( y in B & x c= y )
thus y in B by ; :: thesis: x c= y
thus x c= y by A3, A5, A7, A9, A10, Lm2; :: thesis: verum
end;
hence ( A is_finer_than B or B is_finer_than A ) ; :: thesis: verum
end;
suppose A11: a1 > a2 ; :: thesis: ( A is_finer_than B or B is_finer_than A )
now :: thesis: for y being set st y in B holds
ex x being set st
( x in A & y c= x )
let y be set ; :: thesis: ( y in B implies ex x being set st
( x in A & y c= x ) )

assume y in B ; :: thesis: ex x being set st
( x in A & y c= x )

then consider c being object such that
A12: c in X and
A13: y = Class (R2,c) by ;
consider x being set such that
A14: x = Class (R1,c) ;
take x = x; :: thesis: ( x in A & y c= x )
thus x in A by ; :: thesis: y c= x
thus y c= x by A3, A5, A11, A13, A14, Lm2; :: thesis: verum
end;
hence ( A is_finer_than B or B is_finer_than A ) ; :: thesis: verum
end;
end;
end;
hence ( A is_finer_than B or B is_finer_than A ) ; :: thesis: verum
end;
hence fam_class f is Classification of X by Def1; :: thesis: verum