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 A1: ( A in fam_class f & B in fam_class f ) ; :: thesis: ( A is_finer_than B or B is_finer_than A )
then consider a1 being non negative real number , R1 being Equivalence_Relation of X such that
A2: R1 = (low_toler f,a1) [*] and
A3: Class R1 = A by Def5;
consider a2 being non negative real number , R2 being Equivalence_Relation of X such that
A4: R2 = (low_toler f,a2) [*] and
A5: Class R2 = B by A1, Def5;

now

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

suppose A6: 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 A7: x in A ; :: thesis: ex y being set st
( y in B & x c= y )
consider c being set such that
A8: ( c in X & x = Class R1,c ) by A3, A7, EQREL_1:def 5;
consider y being set such that
A9: y = Class R2,c ;
take y = y; :: thesis: ( y in B & x c= y )
thus y in B by A5, A8, A9, EQREL_1:def 5; :: thesis: x c= y
thus x c= y by A2, A4, A6, A8, A9, 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 A10: 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 A11: y in B ; :: thesis: ex x being set st
( x in A & y c= x )
consider c being set such that
A12: ( c in X & y = Class R2,c ) by A5, A11, EQREL_1:def 5;
consider x being set such that
A13: x = Class R1,c ;
take x = x; :: thesis: ( x in A & y c= x )
thus x in A by A3, A12, A13, EQREL_1:def 5; :: thesis: y c= x
thus y c= x by A2, A4, A10, A12, A13, 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