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