scheme :: TOLER_1:sch 1
ToleranceEx{ F1() -> set , P1[ object , object ] } :
ex T being Tolerance of F1() st
for x, y being set st x in F1() & y in F1() holds
( [x,y] in T iff P1[x,y] )
provided
A1: for x being set st x in F1() holds
P1[x,x] and
A2: for x, y being set st x in F1() & y in F1() & P1[x,y] holds
P1[y,x]