let X be set ; :: thesis: for T being Tolerance of X holds TolClasses T c= TolSets T
let T be Tolerance of X; :: thesis: TolClasses T c= TolSets T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in TolClasses T or x in TolSets T )
assume x in TolClasses T ; :: thesis: x in TolSets T
then x is TolSet of T by Def7;
hence x in TolSets T by Def6; :: thesis: verum