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