defpred S1[ object ] means ex a being non negative Real 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 object holds
( x in A iff ( x in PARTITIONS X & S1[x] ) ) from A c= PARTITIONS X by A1;
then reconsider A1 = A as Subset of () ;
take A1 ; :: thesis: for x being object holds
( x in A1 iff ex a being non negative Real ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) )

let x be object ; :: thesis: ( x in A1 iff ex a being non negative Real 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 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 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, 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