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

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