defpred S₁[ Element of , Element of ] means $1,$2 are_in_tolerance_wrt a;
consider R being Relation of , such that
A1: for x, y being Element of holds
( [x,y] in R iff S₁[x,y] ) from RELSET_1:sch 2();
reconsider R = R as Relation of ;
take R ; :: thesis: for x, y being Element of holds
( [x,y] in R iff x,y are_in_tolerance_wrt a )
thus for x, y being Element of holds
( [x,y] in R iff x,y are_in_tolerance_wrt a ) by A1; :: thesis: verum