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 A1, Def5;
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 A2, Def5;

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 A4, EQREL_1:def 3;
consider y being set such that
A10: y = Class (R2,c) ;
take y = y; :: thesis: ( y in B & x c= y )
thus y in B by A6, A8, A10, EQREL_1:def 3; :: thesis: x c= y
thus x c= y by A3, A5, A7, A9, A10, Lm2; :: thesis: verum

end;

hence ( A is_finer_than B or B is_finer_than A ) ; :: 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 A6, EQREL_1:def 3;
consider x being set such that
A14: x = Class (R1,c) ;
take x = x; :: thesis: ( x in A & y c= x )
thus x in A by A4, A12, A14, EQREL_1:def 3; :: thesis: y c= x
thus y c= x by A3, A5, A11, A13, A14, Lm2; :: thesis: verum

end;

hence ( A is_finer_than B or B is_finer_than A ) ; :: 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