defpred S_{1}[ object ] means ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = $1 );

A3: for X1, X2 being Subset of (PARTITIONS the carrier of M) st ( for x being object holds

( x in X1 iff S_{1}[x] ) ) & ( for x being object holds

( x in X2 iff S_{1}[x] ) ) holds

X1 = X2 from LMOD_7:sch 1();

let X1, X2 be Subset of (PARTITIONS the carrier of M); :: thesis: ( ( for x being object holds

( x in X1 iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) & ( for x being object holds

( x in X2 iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) implies X1 = X2 )

assume ( ( for x being object holds

( x in X1 iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) & ( for x being object holds

( x in X2 iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) ) ; :: thesis: X1 = X2

hence X1 = X2 by A3; :: thesis: verum

( R = (dist_toler (M,a)) [*] & Class R = $1 );

A3: for X1, X2 being Subset of (PARTITIONS the carrier of M) st ( for x being object holds

( x in X1 iff S

( x in X2 iff S

X1 = X2 from LMOD_7:sch 1();

let X1, X2 be Subset of (PARTITIONS the carrier of M); :: thesis: ( ( for x being object holds

( x in X1 iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) & ( for x being object holds

( x in X2 iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) implies X1 = X2 )

assume ( ( for x being object holds

( x in X1 iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) & ( for x being object holds

( x in X2 iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) ) ; :: thesis: X1 = X2

hence X1 = X2 by A3; :: thesis: verum