defpred S₁[ 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₁[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