defpred S₁[ set ] means ex a being non negative real number 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 set holds
( x in X iff ( x in PARTITIONS the carrier of M & S₁[x] ) ) from XBOOLE_0:sch 1();
X c= PARTITIONS the carrier of M

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in PARTITIONS the carrier of M )
assume a in X ; :: thesis: a in PARTITIONS the carrier of M
hence a in PARTITIONS the carrier of M by A1; :: thesis: verum

end;

then reconsider X1 = X as Subset of (PARTITIONS the carrier of M) ;
take X1 ; :: thesis: for x being set holds
( x in X1 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler M,a) [*] & Class R = x ) )
let x be set ; :: thesis: ( x in X1 iff ex a being non negative real number 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 number 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 number 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 number , 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