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

consider X being set such that

A1: for x being object holds

( x in X iff ( x in PARTITIONS the carrier of M & S_{1}[x] ) )
from XBOOLE_0:sch 1();

X c= PARTITIONS the carrier of M by A1;

then reconsider X1 = X as Subset of (PARTITIONS the carrier of M) ;

take X1 ; :: 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 ) )

let x be object ; :: thesis: ( 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 ) )

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

( R = (dist_toler (M,a)) [*] & Class R = x ) ) by A1; :: thesis: ( ex a being non negative Real ex R being Equivalence_Relation of M st

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

given a being non negative Real, R being Equivalence_Relation of M such that A2: ( R = (dist_toler (M,a)) [*] & Class R = x ) ; :: thesis: x in X1

Class R in PARTITIONS the carrier of M by PARTIT1:def 3;

hence x in X1 by A1, A2; :: thesis: verum

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

consider X being set such that

A1: for x being object holds

( x in X iff ( x in PARTITIONS the carrier of M & S

X c= PARTITIONS the carrier of M by A1;

then reconsider X1 = X as Subset of (PARTITIONS the carrier of M) ;

take X1 ; :: 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 ) )

let x be object ; :: thesis: ( 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 ) )

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

( R = (dist_toler (M,a)) [*] & Class R = x ) ) by A1; :: thesis: ( ex a being non negative Real ex R being Equivalence_Relation of M st

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

given a being non negative Real, R being Equivalence_Relation of M such that A2: ( R = (dist_toler (M,a)) [*] & Class R = x ) ; :: thesis: x in X1

Class R in PARTITIONS the carrier of M by PARTIT1:def 3;

hence x in X1 by A1, A2; :: thesis: verum