let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL holds fam_class f is Classification of X
let f be PartFunc of [:X,X:],REAL ; :: thesis: fam_class f is Classification of X
for A, B being a_partition of X st A in fam_class f & B in fam_class f & not A is_finer_than B holds
B is_finer_than A

proof

let A, B be a_partition of X; :: thesis: ( A in fam_class f & B in fam_class f & not A is_finer_than B implies B is_finer_than A )
assume that
A1: A in fam_class f and
A2: B in fam_class f ; :: thesis: ( A is_finer_than B or B is_finer_than A )
consider a1 being non negative real number , R1 being Equivalence_Relation of X such that
A3: R1 = (low_toler f,a1) [*] and
A4: Class R1 = A by A1, Def5;
consider a2 being non negative real number , R2 being Equivalence_Relation of X such that
A5: R2 = (low_toler f,a2) [*] and
A6: Class R2 = B by A2, Def5;

now

per cases ( a1 <= a2 or a1 > a2 ) ;

suppose A7: a1 <= a2 ; :: thesis: ( A is_finer_than B or B is_finer_than A )

now

let x be set ; :: thesis: ( x in A implies ex y being set st
( y in B & x c= y ) )
assume x in A ; :: thesis: ex y being set st
( y in B & x c= y )
then consider c being set such that
A8: c in X and
A9: x = Class R1,c by A4, EQREL_1:def 5;
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 5; :: thesis: x c= y
thus x c= y by A3, A5, A7, A9, A10, Lm2; :: thesis: verum

end;

hence ( A is_finer_than B or B is_finer_than A ) by SETFAM_1:def 2; :: thesis: verum

end;

suppose A11: a1 > a2 ; :: thesis: ( A is_finer_than B or B is_finer_than A )

now

let y be set ; :: thesis: ( y in B implies ex x being set st
( x in A & y c= x ) )
assume y in B ; :: thesis: ex x being set st
( x in A & y c= x )
then consider c being set such that
A12: c in X and
A13: y = Class R2,c by A6, EQREL_1:def 5;
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 5; :: thesis: y c= x
thus y c= x by A3, A5, A11, A13, A14, Lm2; :: thesis: verum

end;

hence ( A is_finer_than B or B is_finer_than A ) by SETFAM_1:def 2; :: thesis: verum

end;

end;

end;

hence ( A is_finer_than B or B is_finer_than A ) ; :: thesis: verum

end;

hence fam_class f is Classification of X by Def1; :: thesis: verum