defpred S_{1}[ 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 & S_{1}[x] ) )
from XBOOLE_0:sch 1();

A c= PARTITIONS X by A1;

then reconsider A1 = A as Subset of (PARTITIONS X) ;

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

( 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 & S

A c= PARTITIONS X by A1;

then reconsider A1 = A as Subset of (PARTITIONS X) ;

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