defpred S₁[ set ] means ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler f,a) [*] & Class R = $1 );
consider A being set such that
A1: for x being set holds
( x in A iff ( x in PARTITIONS X & S₁[x] ) ) from XBOOLE_0:sch 1();
A c= PARTITIONS X

proof

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

end;

then reconsider A1 = A as Subset of (PARTITIONS X) ;
take A1 ; :: thesis: for x being set holds
( x in A1 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler f,a) [*] & Class R = x ) )
let x be set ; :: thesis: ( x in A1 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler f,a) [*] & Class R = x ) )
thus ( x in A1 implies ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler f,a) [*] & Class R = x ) ) by A1; :: thesis: ( ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler f,a) [*] & Class R = x ) implies x in A1 )
given a being non negative real number , R being Equivalence_Relation of X such that A2: ( R = (low_toler f,a) [*] & Class R = x ) ; :: thesis: x in A1
Class R in PARTITIONS X by PARTIT1:def 3;
hence x in A1 by A1, A2; :: thesis: verum