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

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

hence
fam_class f is Classification of X
by Def1; :: thesis: verum
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;

end;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 )end;

hence
( A is_finer_than B or B is_finer_than A )
; :: thesis: verumper cases
( a1 <= a2 or a1 > a2 )
;

end;

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

end;

now :: thesis: for x being set st x in A holds

ex y being set st

( y in B & x c= y )

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

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

end;

now :: thesis: for y being set st y in B holds

ex x being set st

( x in A & y c= x )

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