theorem Th14: :: COH_SP:14

for a, X being set
for E being Tolerance of X holds
( a in CohSp E iff a is TolSet of E )