consider R being Relation of D such that
A1: for x, y being set holds
( [x,y] in R iff ( x in D & y in D & S₁[x,y] ) ) from RELSET_1:sch 5();
take R ; :: thesis: for A, B being set holds
( [A,B] in R iff ( A in D & B in D & ( for a, b being set st a in A & b in B holds
[a,b] in the ToleranceRel of P ) ) )
thus for A, B being set holds
( [A,B] in R iff ( A in D & B in D & ( for a, b being set st a in A & b in B holds
[a,b] in the ToleranceRel of P ) ) ) by A1; :: thesis: verum