let X be set ; :: thesis: for R being Tolerance of X
for x being set st x in X holds
ex y being set st x in Class R,y
let R be Tolerance of X; :: thesis: for x being set st x in X holds
ex y being set st x in Class R,y
let x be set ; :: thesis: ( x in X implies ex y being set st x in Class R,y )
assume x in X ; :: thesis: ex y being set st x in Class R,y
then x in Class R,x by Th28;
hence ex y being set st x in Class R,y ; :: thesis: verum