let X be set ; :: thesis: for E being Tolerance of X holds CohSp E = TolSets E
let E be Tolerance of X; :: thesis: CohSp E = TolSets E
thus CohSp E c= TolSets E :: according to XBOOLE_0:def 10 :: thesis: TolSets E c= CohSp E

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in CohSp E or x in TolSets E )
assume x in CohSp E ; :: thesis: x in TolSets E
then x is TolSet of E by Th14;
hence x in TolSets E by TOLER_1:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in TolSets E or x in CohSp E )
assume x in TolSets E ; :: thesis: x in CohSp E
then x is TolSet of E by TOLER_1:def 3;
hence x in CohSp E by Th14; :: thesis: verum