:: deftheorem Def3 defines CohSp COH_SP:def 3 :
for X being set
for E being Tolerance of X
for b₃ being Coherence_Space holds
( b₃ = CohSp E iff for a being set holds
( a in b₃ iff for x, y being set st x in a & y in a holds
[x,y] in E ) );