defpred S_{1}[ 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_{1}[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

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

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