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