let a, X be set ; :: thesis: for E being Tolerance of X holds
( a in CohSp E iff a is TolSet of E )
let E be Tolerance of X; :: thesis: ( a in CohSp E iff a is TolSet of E )
thus ( a in CohSp E implies a is TolSet of E ) :: thesis: ( a is TolSet of E implies a in CohSp E )

proof

assume a in CohSp E ; :: thesis: a is TolSet of E
then for x, y being set st x in a & y in a holds
[x,y] in E by Def3;
hence a is TolSet of E by TOLER_1:def 1; :: thesis: verum

end;

assume a is TolSet of E ; :: thesis: a in CohSp E
then for x, y being set st x in a & y in a holds
[x,y] in E by TOLER_1:def 1;
hence a in CohSp E by Def3; :: thesis: verum